On the refinement of specifications 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 develop the basic proof theory of Hoare's logic for the partial correctness of while-programs whose underlying data types are defined by first-order axiomatic specifications.Our objective is to study the effects of refining data type specifications on the program correctness proofs they support.It :i.s shown that any finite selection of refinements is stable relative to a given asserted program, but that this stability is a strictly local property of families of specifications.