Contents

• Contents
• Introduction to Formal Specification
  • A First Specification Language
  • What is a Software Specification?
  • What is a Formal Specification?
  • The Scope of this Book
  • Summary
• Mathematical Structures for Formal Specification
  • Introduction
  • Sets
    • Terminology
    • Subsets
    • Equality
    • Intersection
    • Union
    • Null or Empty Set
    • Disjoint Sets
    • Cardinality and Finite Sets
    • Power Set
    • Set Difference
    • Associativity and Commutativity
  • Cartesian Product and Tuples
  • Mappings
    • Relations and Mappings
    • Domain and Range
    • Composition of Mappings
    • Mappings and PASCAL
  • Types of Mapping (Function)
    • Injective
    • Surjective
    • Bijective
    • Total and Partial Mappings
    • Two Examples of Mappings
  • Binary Relations
    • Equivalence Relation
    • Partitions and Equivalence Classes
    • Partial Ordering
    • Examples of Partially Ordered Sets
    • Total Ordering
  • Binary Operations
    • Unary Operations
    • Common Properties or Attributes of Operations
    • Closure
  • Operation Types
  • Bags and Lists
    • Bags
    • Lists
  • Mathematical Induction
  • Summary
• Introduction to Model-based Specification using VDM
  • Introduction
  • The Implicit Specification of Operations
    • Examples of Implicit Specifications
    • The Logical Condition
    • Reasoning with pre- and post-conditions
  • Introduction to VDM Data Types
    • The Primitive Types
    • The Set Type
    • Worked Example using Sets
    • Implicit Definition of Sets
  • Creating VDM State Models
    • An Example using an External State
    • Composites
  • A Systematic Approach to the Construction of VDM Specifications
    • First Step: Creation of a System State
    • Second Step: Construction of Data Type Invariants
    • Third Step: Modelling of the system's operations
    • Fourth Step: Discharging Proof Obligations
    • Fifth Step: Specification Refinement
  • Formal Proof Obligations
  • Summary
• The Sequence and Map types
  • Introduction
  • The Sequence Data Type
  • A Model-based Specification of the Stack
    • Requirement
    • Creation of the System State
    • Construction of Data Type Invariant
    • Modelling of the System's Operations
    • Proof Obligations for the Stack
    • Validation: a simple example
  • A Horse Racing Information System
    • Creation of a System State
    • Construction of Data Type Invariant
    • Modelling of the System's Operations
    • Proof Obligations
  • The Map Data Type
    • Intuitive view of maps
    • Map Operations
  • The Symbol Table
    • Requirement
    • Creation of a System State: First Attempt
    • Creation of the System State: A better attempt
    • Construction of the Data Type Invariant
    • Modelling of the Operations
  • Summary
• Building Up VDM Specifications
  • Introduction
  • User-Defined Functions
    • Function Definitions in VDM
    • Proof Obligations for Implicitly Defined Functions
    • Explicitly Defined Functions
    • Proof Obligations for Explicitly Defined Functions
    • The Relationship between Implicit and Explicit Functions
    • An Inductive Proof
    • Induction and Proof Obligations
    • Partial Functions
  • The Specification of a Partial Order
    • Weak and Strong Partial Orders
    • A Plan as a Strong Partial Order of Actions
    • Developing the Specification
    • Creation of the Partial Order Data Type
    • The Data Type Invariant
    • Modelling the Operations
    • Proof Obligations
  • An Extension to the Specification
    • New Requirements
    • A New Data Model
    • Modelling the New Operations
  • Summary
• Specification Case Study in VDM
  • Introduction
  • Automatic Planning
    • Objects in the Blocks World
    • Actions in the Blocks World
    • Action Application
    • Plans
  • An Abstract Specification of the Planner
    • A VDM Representation of Planning Problems
    • Exercises 6.3
    • Invariants for the Planning Problem
    • A First Specification of the Planner
  • A Design Level Specification
    • A Technique for Solving Planning Problems
    • An Introduction to Goal Achievement in Planning
    • Modelling the VDM State
    • The State Invariant
    • VDM Operations
    • Proof Obligations
  • Summary
• Prototyping VDM Specifications
  • Introduction
  • Prolog as a Prototyping Language for VDM
    • Prolog
  • VDM to Prolog Translation
    • Data Type Implementation
    • Operator Translation
    • The Existential Quantifiers
    • The Universal Quantifier
    • Prototyping Pitfalls
  • The Planner Prototype
    • The INIT Operator
    • The ACHIEVE Operators
  • Summary
• Algebraic Specification of Abstract Data Types
  • Introduction
  • Specification of Abstract Data Types
    • Sorts and Types of Interest
    • The Syntax of the Operations
    • Constructors and Accessors
    • Exercises
  • Semantic Specification in Modula-2 and Ada
  • Algebraic Specification of Abstract Data Types
    • An Algebraic Specification Language
    • Pre-defined Types
  • Algebraic Specification of an Unbounded Stack
    • The Operations and their Syntax
    • Sorts
    • Axioms for the Unbounded Stack
    • Interpretations of a Signature
    • Comparison with VDM
  • Completeness
  • Examples of Evaluations
    • Example 1
    • Example 2
  • Axioms and Term Rewriting
    • Pattern Matching and Unification
    • Term Rewriting Example
    • Term Rewriting for Stack
  • Summary
