Preface ......................................................... v
Contributors ................................................... xv
Part I Models and correctness ................................... 1
A. Concurrency and interaction .................................. 3
1. Wanted: a compositional approach to concurrency ........... 5
C.B.Jones
1.1. Compositionality ........................................ 5
1.2. The essence of concurrency is interference .............. 7
1.3. Reasoning about interference ............................ 8
1.4. Some problems with assumption/commitment reasoning ..... 10
1.5. The role of ghost variables ............................ 11
1.6. Granularity concerns ................................... 12
1.7. Atomicity as an abstraction, and its refinement ........ 12
1.8. Conclusion ............................................. 13
References .................................................. 13
2. Enforcing behavior with contracts ........................ 17
Ralph-Johan Back and Joakim von Wright
2.1. Introduction ........................................... 17
2.2. Contracts .............................................. 19
2.3. Achieving goals with contracts ......................... 27
2.4. Enforcing behavioral properties ........................ 33
2.5. Analyzing behavior of action systems ................... 39
2.6. Verifying enforcement .................................. 43
2.7. Conclusions and related work ........................... 50
References .................................................. 51
В. Logical approaches to asynchrony ............................ 53
3. Asynchronous progress .................................... 57
Ernie Cohen
3.1. Introduction ........................................... 57
3.2. Programs ............................................... 59
3.3. Achievement ............................................ 61
3.4. Decoupling ............................................. 63
3.5. Example - Loosely-coupled programs ..................... 64
3.6. Asynchronous safety .................................... 65
3.7. Caveats ................................................ 66
3.8. Conclusions ............................................ 67
3.9. Acknowledgements ....................................... 68
References .................................................. 68
4. A reduction theorem for concurrent object-oriented
programs ................................................. 69
Jayadev Misra
4.1. Introduction ........................................... 69
4.2. The Seuss programming notation ......................... 71
4.3. A model of Seuss programs .............................. 78
4.4. Restrictions on programs ............................... 80
4.5. Compatibility .......................................... 83
4.6. Proof of the reduction theorem ......................... 87
4.7. Concluding remarks ..................................... 91
References .................................................. 91
С. Systems and real time ....................................... 93
5. Abstractions from time ................................... 95
Manfred Broy
5.1. Introduction ........................................... 95
5.2. Streams ................................................ 96
5.3. Components as functions on streams ..................... 99
5.4. Time abstraction ...................................... 100
5.5. Conclusions ........................................... 104
References ................................................. 106
6. A predicative semantics for real-time refinement ........ 109
Ian Hayes
6.1. Background ............................................ 109
6.2. Language and semantics ................................ 1ll
6.3. An example ............................................ 124
6.4. Repetitions ........................................... 126
6.5. Timing-constraint analysis ............................ 129
6.6. Conclusions ........................................... 131
References ................................................. 132
D. Specifying complex behaviour ............................... 135
7. Aspects of system description ........................... 137
Michael Jackson
7.1. Introduction .......................................... 137
7.2. Symbol manipulation ................................... 138
7.3. The Machine and the World ............................. 140
7.4. Describing the World .................................. 144
7.5. Descriptions and models ............................... 147
7.6. Problem decomposition and description structures ...... 153
7.7. The scope of software development ..................... 156
7.8. Acknowledgements ...................................... 158
References ................................................. 159
8. Modelling architectures for dynamic systems ............. 161
Peter Henderson
8.1. Introduction .......................................... 161
8.2. Models of dynamic systems ............................. 163
8.3. Architectures for reuse ............................... 168
8.4. Conclusions ........................................... 172
References ................................................. 173
9. "What is a method?" - an essay on some aspects of
domain engineering ...................................... 175
Dines Bj0rner
9.1. Introduction .......................................... 175
9.2. Method and Methodology ................................ 178
9.3. Domain Perspectives and Facets ........................ 181
9.4. Conclusion ............................................ 199
References ................................................. 201
Part II Programming techniques ................................ 205
E. Object orientation ......................................... 207
10.Object-oriented programming and software
development - a critical assessment ..................... 211
Manfred Broy
10.1.Introduction .......................................... 211
10.2.Object orientation - its claims and its
limitations ........................................... 212
10.3.Object-oriented programming - a critique .............. 214
10.4.Object-oriented analysis and design - a critique ...... 219
10.5.Concluding remarks .................................... 220
References ................................................. 220
11.A trace model for pointers and objects .................. 223
C.A.R.Hoare and He Jifeng
11.1.Introduction: the graph model ......................... 223
11.2.The trace model ....................................... 229
11.3.Applications .......................................... 236
11.4.Conclusion ............................................ 242
References ................................................. 243
12.Object models as heap invariants ........................ 247
Daniel Jackson
12.1.Snapshots and object models ........................... 249
12.2.Object-model examples ................................. 250
12.3.A relational logic .................................... 253
12.4.Diagrams to logic ..................................... 255
12.5.Textual annotations ................................... 258
12.6.Discussion ............................................ 260
References ................................................. 266
13.Abstraction dependencies ................................ 269
K.Rustan, M.Leino and Greg Nelson
13.1.Introduction .......................................... 269
13.2.On the need for data abstraction ...................... 270
13.3.Validity as an abstract variable ...................... 272
13.4.Definition of notation ................................ 273
13.5.Example: Readers ...................................... 278
13.6.Related work .......................................... 285
13.7.Conclusions ........................................... 286
References ................................................. 287
F. Type theory ................................................ 291
14.Type systems ............................................ 293
Benjamin C.Pierce
14.1.Type systems in computer science ...................... 293
14.2.What are type systems good for? ....................... 295
14.3.History ............................................... 300
References ................................................. 301
15.What do types mean? - From intrinsic to extrinsic
semantics ............................................... 309
John С.Reynolds
15.1.Syntax and typing rules ............................... 310
15.2.An intrinsic semantics ................................ 312
15.3.An untyped semantics .................................. 314
15.4.Logical relations ..................................... 315
15.5.Bracketing ............................................ 321
15.6.An extrinsic PER semantics ............................ 323
15.7.Further work and future directions .................... 326
15.8.Acknowledgements ...................................... 326
References ................................................. 326
Part III Applications and automated theories .................. 329
G. Putting theories into practice by automation ............... 331
16.Automated verification using deduction,
exploration, and abstraction ............................ 333
Natarajan Shankar
16.1.Models of computation ................................. 335
16.2.Logics of program behavior ............................ 337
16.3.Verification techniques ............................... 339
16.4.Abstractions of programs and properties ............... 341
16.5.Verification methodology .............................. 347
16.6.Conclusions ........................................... 348
References ................................................. 348
17.An experiment in feature engineering .................... 353
Pamela Zave
17.1.Feature-oriented specification ........................ 353
17.2.The challenge of feature engineering .................. 354
17.3.A feature-oriented specification technique ............ 356
17.4.A modest method for feature engineering ............... 359
17.5.An application of the method .......................... 370
17.6.Evaluation of the method .............................. 375
17.7.Acknowledgments ....................................... 376
References ................................................. 376
H. Programming circuits ....................................... 379
18.High-level circuit design ............................... 381
Eric C.R.Hehner, Theodore S.Norvell,
and Richard Paige
18.1.Introduction .......................................... 381
18.2.Diagrams .............................................. 383
18.3.Time .................................................. 384
18.4.Flip-flops ............................................ 385
18.5.Edge-triggering ....................................... 387
18.6.Memory ................................................ 389
18.7.Merge ................................................. 390
18.8.Imperative circuits ................................... 392
18.9.Functional circuits ................................... 401
18.10.Hybrid circuits ...................................... 405
18.11.Performance .......................................... 406
18.12.Correctness .......................................... 407
18.13.Synchronous and asynchronous circuits ................ 410
18.14.Conclusions .......................................... 410
I. Security and keeping secrets ............................... 413
19.Power analysis: attacks and countermeasures ............. 415
Suresh Chari, Charanjit S.Jutla,
Josyula R.Rao, and Pankaj Rohatgi
19.1.Introduction .......................................... 415
19.2.Power analysis of a Twofish implementation ............ 419
19.3.Power model and attacks ............................... 425
19.4.Countermeasures to power analysis ..................... 428
19.5.Conclusions ........................................... 436
19.6.Acknowledgments ....................................... 436
References ................................................. 436
20.A probabilistic approach to information hiding .......... 441
Annabelle Mclver and Carroll Morgan
20.1.Introduction .......................................... 441
20.2.Background: multi-level security and
information flow ...................................... 442
20.3.Classical information theory, and program
refinement ............................................ 443
20.4.Information flow in imperative programs ............... 448
20.5.Example: The secure file store ........................ 454
20.6.The Refinement Paradox ................................ 457
References ................................................. 460
Index ......................................................... 461
|
