Algebraically specified programming systems and Hoare's logic : (preprint)
Jan Aldert Bergstra, John Vivian Tucker · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1980
We describe a special set 9f program constructs for computing on data types defined by algebraic specifications using initial algebra semantics.And we provide an algebraically styled Hoare logic for proving algebraic statements about the partial correctness of programs in the resulting programming language.It is shown that given any computable data type A and any algebraica'l.lyasserted program {p}S{q} which is provable in a Hoare logic using computable intermediate assertions then there exists an algebraic specification, involving at most 6 hidden functions and 4 equations, which defines A and allows {p}S{q} to be provable in our algebraic Hoare logic using intermediate assertions formally provable from the axioms of the specification.