Algebraic Specifications in Software Engineering

1. Introduction.- 1.1 Software Engineering.- 1.2 Software Life Cycle.- 1.3 Abstract Data Types and Specifications.- 1.4 Why Specifications ?.- 1.5 Why Formal Specifications ?.- 1.6 Algebraic Specifications, an Intuitive Approach.- 1.7 Survey.- 1.8 Historical Remarks on Algebraic Specifications.- 2. Abstract Data Types as Initial Algebras.- 2.1 Many-Sorted Algebra, Signature and Graphical Notation.- 2.2 Homomorphism and Isomorphism.- 2.3 Variable-Free Termlanguage.- 2.4 Word Algebra.- 2.5 Signature, Variety and Termalgebra.- 2.6 Signature and Initial Algebra.- 2.7 Abstract Data Types Defined by a Signature.- 2.8 Termlanguage.- 2.9 Substitution and Ground Substitution.- 2.10 Assignment.- 2.11 Axioms and Presentation.- 2.12 Presentation, Variety and Termalgebra.- 2.13 Equational Reasoning.- 2.14 Presentation and Initial Algebra.- 2.15 Abstract Data Types Defined by a Presentation.- 2.16 Examples.- 2.17 Induction.- 2.18 Hidden Operations and Sorts.- 2.19 Bibliographic Notes.- 3. An Algebraic Specif ication Language.- 3.1 Modularity.- 3.1.1 Modules.- 3.1.2 Import and Export Clauses.- 3.1.3 Export of the Import.- 3.2 Hierarchical Specifications.- 3.3 Notational Extensions.- 3.3.1 Ifthenelse Construct.- 3.3.2 Mixfix Notations.- 3.3.3 Conditional Axioms.- 3.3.4 Case Constructs.- 3.3.5 Let Constructs.- 3.3.6 Qualified Names and Renaming.- 3.4 Parameterized Specifications.- 3.4.1 Parameter Morphisms.- 3.4.2 Instantiations.- 3.4.3 Requirements and Induction.- 3.4.4 Remarks on Hierarchical Constraints.- 3.4.5 Renaming and Qualified Names.- 3.4.6 Partial Instantiations.- 3.4.7 Parameterized Parameter Passing.- 3.4.8 Parameterizing Requirements.- 3.5 Clusters.- 3.6 Bibliographic Notes.- 4. Constructive Specifications.- 4.1 Simple Example.- 4.2 Constructive Specifications.- 4.3 Theorems.- 4.4 Equality Operation.- 4.5 Example.- 4.6 Constructor Axioms.- 4.7 Semi-Constructive Specifications.- 4.8 Inconsistency.- 4.9 On Constructing Requirements.- 4.10 Claiming Modules.- 4.11 The Cartesian Product of Sorts.- 4.12 Constructivity and Abstraction.- 4.13 Bibliographic Notes.- 5. A Case Study: the Ferry Problem.- 5.1 Informal Description of tlie Ferry Problem.- 5.2 Formal Specification of the Ferry Problem.- 5.3 The Farmer, the Wolf, the Goat and the Cabbage.- 5.4 The Missionaries and the Cannibals.- 5.5 Specification of a Search Strategy.- 5.6 Conclusion.- 6. A Case Study: the Mini-PABX.- 6.1 Object-Oriented Design Method.- 6.2 Modularity.- 6.3 The Abstract Data Type Phone.- 6.4 Error Handling.- 6.5 The Abstract Data Type Mini-PABX.- 6.6 The Scheduling of the Messages.- 6.7 Skeleton of the Mini-PABX.- 6.8 A Two-Party Voice Call.- 6.8.1 The Module Phone.- 6.8.2 The Module PhoneMessages.- 6.8.3 The Module NextPhone.- 6.8.4 The Module OutPhone.- 6.9 Enquiry Call.- 6.9.1 The Module Phone.- 6.9.2 The Module PhoneMessages.- 6.9.3 The Module NextPhone.- 6.9.4 The Module OutPhone.- 6.10 User Actions.- 6.10.1 The Module PhoneMessages.- 6.10.2 The Module NextPhone.- 6.10.3 The Module OutPhone.- 6.11 Conclusion.- 7. Error Handling.- 7.1 The Need for an Error Handling System.- 7.2 Safety Functions.- 7.3 Safety and Unsafety Markers.- 7.4 Method of Error Specification.- 7.5 Safety Conditions.- 7.6 Miscellanies.- 7.7 Bibliographic Notes.- 8. Abstract Implementations.- 8.1 Example of the Stacks.- 8.2 Concepts of Abstract Implementations.- 8.2.1 Data Representation Part of ?A.- 8.2.2 Procedure Implementation Part of ?A.- 8.2.3 Representation Function.- 8.2.4 Implementation Invariant.- 8.2.5 Abstraction Function.- 8.2.6 Equivalence Relation.- 8.2.7 A Multi-Step Implementation Method.- 8.3 Implementation Constraints.- 8.4 Example: Scheme of Stacks.- 8.5 Example: Scheme of Symbol Tables.- 8.6 Properties and Relations.- 8.7 Bibliographic Notes.- Conclusions.- Appendix A: Syntax.- Appendix B: Rapid Prototyping, the Mini-PABX.