Book:D.C. Ince/An Introduction to Discrete Mathematics and Formal System Specification
Jump to navigation
Jump to search
D.C. Ince: An Introduction to Discrete Mathematics and Formal System Specification
Published $\text {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