SPECIFICATION CASE STUDIES, Edited by Ian Hayes

 

 https://staff.itee.uq.edu.au/ianh/Papers/SCS2.pdf

SPECIFICATION CASE STUDIES
Second Edition
Copyright c© 1987, 1992 Prentice Hall International
(UK) Ltd
Appendices A and B may be copied for educational
purposes.
Edited by
Ian Hayes
With Contributions by
Bill Flinn
Roger Gimson
Steve King
Carroll Morgan
Ib Holm Sørensen
Bernard Sufrin
ii
Contents
I Tutorials 1
1 Small examples of specification using mathematics 3
Ian Hayes
1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.2 A symbol table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 File update . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.4 Sorting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.5 Solutions to exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2 Block-structured symbol table 13
Ian Hayes
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Symbol table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2.1 The state . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.2.2 Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.2.3 Errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.3 Block-structured symbol table . . . . . . . . . . . . . . . . . . . . . . . 18
2.3.1 The state . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.3.2 Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.3.3 Errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.4 Other approaches . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.5 Solutions to exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3 Telephone network 29
Carroll Morgan
3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2 The specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2.1 Call . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.2 HangUp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.3 Engaged . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.3 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.4 Solutions to exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.5 Supplementary exercises . . . . . . . . . . . . . . . . . . . . . . . . . . 37
v
vi CONTENTS
II Software engineering 39
4 Unix filing system 41
Carroll Morgan and Bernard Sufrin
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.2 Scope of the specification . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.3 The specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.3.1 Bytes and files . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.3.2 Reading and writing . . . . . . . . . . . . . . . . . . . . . . . . 44
4.3.3 File storage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.3.4 Reading and writing stored files – framing . . . . . . . . . . . . 48
4.3.5 Hiding and simplification . . . . . . . . . . . . . . . . . . . . . 50
4.3.6 Sequential access to files . . . . . . . . . . . . . . . . . . . . . . 50
4.3.7 Channel system . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.3.8 The access system . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.3.9 A file naming system . . . . . . . . . . . . . . . . . . . . . . . . 55
4.3.10 Pathnames and directories . . . . . . . . . . . . . . . . . . . . . 56
4.3.11 Directories are files . . . . . . . . . . . . . . . . . . . . . . . . . 57
4.3.12 The complete filing system . . . . . . . . . . . . . . . . . . . . 57
4.3.13 Honesty of definitions . . . . . . . . . . . . . . . . . . . . . . . 60
4.3.14 Observation renaming and schema composition . . . . . . . . . 61
4.3.15 Definition of error conditions . . . . . . . . . . . . . . . . . . . 63
4.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4.5 Appendix: differences from Unix . . . . . . . . . . . . . . . . . . . . . 67
4.5.1 File size . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.5.2 Directory size . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.5.3 Storage medium capacity . . . . . . . . . . . . . . . . . . . . . 68
4.5.4 Seek . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.5.5 Representation of numbers . . . . . . . . . . . . . . . . . . . . 69
5 CAVIAR 71
Bill Flinn and Ib Holm Sørensen
5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.2 The case study . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
5.3 Identification of the basic sets . . . . . . . . . . . . . . . . . . . . . . . 73
5.4 The subsystems of CAVIAR . . . . . . . . . . . . . . . . . . . . . . . . 73
5.5 Modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
5.6 Module: Resource User [T, R, U ] . . . . . . . . . . . . . . . . . . . . . 75
5.7 Specialisations of the resource–user system . . . . . . . . . . . . . . . . 79
5.7.1 Module: Exclusive Resource[T, R, U ] . . . . . . . . . . . . . . 79
5.7.2 Module: Sole Resource[T, R, U ] . . . . . . . . . . . . . . . . . 80
5.7.3 Module: Sole Exclusive Resource[T, R, U ] . . . . . . . . . . . 81
5.7.4 The specification library . . . . . . . . . . . . . . . . . . . . . . 81
5.8 Classification and instantiation . . . . . . . . . . . . . . . . . . . . . . 81
5.8.1 Some laws for CAVIAR . . . . . . . . . . . . . . . . . . . . . . 81
5.8.2 Matching systems with models . . . . . . . . . . . . . . . . . . 83
5.8.3 Module: Hotel Reservation . . . . . . . . . . . . . . . . . . . . 83
5.8.4 Module: Transport Reservation . . . . . . . . . . . . . . . . . . 84
5.9 The meeting attendance subsystem . . . . . . . . . . . . . . . . . . . . 85
5.9.1 Module: Resource Pool [T, X ] . . . . . . . . . . . . . . . . . . . 85
CONTENTS vii
5.9.2 Module: Meeting Visitor . . . . . . . . . . . . . . . . . . . . . . 86
5.10 The meeting resource subsystems . . . . . . . . . . . . . . . . . . . . . 87
5.10.1 Module: Diary System[T, X, IX ] . . . . . . . . . . . . . . . . . 87
5.10.2 Module: Conference Room Booking . . . . . . . . . . . . . . . 88
5.10.3 Module: Dining Room Booking . . . . . . . . . . . . . . . . . . 90
5.10.4 Module: Visitor Pool . . . . . . . . . . . . . . . . . . . . . . . 91
5.10.5 The construction process . . . . . . . . . . . . . . . . . . . . . 92
5.11 Module: CAVIAR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92
5.11.1 Combining subsystems to form the state . . . . . . . . . . . . . 93
5.11.2 Operations that involve meetings only . . . . . . . . . . . . . . 94
5.11.3 Operations that involve visitors only . . . . . . . . . . . . . . . 96
5.11.4 A general visitor removal operation . . . . . . . . . . . . . . . . 96
5.12 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
6 ICL Data Dictionary 99
Bernard Sufrin
6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
6.2 Overview of the Data Dictionary System . . . . . . . . . . . . . . . . . 100
6.3 Access control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
6.3.1 Abstract information structures of DDS . . . . . . . . . . . . . 101
6.4 DDS dynamics: Part 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
6.4.1 The state of a running DDS . . . . . . . . . . . . . . . . . . . . 106
6.4.2 The display command . . . . . . . . . . . . . . . . . . . . . . . 109
6.4.3 Setting the element context . . . . . . . . . . . . . . . . . . . . 109
6.5 Access-control information . . . . . . . . . . . . . . . . . . . . . . . . . 110
6.6 DDS dynamics: Part 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
6.6.1 Inserting elements . . . . . . . . . . . . . . . . . . . . . . . . . 113
6.6.2 Deleting elements . . . . . . . . . . . . . . . . . . . . . . . . . . 115
6.7 Prospects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
6.8 Appendix: potential simplifications . . . . . . . . . . . . . . . . . . . . 116
7 Flexitime specification 121
Ian Hayes
7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
7.2 State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
7.3 Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
8 Simple assembler 125
Ib Holm Sørensen and Bernard Sufrin
8.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
8.1.1 The structure of instructions . . . . . . . . . . . . . . . . . . . 126
8.2 Requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
8.2.1 Symbol definitions . . . . . . . . . . . . . . . . . . . . . . . . . 127
8.2.2 Symbolic operands . . . . . . . . . . . . . . . . . . . . . . . . . 128
8.2.3 Numeric operands . . . . . . . . . . . . . . . . . . . . . . . . . 128
8.2.4 Symbolic opcodes . . . . . . . . . . . . . . . . . . . . . . . . . 128
8.2.5 Operands of machine instructions . . . . . . . . . . . . . . . . 129
8.2.6 Opcode fields . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
8.2.7 Specification summary . . . . . . . . . . . . . . . . . . . . . . . 130
8.2.8 Consequences of the specification . . . . . . . . . . . . . . . . . 130
viii CONTENTS
8.2.9 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
8.3 High-level design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
8.3.1 Design of the first phase . . . . . . . . . . . . . . . . . . . . . . 133
8.3.2 Design of the second phase . . . . . . . . . . . . . . . . . . . . 133
8.3.3 Putting the phases together . . . . . . . . . . . . . . . . . . . . 134
8.3.4 Correctness of the design . . . . . . . . . . . . . . . . . . . . . 134
8.3.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136
III Distributed Computing 137
9 The role of mathematical specifications 139
Roger Gimson and Carroll Morgan
9.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
9.2 A first example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
9.3 The first compromises . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
9.4 A compromise avoided . . . . . . . . . . . . . . . . . . . . . . . . . . . 145
9.5 Modularity and composition of services . . . . . . . . . . . . . . . . . 147
9.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149
10 Authentication of usernames 151
Roger Gimson and Carroll Morgan
10.1 Nicknames and usernames . . . . . . . . . . . . . . . . . . . . . . . . . 151
10.2 Authentication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 151
10.3 Guest user . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152
11 Time service – user manual 153
Roger Gimson and Carroll Morgan
11.1 Time service operation . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
11.2 Error reports . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
11.3 Modula-2 interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
12 Reservation service – user manual 155
Roger Gimson and Carroll Morgan
12.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155
12.2 Reservation service operations . . . . . . . . . . . . . . . . . . . . . . . 157
12.3 Error reports . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160
12.4 Modula-2 interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
IV Transaction Processing 163
13 Application to industry 165
Ian Hayes
13.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
13.2 Uses of formal specification . . . . . . . . . . . . . . . . . . . . . . . . 167
13.3 The specification process . . . . . . . . . . . . . . . . . . . . . . . . . . 168
13.3.1 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
13.4 A sample specification . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
13.4.1 Exceptional conditions specification . . . . . . . . . . . . . . . 170
13.4.2 The state . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170
CONTENTS ix
13.4.3 The operations . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
13.4.4 Exception checking . . . . . . . . . . . . . . . . . . . . . . . . . 172
13.5 Questions raised . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173
13.5.1 Exceptional conditions . . . . . . . . . . . . . . . . . . . . . . . 173
13.5.2 Interval control . . . . . . . . . . . . . . . . . . . . . . . . . . . 175
13.5.3 Interaction between modules . . . . . . . . . . . . . . . . . . . 176
13.6 Problems with specification . . . . . . . . . . . . . . . . . . . . . . . . 176
13.6.1 Communication problems . . . . . . . . . . . . . . . . . . . . . 176
13.6.2 The right level of abstraction . . . . . . . . . . . . . . . . . . . 177
13.6.3 Technical problems . . . . . . . . . . . . . . . . . . . . . . . . . 177
13.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
13.8 Appendix: exceptional conditions manual . . . . . . . . . . . . . . . . 179
14 CICS restructure 183
Steve King
14.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183
14.2 The CICS program product . . . . . . . . . . . . . . . . . . . . . . . . 183
14.3 Early experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
14.4 The decision to use Z . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
14.5 Education and tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186
14.6 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187
14.6.1 Subjective results . . . . . . . . . . . . . . . . . . . . . . . . . . 187
14.6.2 Quantitative results . . . . . . . . . . . . . . . . . . . . . . . . 188
14.7 The Oxford–Hursley collaboration . . . . . . . . . . . . . . . . . . . . 190
14.8 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192
15 CICS API specification 193
Steve King
15.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193
15.2 Using Z to describe interfaces . . . . . . . . . . . . . . . . . . . . . . . 194
15.3 The CICS Application Programming Interface (API) . . . . . . . . . . 194
15.4 Reasons for specifying the API . . . . . . . . . . . . . . . . . . . . . . 196
15.5 How the specifications were written . . . . . . . . . . . . . . . . . . . . 197
15.6 Experiences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198
15.6.1 Communication problems . . . . . . . . . . . . . . . . . . . . . 198
15.6.2 The ‘right’ level of abstraction . . . . . . . . . . . . . . . . . . 198
15.6.3 Putting modules together . . . . . . . . . . . . . . . . . . . . . 199
15.6.4 Parallelism . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200
15.6.5 Distributed systems . . . . . . . . . . . . . . . . . . . . . . . . 200
15.7 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201
15.8 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202
16 CICS Temporary Storage 203
Ian Hayes
16.1 A single queue . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203
16.1.1 Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204
16.1.2 Errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207
16.2 Named queues . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208
16.3 A network of systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210
16.3.1 A note on the current implementation . . . . . . . . . . . . . . 211
x CONTENTS
17 CICS message system 213
Ian Hayes
17.1 Message output . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213
17.2 Multiple destinations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 214
17.3 Message input . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 214
17.4 Send and receive . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215
17.5 Combining input and output . . . . . . . . . . . . . . . . . . . . . . . 215
17.6 Logical names . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215
17.7 Multiple logical destinations . . . . . . . . . . . . . . . . . . . . . . . . 216
17.8 Domains of the operations . . . . . . . . . . . . . . . . . . . . . . . . . 217
V Appendices 219
A Glossary: Z mathematical notation 221
A.1 Definitions and declarations . . . . . . . . . . . . . . . . . . . . . . . . 221
A.2 Axiomatic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
A.3 Generic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
A.4 Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223
A.5 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
A.6 Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225
A.7 Binary relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226
A.8 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228
A.9 Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229
A.10 Sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229
A.11 Bags . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231
A.12 Generalised bags . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233
A.13 Free type definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234
B Glossary: Z schema notation 235
B.1 Schema definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 235
B.2 Schema operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 235
B.3 Operation schemas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 239
B.4 Operation schema operators . . . . . . . . . . . . . . . . . . . . . . . . 240
Index 249