Introduction 1
Part 1 ARM-a simple methodology 5
Chapter 1 ARM as a meta-method 7
1.1 Steps in ARM 7
1.2 Importance of abstraction step 10
Chapter 2 ARM leads to a 3-layer model of BPM 13
2.1 Why BPM today:the purpose 13
2.2 Abstraction 14
2.2.1 Physical objects 14
2.2.2 Mathematical objects 15
2.3 Mathematical system:the 3 layers 19
2.4 Correctness criteria and proof method 22
Part 2 OESPA:to combine program semantics with program syntax 27
Chapter 3 Assertions on programs 29
3.1 Formal treatment 29
3.2 Assertions and weakest preconditions 32
3.3 To remove ambiguity from programs 33
Chapter 4 OE:operation expressions 38
4.1 Operations on a memory location 39
4.1.1 Read and write operations 40
4.1.2 Semantic functions 44
4.1.3 Semantic predicates 46
4.2 Operation expressions 51
4.2.1 OE syntax in terms of BNF 51
4.2.2 Semantic axioms for OE 59
4.3 How to compute semantic function u( p) 66
4.4 Theorems provable from semantic axioms 77
Chapter 5 SP calculus 81
5.1 Reduction rules 82
5.2 SP-formulas for loops 88
5.2.1 Loop pn 88
5.2.2 Loop pb and pb′ 91
5.3 Complete specification 93
Chapter 6 Programming in OE by examples 96
6.1 8-queen problem 96
6.1.1 Abstraction and specification 96
6.1.2 Specification refinement 98
6.1.3 Programming in OE 107
6.1.4 Program verification 115
6.1.5 Complete OE of queen-all 121
6.2 Sorting an array into ascending order 122
6.2.1 Specification 122
6.2.2 Sorting program in C 124
6.2.3 Replacing val with swap 127
6.2.4 Quick-sorting in OE 130
6.2.5 Verifying q-sorting 132
6.3 N-lift problem:service sharing 137
6.3.1 From requirement to specification 137
6.3.2 Global control vs local determination 142
6.3.3 Atomic action and atomic request 144
6.3.4 To assemble actions at floor k in up direction 150
6.3.5 Complete OE for the lift 154
Part 3 Connecting OE with C 157
Chapter 7 Pointers， functions and structures on C 159
7.1 Semantic axioms on C pointers 159
7.2 Theorems about C pointers and examples 161
7.3 C functions:definition and call 171
7.4 Structures and union of C 175
Part 4 Parallel operation expressions(POE) 177
Chapter 8 Syntax and semantics of POE 179
8.1 Semantic consideration on POE 180
8.2 Semantics of solutions in different categories 183
8.2.1 Loose dependence:shared services 183
8.2.2 Simple dependence:shared resources 187
8.2.3 Simple cooperation:shared CPU time 189
8.2.4 Frangible cooperation:shared operands 190
8.2.5 Other problems involving parallelism 195
Chapter 9 5-philosopher problem 198
9.1 Fork management 198
9.2 Efficiency and fairness 202
9.2.1 Efficiency by “law” 202
9.2.2 Fairness 204
9.3 Shared variables as communication channels 207
References 212
Epilogue 213