• The Queue and Binary Tree
  • Introduction
  • Atomic Constructors
  • Heuristics for Axiomatisation
  • Algebraic Specification of a Queue of Natural Numbers
    • Axiomatisation for Queue
    • Examples of Evaluating Terms
    • Exercises
    • Specification of Stack and Queue using VDM
  • Algebraic Specification of a Binary Tree
    • Simple Examples of Binary Trees
    • Tree Traversal
  • Hidden Operations
  • VDM Specification of an Ordered Binary Tree
    • The VDM Operation build
    • The VDM Operations $left\_tree$ and $right\_tree$
    • The VDM Operation node
    • The VDM Operation is_empty?
    • The VDM Operation $is\_in?$
  • Functional Programming Languages and Data Types
  • Errors and Algebraic Specifications
  • Use of Error Values
    • Strictness and Implicit Axioms
  • Subsorts and Subtypes
    • Operation Overloading
  • Error Detection and Error Handling
  • Specification of a Stack
  • Summary
• Algebras and Abstract Data Types
  • Introduction
  • Algebras
    • Homogeneous or Single-sorted Algebras
    • Heterogeneous or Many-sorted Algebras
    • Models
  • Signatures and Heterogeneous Algebras
  • Interpretations of a Signature
  • Term Algebra
  • Transformations between Algebras
    • Homomorphism
    • Isomorphism
    • Some Examples and a Counter Example
  • Axioms and Theory Presentations
    • Axioms and Equational Logic
  • Algebras as Models of a Theory
    • Model 1
    • Model 2
  • Initial Algebras
    • Initial Models - Junk and Confusion
    • Models of a Boolean Theory
    • The Importance of Initial Models
    • Models in VDM
  • Deriving an Initial Algebra
    • Quotient Term Algebra
    • Canonical Term Algebra and Reduced Expressions
    • Canonical Term Algebras and Implementations
  • Axioms as Equations
  • Axioms as Rewrite Rules
  • Operational Semantics
  • Initial versus Final Semantics
  • Summary
    • Signatures and Algebras
    • Theory Presentations and their Interpretations
    • Axioms as Rewrite Rules
• Building Larger Specifications
  • Introduction
  • Estate Agent Example
    • For-sale and Under-offer Mode
    • Operations for the Database
    • Axioms for ``delete-house''
    • Axioms for ``is-on-market?''
    • Axioms for ``is-under-offer?''
    • Axioms for ``make-offer''
  • Compound Modules
    • Combinators
    • Module Expressions
  • Petrochemical Plant Example
    • Petrochemical Tank - Version 1
    • The Constructors ``add-chem'' and ``!fill''
    • Axioms for ``remove'', ``empty-tank'' and ``change-pc''
    • Axioms for Boolean-valued Operations
    • Axioms for ``chem'' and ``level''
  • Petrochemical Tank - Version 2
• Canonical Terms and Proof Obligations
  • Introduction
  • Proof Obligation : Canonical Terms (Forms)
    • Canonical Terms and Reduced Expressions
  • Proof Obligations : Consistency and Completeness
    • Consistency
    • Completeness
    • Sufficient Completeness
    • Extensibility (Conservative Extension)
    • Validating an Algebraic Specification
    • Termination
  • Specification of a Set
    • Requirement
    • Additional Axioms
    • Use of Hidden Operations
    • Specification of a Bag
    • Other Atomic Constructors for Set
  • Structural Induction
    • Canonical Forms for the Stack
    • Proof of Canonical Property for Stack
    • Proof of the Sufficient Completeness of Stack
  • Proof of Canonical Property for Set
  • Attributes of an Operation
  • Derivation of Attributes from Axioms
  • Summary
• Prototyping Algebraic Specifications
  • Introduction
  • Initial Models and Prototyping
  • Prototyping Specifications Using OBJ3
  • Overview of OBJ3
    • Some OBJ3 Prototypes
  • Prototyping Using Functional Languages
  • Prototyping Algebraic Specifications in Prolog
    • Use of an Imperative Programming Language
  • Many-sorted and Order-sorted Algebras
    • Mathematical Semantics of OSA
    • An Operational Semantics for Order-sorted Algebra
  • Summary
• Joint Case Study: Development of a Neural Network Specification
  • Introduction
  • Neural Networks
    • A Simple Model of Neurons
    • Applications of Neural Networks
    • Types of Neural Networks
  • Specifying a Neural Network
  • Algebraic Specification of a Neural Network
  • Structure of a Neural Network
    • Specification of Incoming and Outgoing Connections
    • Specification of a Neuron
    • Overview of the Specification for the Network
  • Specifications for the Component Abstract Data Types
    • The Specification ``Outfo''
    • The Specification ``Info''
  • Specification of the Neural Network
  • The Operations of ``Neural-Network''
    • The Operation ``sleep''
    • The Operation ``fire''
    • The Operation ``one-shot''
    • The Operations ``spread-out'' and ``spread''
  • The Operations ``all-settled?'' and ``settle''
  • Example Evaluation of a Neural Network
  • Some Comments on the Algebraic Specification
  • VDM Specification of the Neural Network
    • Requirements
    • Creation of a Data Model: First Attempt
    • Creation of the Data Type Invariant: First Attempt
    • Creation of a Data Model: Second Attempt
    • Creation of Data Type Invariant: Second Attempt
    • The Network Operation
    • Exercises 14.8
  • Summary
• Background, Comparison and Summary
  • Introduction
    • Likely Applications for Formal Specification
    • Which Type of Formal Specification?
  • Comparison of Specification Languages
    • General
    • Operator Definition
    • Building Up Specifications
    • The Data Type Invariant
    • Specification versus High Level Programming Languages
  • History and Applications
    • VDM and Model-based Specification
    • Algebraic Specification

Preface