Lectures on the Logic of Computer Programming
Zohar Manna · Society for Industrial and Applied Mathematics eBooks · 1980
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.