Table of Contents

Part 1 Background in general algebra and OBJ: signatures; algebras; terms; variables; equations; rewriting and equational deduction - attributes of operations, denotational semantics for objects, the theorem of constants; importing modules; literature. Part 2 Stores, variables, values, and assignment: stores, variables, and values - OBJ's built-in inequality; assignment. Part 3 Composition and conditionals: sequential composition; conditionals; structural induction. Part 4 Proving programme correctness: example - absolute value; sample - computing the maximum of two values. Part 5 Iteration: invariants - example - greatest common divisor; termination. Part 6 Arrays: some simple examples; exercises; specifications and proofs. Part 7 Procedures: non-recursive procedures - procedures with no parameters, procedures with varparameters, procedures with expparameters; recursive procedures - procedures with no parameters, procedures with varparameters. Part 8 Some comparison with other approaches; summary of the semantics; first order logic and induction; order sorted algebra; OBJ3 syntax; instructors' guide.

About the Author

Grant Malcolm is Chancellor of University of York and Chairman of NHS England.