An Introduction to Discrete Mathematics, Formal System Specification, and Z Book

1	Commercial software development	1
1.1	The software life cycle	1
1.2	Current problems in software development	7
1.3	Formal methods of software development	7
2	Customer requirements and specification	11
2.2	The content of the statement of requirements	12
2.3	Deficiencies in specifications	14
2.4	The qualities of a good specification	18
2.5	Carrying out analysis and system specification	20
2.6	An example of requirements analysis	21
2.7	Mathematics and system specification	26
2.8	Problems with formal system specification	29
3	Propositional calculus	32
3.2	Propositions and propositional operators	33
3.3	Contradictions and tautologies	41
3.4	Requirements analysis and specification	42
3.5	The detection of inconsistencies	65
4	Predicate calculus	69
4.2	Propositions as predicates	70
4.3	Quantifiers as predicates	73
4.4	Rules of inference and quantification	86
4.5	Predicate calculus and design specification	86
5	Set theory	94
5.2	Sets and subsets	95
5.3	Set operators	103
5.4	Reasoning and proof in set theory	107
5.5	Modelling a file system	108
6	Relations	114
6.1	Relations as sets of ordered pairs	114
6.2	Relation composition	120
6.3	The identity relation	123
6.4	Relation restriction	125
6.5	The transitive closure of a relation	130
6.6	Theorems involving relations	134
7	Functions and sequences	135
7.2	Higher-order functions	142
7.3	Modelling a version control system	145
7.4	Functions as lambda expressions	148
7.5	Sequences as functions	150
7.6	Applying sequences - a print spooler	153
8	The specification language Z	157
8.1	Schemas	157
8.2	Supporting facilities in Z	161
8.3	The structure of Z specifications	162
9	Operations and objects in Z	170
9.1	The Z toolkit	170
9.2	Numbers and sets of numbers	170
9.3	Sets	172
9.4	Relations	174
9.5	Functions and sequences	178
9.6	Modelling a back order system	186
10	The Z schema calculus	196
10.1	Schemas as objects	196
10.2	Extending and manipulating schemas	199
10.3	Z schema conventions	202
10.4	Logical operators and schemas	209
10.5	Using the schema calculus - an example	210
11	Some small Z examples	216
11.1	A block handler	216
11.2	An identifier table	219
11.3	A print spooler	221
12	A large Z specification	226
12.1	The statement of requirements	226
12.2	The static properties of the system	230
12.3	The operations	238
13	Z and design	256
13.2	The nature of design	257
13.3	Some design heuristics	262
13.4	The nature of design	265
13.5	Validating designs	271