Abstract Implementations and Their Correctness Proofs
Cyrus F. Nourani · Journal of the ACM · 1983
Formal Implementations and their correctness proofs are stud~ed.Properties of initial algebras are used to structure proofs of correctness of implementations A new formulation of implementation is given incorporating parameter types Canonical term algebras are argued to be the natural choice of representation for both the abstract and the more concrete specifications as far as correctness proofs are concerned The "fine structure" of lmtlal algebras ts captured by the notion of signature of constructors This notion leads to simple sufficient conditions for obtaining mjective homomorphisms of algebras, a necessary step in algebraic correctness proofs Signature of constructors is also used in connection with the deductive properties of the equational theory of the specification to arrive at sufficient conditions for mject~wty of homomorphtsms of algebras modeling parametenzed specifications.A proof methodology is prescribed which is based on the general constructions of the paper and is demonstrated by a nontnvial example Categories and Subject Descriptors D I. 1 [Programming Techniques[.