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