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: