Predicate transformation semantics is the best specification method for the development of correct and well-structured computer programs. This book is a complete account of the predicate transformation calculus semantics of sequential programs, including repetitions, recursive procedures, computational induction, and unbounded nondeterminacy. The author develops their theory to a greater depth than has been achieved before, and describes it in a way that makes it readily compatible with programming methodology. He gives proofs of the programming rules for partial and total correctness of repetitions and recursive procedures, supplies new rules for proving incorrectness, and a stronger rule for proving that two programs satisfy the same specifications. Finally, the semantics are extended so that non-terminating programs can be specified as well.
Author(s): Wim H. Hesselink
Series: Cambridge Tracts in Theoretical Computer Science 27
Publisher: Cambridge University Press
Year: 1992
Language: English
Pages: 238
Cover......Page 1
Frontmatter......Page 2
Contents......Page 6
Preface......Page 12
List of symbols......Page 14
0.1 Semantics of imperative sequential programs......Page 16
0.2 Predicate-transformation semantics......Page 18
0.3 Program transformations......Page 19
0.4 Overview......Page 20
0.5 The chapters in detail......Page 21
0.6 Notation......Page 23
0.7 Design decisions......Page 25
1 - Weakest preconditions......Page 27
1.1 Predicates and predicate transformers......Page 28
1.2 Weakest preconditions......Page 30
1.3 Guards, assertions, termination and totality......Page 32
1.4 Composition and nondeterminate choice......Page 34
1.5 Intermezzo on the conditional combination......Page 35
1.6 Program variables, state functions and localized relations......Page 36
1.7 The assignment......Page 38
1.8 Deterministic choice......Page 41
1.9 Appendix on predicate calculus......Page 42
1.10 Exercises......Page 44
2.1 Specification with Hoare triples......Page 47
2.2 Proofs by annotation......Page 50
2.3 Specification and invocation of procedures......Page 52
2.4 Correctness of recursive declarations......Page 55
2.5 An abstract version of recursive procedures......Page 57
2.6 Homomorphisms and simple commands......Page 59
2.7 Induction rules......Page 60
2.8 The repetition......Page 63
2.9 Exercises......Page 67
3.1 Conjunctivity properties of predicate transformers......Page 73
3.2 Two laws......Page 74
3.3 Some important implications......Page 75
3.4 Guards, assertions and assignments......Page 77
3.5 The termination law and repetitions......Page 78
3.6 Exercises......Page 79
4.1 Complete lattices and predicate transformers......Page 81
4.2 Fixpoints in complete lattices......Page 85
4.3 A syntax for commands with unbounded choice......Page 86
4.4 The interpretation of recursion......Page 88
4.5 Healthiness laws: the universal conjunctivity of wlp......Page 90
4.6 The termination law......Page 91
4.7 The syntactic algebra......Page 94
4.8 The semantic homomorphisms......Page 95
4.9 The induction rules......Page 97
4.10 Conclusion......Page 98
4.11 Exercises......Page 99
5.1 Refinement and relative refinement......Page 102
5.2 Refinement of procedures......Page 104
5.3 Insertion of guards, and calculus......Page 105
5.4 The commutation problem......Page 106
5.5 Strongest postconditions......Page 108
5.6 Termination and well-founded triples......Page 109
5.7 Two new recursion theorems......Page 112
5.8 Exercises......Page 114
6 - Relational semantics......Page 116
6.1 Relations as an alternative specification method......Page 117
6.2 The relational view of guards, composition and choice......Page 118
6.3 Termination and totality......Page 120
6.4 From commands to relations......Page 121
6.5 Exercises......Page 122
7.1 Determinacy......Page 124
7.2 Disjunctivity properties......Page 126
7.3 Determinacy and disjunctivity......Page 127
7.5 Finite nondeterminacy......Page 128
7.6 Exercises......Page 130
8.1 Syntactic reflexion of semantic properties......Page 131
8.2 Membership of the syntactic reflexion......Page 135
8.3 [GREEK CAPITAL LETTER PSI]-disjunctivity......Page 137
8.4 Totality, disjunctivity and finite nondeterminacy......Page 140
8.5 Exercises......Page 144
9 - Operational semantics of recursion......Page 145
9.2 The proof of the faithful interpreter......Page 146
9.3 The operational interpretation of tail recursion......Page 150
9.4 General operational semantics......Page 156
9.5 Exercises......Page 157
10.1 Substitutions......Page 158
10.3 Procedure abstraction is allowed......Page 159
10.4 A classical example......Page 161
10.5 Exercises......Page 162
11 - Induction and semantic equality......Page 164
11.2 The set Lia......Page 165
11.3 The strong congruence......Page 166
11.5 An application: the storage of a parameter......Page 168
11.6 Compositionality of the strong congruence......Page 170
11.7 The necessity of Lia......Page 171
11.8 Exercises......Page 172
12.1 Admissible preorders......Page 175
12.3 Construction of the strong congruence......Page 176
12.4 Commutation up to refinement......Page 178
12.5 Exercises......Page 181
13.1 Intermezzo: an extension of the theorem of Knaster--Tarski......Page 182
13.2 Unfolding......Page 184
13.3 The construction of the strong preorder......Page 186
13.4 The abortive interpretations......Page 188
13.5 Inf--safety......Page 189
13.7 Linear approximation......Page 191
13.8 The set Lia and sequential composition......Page 193
13.9 Exercises......Page 194
14 - Temporal operators......Page 195
14.1 Stability and the function `always'......Page 196
14.2 Termination and unfolding......Page 199
14.3 The temporal predicate transformer for always......Page 200
14.4 Temporal functions for eventually......Page 202
14.5 Possible termination......Page 204
14.6 Exercises......Page 207
15 - Predicative fairness......Page 208
15.1 Starvation of predicates......Page 209
15.2 An abstract syntax and weak fairness......Page 211
15.3 A general fairness definition......Page 212
15.4 Examples......Page 215
15.5 The operational meaning......Page 218
15.6 A proposal for strong fairness......Page 221
16 - Solutions of exercises......Page 223
References......Page 232
Index of concepts and identifiers......Page 236
