Program Correctness over Abstract Data Types, With Error State Semantics
John Vivian Tucker, Jeffery I. Zucker · Data Archiving and Networked Services (DANS) · 1988
Straight-Line Programs. Preliminaries: Signatures and Structures. The Programming Language. Assertions. Correctness Formulae. A Proof System Soundness. Predicates State Transformers The Weakest Precondition and Strongest Postcondition. Completeness of the Proof System. `While' Programs. Notation for Partial Functions. The Programming Language. Assertions. Correctness Formulae. A Proof System Soundness. Partial State Transformers The Weakest Precondition and Strongest Postcondition. Completeness of the Proof System. Appendix: Total Correctness for `While' Programs. Recursive Programs. The Programming Language. Assertions. Correctness Formulae. A Proof System Soundness. A Look Ahead. Inductive Computability of the Input-Output Relation. Completeness of the Proof System. Appendix: Total Correctness for Recursive Programs. Computability in an Abstract Setting. Induction Schemes. Some Important Properties. From Induction Schemes to `While' Programs. From `While' Programs to Induction Schemes. Course-of-Values Induction. From COV Induction Schemes to `While'-Array Programs. From `While'-Array Programs to COV Induction Schemes. More on Induction. The COV Inductively Definable Functions. A Survey of Computability in an Abstract Setting. A Generalized Church-Turing Thesis. Bibliography.