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 $\text {1988}$, Oxford University Press

ISBN 0-19-859664-2

Subject Matter

• Discrete Mathematics
• Computer Science

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