## Formal Specification and DesignFormal specification is a method for precisely modelling computer-based systems that combines concepts from software engineering and mathematical logic. In this book the authors describe algebraic and state-based specification techniques from the unified view of the Common Object-oriented Language for Design, COLD, a wide-spectrum language in the tradition of VDM and Z. The kernel language is explained in detail, with many examples, including: set representation, a display device, an INGRES-like database system, and a line editor. Fundamental techniques such as initial algebra semantics, loose semantics, partial functions, hiding, sharing, predicate and dynamic logic, abstraction functions, representation of invariants and black-box correctness are also presented. More advanced ideas, for example Horn logic, and large systems are given in the final part. Appendices contain full details of the language's syntax and a specification library. Techniques for software development and design are emphasised throughout, so the book will be an excellent choice for courses in these areas. |

### What people are saying - Write a review

User Review - Flag as inappropriate

It was okey but alot of this stuff is super hard to understand and is not explained very well.

### Contents

1 Introducing the basic concepts | 3 |

2 Setting up algebraic specifications | 33 |

3 Structuring algebraic specifications | 59 |

4 Implementing algebraic specifications | 79 |

II Statebased specification | 111 |

5 From algebras to states | 113 |

6 Setting up statebased specifications | 143 |

7 Structuring statebased specifications | 171 |

III Advanced techniques | 241 |

9 Theoretical topics | 243 |

10 Additional language constructs | 263 |

11 Towards large systems | 287 |

Bibliography | 303 |

A Syntax | 309 |

B Standard library | 317 |

332 | |

### Other editions - View all

### Common terms and phrases

algebraic speciﬁcation algorithmic applied assertion Attr AXIOM FORALL Bool box correct buffer Char CLASS FUNC CLASS SORT clause COLD-K component constructs cursor data types deﬁned deﬁnedness denotes dynamic logic east_street example Expr expression ExprList ﬁeld ﬁrst FORALL m:Nat,n:Nat FORALL n:Nat formal speciﬁcation FUNC empty FUNC f FUNC IND FUNC function name gap2 Geldrop Hoare logic Horn clause identiﬁer imperative programming implementation IMPORT NAT IND FORALL IND FUNC IND inductive deﬁnitions initial algebra interpretation introduced invariant is_gen is_in is_in(i,s List mapping means modiﬁcation Nat IND NAT INTO IMPORT natural numbers notation notion object names operations parameter partial function postcondition predicate deﬁnition PREV PROC procedure programming languages programming variable quantiﬁers Queue renaming RName satisﬁes scheme Section semantics Set_VName Set2 Seti SORT Item sort names speciﬁcation language Stack state-based speciﬁcation String succ(n syntactic syntactic sugar syntax transition relation tuples undeﬁned VName zero