
1980 / iv + 49 pages / Softcover / ISBN: 9780898711646 / List Price $41.50 / SIAM/CBMS Member Price $29.05 / Order Code CB31
This monograph deals with aspects of the computer programming process that involve techniques derived from mathematical logic. The author focuses on proving that a given program produces the intended result whenever it halts, that a given program will eventually halt, that a given program is partially correct and terminates, and that a system of rewriting rules always halts. Also, the author describes the intermediate behavior of a given program, and discusses constructing a program to meet a given specification.
Contents
Partial correctness: Invariant method; Subgoal method; Subgoal method versus invariant method; Termination: Wellfounded ordering method; The multiset ordering; Total correctness; Intermittent method; Systematic program annotation; Range of Individual variables; Relation between variables; Control invariants; Debugging; Termination and runtime analysis; Synthesis of programs: The weakest precondition operator; Transformation rules; Simultaneousgoal principle; Conditionalformation principle; Recursionformulation principle; Generalization; Program modification; Comparison with structured programming; Termination of production systems: Examples: Associativity; Example: Distribution system; Differentiation system; Nested Multisets.
ISBN: 9780898711646