Lectures on the Logic of Computer Programming

Partial correctness: Invariant method Subgoal method Subgoal method versus invariant method Termination: Well-founded ordering method The multiset ordering Total correctness Intermittent method Systematic program annotation Range of Individual variables Relation between variables Control invariants Debugging Termination and run-time analysis Synthesis of programs: The weakest precondition operator Transformation rules Simultaneous-goal principle Conditional-formation principle Recursion-formulation principle Generalization Program modification Comparison with structured programming Termination of production systems: Examples: Associativity Example: Distribution system Differentiation system Nested Multisets.