Formal Specifications— 1 Model Oriented
After reading this chapter, you should understand:
- What is a Software Specification
- Two methods for Formal Specifications — Model oriented and Algebraic
- VDM as a vehicle for model oriented formal specification
- Creating VDM models through a number of examples
- Specification Refinement
- Formal Proof Obligations
20.1 Formal Specifications
20.1.1 A First Specification Language
20.1.2 What is a Software Specification?
20.1.3 What is a Formal Specification?
20.1.4 An Apparent Disadvantage of FSL
20.2 Introduction to VDM
20.2.1 The Implicit Specification of Operations
20.2.2 Examples of Implicit Specifications
20.2.3 The Logical Condition
20.2.4 Reasoning with pre- and post-conditions ...