Notations for Software Design

1 Introduction.- 1.1 Software Design.- 1.2 Software Specification.- 1.3 Notations for Software Design.- 2 The Vending Machine Case.- 2.1 Objectives.- 2.2 Analysing the Application.- 2.3 Analysing the Building Blocks.- 2.4 Design.- 2.5 Realization.- 2.6 Concluding Remarks.- 3 Patterns for Definitions.- 3.1 Introduction and Motivation.- 3.2 States and State Transformers.- 3.3 Patterns for Function Definitions.- 3.4 Patterns for Predicate Definitions.- 3.5 Patterns for Sort Definitions.- 3.6 Patterns for Procedure Definitions.- 3.7 Axioms and Theorems.- 3.8 Assertions.- 3.9 Expressions.- 3.10 Concluding Remarks.- 4 Patterns for Components.- 4.1 Introduction and Motivation.- 4.2 Basic Pattern.- 4.3 Using Components.- 4.4 Signatures.- 4.5 Renamings.- 4.6 More on Component Definitions.- 4.7 Structure of Complete Descriptions.- 4.8 More on Instantiating Components.- 4.9 Concluding Remarks.- 5 Mechanisms for Naming.- 5.1 Introduction and Motivation.- 5.2 Structure of Names.- 5.3 Names in Definitions and Axioms.- 5.4 Names in Signatures and Renamings.- 5.5 Names in Instantiations.- 5.6 Object Names.- 5.7 Name Clashes.- 5.8 Names and Notational Conventions.- 5.9 Concluding Remarks.- 6 The Automatic Railway Case.- 6.1 Objectives.- 6.2 Vocabulary of the Application Domain.- 6.3 Analysis of the Application Domain.- 6.4 System Requirements.- 6.5 The Architecture of Safety.- 6.6 Components for Safety and Reachability.- 6.7 Putting the Components Together.- 6.8 Refinements of the Safety Requirement.- 6.9 Data Structures.- 6.10 Invariant Assertions.- 6.11 Algorithms.- 6.12 Proof Aspects.- 6.13 Real-time Aspects.- 6.14 Realization Aspects.- 6.15 Concluding Remarks.- 7 Pictorial Representations.- 7.1 Survey.- 7.2 Area Diagrams: General.- 7.3 Venn diagrams.- 7.4 Statecharts.- 7.5 Nassi-Shneidermann Diagrams.- 7.6 HOOD diagrams.- 7.7 Graph Diagrams: General.- 7.8 Function Graphs.- 7.9 State Transition Diagrams.- 7.10 Call Graphs.- 7.11 Import Graphs.- 7.12 Concluding Remarks.- 8 More Pictorial Representations.- 8.1 Network Diagrams: General.- 8.2 Data Flow Diagrams.- 8.3 Data Flow Diagrams with Stores.- 8.4 Flow Charts.- 8.5 Abstract Hardware Diagrams.- 8.6 State-based Abstract Hardware Diagrams.- 8.7 Petri Nets.- 8.8 SDL-like Diagrams.- 8.9 Sequence Charts: General.- 8.10 Asynchronous Sequence Charts.- 8.11 Synchronous Sequence Charts.- 8.12 Concluding Remarks.- 9 Advanced Topics.- 9.1 Introduction and Motivation.- 9.2 Review of Modular Structuring.- 9.3 How to Set up Basic Components.- 9.4 Sharing a State Space.- 9.5 Principles of Modular Structuring.- 9.6 Guidelines and Techniques.- 9.7 Mirroring.- 9.8 Object-orientedness.- 9.9 Conservativity and Visibility Consistency.- 9.10 Black Box Correctness.- 9.11 Component Invariants.- 9.12 Loop Invariants.- 9.13 Memoization.- 9.14 Concluding Remarks.- A Syntax of COLD-1.- A.1 Introduction.- A.2 Lexical Units.- A.3 Grammar.- A.4 Operator Priorities and Associativities.- B Standard Library.- B.1 Items.- B.2 Ordered Items.- B.3 Booleans.- B.4 Natural Numbers.- B.5 Integer Numbers.- B.6 Enumerations.- B.7 Characters.- B.8 Tuples.- B.9 Unions.- B.10 Finite Sets.- B.11 Finite Bags.- B.12 Finite Sequences.- B.13 Finite Maps.- C Glossary of Terms.