# Book:D.C. Ince/An Introduction to Discrete Mathematics and Formal System Specification

## D.C. Ince: *An Introduction to Discrete Mathematics and Formal System Specification*

Published $1988$, **Oxford University Press**

- ISBN 0-19-859664-2.

### Subject Matter

### Contents

- Preface (Milton Keynes, May 1987)

- Part I

- 1 COMMERCIAL SOFTWARE DEVELOPMENT
- 1.1 The software life cycle
- 1.1.1 Software requirements analysis and system specification
- 1.1.2 System design
- 1.1.3 Detailed design
- 1.1.4 Coding
- 1.1.5 Integration
- 1.1.6 Maintenance
- 1.1.7 Validation and verification

- 1.2 Current problems in software development
- 1.3 Formal methods of software development

- 1.1 The software life cycle

- 1 COMMERCIAL SOFTWARE DEVELOPMENT

- 2 CUSTOMER REQUIREMENTS, SYSTEM SPECIFICATION, AND NATURAL LANGUAGE
- 2.1 The contents of the statement of requirements
- 2.2 Deficiencies in statements of requirements and specifications
- 2.3 The qualities of a good systems specification
- 2.4 A procedure for requirements analysis and specification
- 2.5 An example of requirements analysis-a reactor monitoring system
- 2.5.1 The statement of requirements
- 2.5.2 An examination of the statement of requirements

- 2.6 Mathematics and system specification
- 2.7 Problems with formal system specification

- 2 CUSTOMER REQUIREMENTS, SYSTEM SPECIFICATION, AND NATURAL LANGUAGE

- Part II

- 3 PROPOSITIONAL CALCULUS
- 3.1 Propositions and propositional operators
- 3.2 Contradictions and tautologies
- 3.3 Requirements analysis, system specification, and propositional calculus
- 3.3.1 Simplification
- 3.3.2 Reasoning
- 3.3.2.1 Reasoning using transformation to implication form
- 3.3.2.2 Inference using invalid argument

- 3.4 The detection of inconsistencies
- 3.5 An example of the use of propositional calculus in the specification of a coupled computer system
- 3.6 Summary

- 3 PROPOSITIONAL CALCULUS

- 4. PREDICATE CALCULUS
- 4.1 Propositions as predicates
- 4.2 Quantifiers as predicates
- 4.2.1 Existential quantification
- 4.2.2 Universal quantification

- 4.3 Proof and deduction
- 4.4 Reasoning about natural numbers
- 4.5 Predicate calculus and design specification
- 4.6 Requirements analysis and specification as the construction of informal theories

- 4. PREDICATE CALCULUS

- 5. SET THEORY
- 5.1 Sets and subsets
- 5.1.1 Set specification
- 5.1.2 The empty set
- 5.1.3 Subsets and the power set

- 5.2 Set operators
- 5.2.1 Set equality
- 5.2.2 Set union and set intersection
- 5.2.3 Set difference
- 5.2.4 The cross-product
- 5.2.5 Set cardinality

- 5.3 Reasoning and proof in set theory
- 5.4 Modelling a filing system

- 5.1 Sets and subsets

- 5. SET THEORY

- 6 RELATIONS AND RELATIONAL OPERATORS
- 6.1 Relations as sets of ordered pairs
- 6.2 Relation composition
- 6.3 The identity relation
- 6.4 Relation restriction
- 6.5 The transitive closure of a relation
- 6.6 Theorems involving relations

- 6 RELATIONS AND RELATIONAL OPERATORS

- 7 FUNCTIONS AND SEOUENCES
- 7.1 Functions
- 7.2 Higher-order functions
- 7.3 Modelling a version-control system using higher-order functions
- 7.4 Functions as lambda expressions
- 7.4.1 Curried functions

- 7.5 Sequences as functions
- 7.6 Applying sequences in specifications - a print spooler

- 7 FUNCTIONS AND SEOUENCES

- 8 INDUCTION AND RECURSIVE SPECIFICATION
- 8.1 Recursive specification
- 8.2 Numbers and induction
- 8.3 Set induction
- 8.4 Sequence induction

- 8 INDUCTION AND RECURSIVE SPECIFICATION

- Part III

- 9 THE SPECIFICATION LANGUAGE Z
- 9.1 Schemas
- 9.2 The structure of Z specifications
- 9.2.1 Schema inclusion
- 9.2.2 Events and observations in Z

- 9.3 Some examples of schema use

- 9 THE SPECIFICATION LANGUAGE Z

- 10 OPERATORS AND OBJECTS IN Z
- 10.1 Numbers and sets of numbers
- 10.2 Sets
- 10.3 Relations
- 10.4 Functions and sequences
- 10.4.1 Functions
- 10.4.2 Sequences

- 10.5 Modelling a back-order system
- 10.5.1 The statement of requirements
- 10.5.2 Specifying the static properties of the system

- 10 OPERATORS AND OBJECTS IN Z

- 11 THE Z SCHEMA CALCULUS
- 11.1 Schemas as objects
- 11.2 Extending and manipulating schemas
- 11.3 Z schema conventions
- 11.4 Logical operators and schemas
- 11.5 Using the schema calculus - a simple query system for a spare-parts data base

- 11 THE Z SCHEMA CALCULUS

- 12 Z SPECIFICATIONS IN ACTION - THE UNIVERSITY OF LINCOLN LIBRARY SYSTEM
- 12.1 The statement of requirements
- 12.2 The static properties of the system
- 12.3 The operations
- 12.4 Presenting a Z specification
- 12.5 Postscript

- 12 Z SPECIFICATIONS IN ACTION - THE UNIVERSITY OF LINCOLN LIBRARY SYSTEM

- APPENDIX: DEFINITION OF Z OPERATORS

- REFERENCES

- INDEX