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

From ProofWiki
Jump to: navigation, search

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
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


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
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
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
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
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
8 INDUCTION AND RECURSIVE SPECIFICATION
8.1 Recursive specification
8.2 Numbers and induction
8.3 Set induction
8.4 Sequence induction


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
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
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
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
APPENDIX: DEFINITION OF Z OPERATORS
REFERENCES
INDEX