Abstract Implementations and Their Correctness Proofs

Publisher Website
Google Scholar
Abstract
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(. Applicative Programming; D 2 2 (Software Engineering( Tools and Techniques--structured programming; top-down programming, D 3.1 (Programming Languages) Formal Defimtlons and Theory--semantics; D.3.3 (Programming Lan- guages) Language Constructs--abstract data types, data types and structures; F.3.1 (Logics and Meanings of Programs) Specifying and Verifying and Reasoning about Programs--logics of programs; specificat:on techmques, F 3 2 )Logics and Meanings of Programs) Semantics of Programming Languages--algebraic approaches :o semantics

This publication has 12 references indexed in Scilit: