Poised Solutions Tech Library

An Introduction to Formal Specification and Z

An Introduction to Formal Specification and Z Author: Ben Potter Jane Sinclair David Till Publisher: Prentice Hall Published: 1991 Pages: 303

An Introduction to Formal Specification and Z

An Introduction to Formal Specification and Z Chapters

An Introduction to Formal Specification and Z Chapters

1. Formal specification in the context of software engineering
   • Software engineering
   • The software life-cycle
   • The importance of specification
   • The need for formality and abstraction
   • The notation we shall use
   • Further reading
2. An informal introduction to logic and set theory
   • Sets
     • Basic ideas of sets
     • Set operators
     • Set comparisons
   • Propositions and predicates
     • Combining popositions
     • Introducing the quantifiers
     • Quantifiers applied to lists of variables
   • More about sets
     • Defiing sets using predicates
     • Tuples and sets of tuples
     • Sets of sets
   • Further reading
3. A first specification
   • An informal presentation
   • A more formal presentation
     • Word-For-Word: a vocabulary system
4. The Z notation: the mathematical language
   • Why types are used
   • The Z type systems
     • Basic types
     • Powersets
     • Cartesian product
     • Declaration abbreviations
     • Simple data types
     • Other type construction mechanisms
   • Extending the notation
     • From the basic Z library
     • Extending the qualification notation
     • Extending the notation of set expressions
   • Some specification construction units
     • Axiomatic descriptions
     • Abbreviation definitions
     • Generic definitions
   • Summary of notation introduced
   • Further reading
5. The Z notation: relations and functions
   • Relations
     • Notations for relations
     • Domains and ranges
     • Example
   • Operations on relations
     • Relational inverse
     • Restriction and subtraction
     • Composition of relations
     • Relational image
   • Functions
     • Partial and total functions
     • Examples
     • Injecctive and surjective functions
     • Surjection and bijections
     • Finite functions
     • Summary or properties of funcions
   • Operations on functions
     • Generic definitions of operations
     • Example
   • Lambda notation
   • Sequences
     • Representing sequences
     • Operations on sequences
6. The Z notation: schemas and specification structure
   • Schema notation
   • An example application: LibSys
   • Schemas describing abstract states
   • Schemas describing operations
   • The schema caculus
     • Schema inclusion
     • Schema decoration
     • Schema disjunction
     • Schema conjunction
     • Schema negation
     • Schema hiding operators
     • Schema compoisition
     • Schema preconditions
   • Further reading
7. A first specification revisited
   • The expanded vocabulary system
     • Given sets and global variables
     • Some general theory: alaphabetical orders
     • Abstract state definition
     • Initialisation
     • Definition of partial operations
     • Precondition investigation and summary
     • Error handling
     • Summary of operations
   • The structure of specification documents
   • Further reading
8. Formal reasoning
   • A first example
   • Schemas as predicates
   • Reasoning about specifications
     • The Initialisation Theorem
     • Precondition simplification
     • Properties of a specification
     • Refinement
   • What is a proof?
   • Reasoning with propositions
     • Some propositional laws
     • Examples using laws for propositions
   • Reasoning with predicates
     • Free Variables and Bound Variables
     • Substitution
     • Laws for quantifiers
     • Examples using laws for predicates
   • A library of laws
   • Examples of reasoning about a specification
     • An iniitalisation theorem
     • Simplifying a precondition
     • Proving a property of a specification
   • Further reading
9. From specification to program: data and operation refinement
   • What is refinement
     • Refinement of relations
     • Refinement of operations on the same state
     ?
   • Data refinement
     • An example data refinement
     • The Initial States Theorem
   • Operation refinement
     • An example operation refinement
     • The Applicability Theorem
     • The Correctness Theorem
   • Further discussion and summary
   • Further reading
10. From specification to program: operation decomposition
    • Declarations
    • using local variables
    • Reducing the frame
    • Assignment
    • Sequencing
    • Alternation
    • Iteration
    • Functions and Procedures
    • An example of operation decomposition
      • Translating the concrete state definition
      • Translating a concrete operation
    • Further reading
11. From theory to practice
    • The place of formal methods
    • Notes for new users
      • Effects of formal methods
    • Relationship to other methods
    • Prototyping
    • Support tools
    • Case histories
      • The CICS product
      • The Inmos T800 Floating Point Transputer
      • A cautionary tale
    • Useful Sources
    • Future possibilities

An Introduction to Formal Specification and Z Appendices

1. The syntax of Z
2. Bibliography
3. Index