Prespecification in data refinement (Q578901)

In data refinement, a concrete data type replaces an abstract data type used in the design of an algorithm or system. We present two methods for calculating the weakest specification of each operation on a concrete data type from the specification of the corresponding abstract operation, together with a single simulation relation, which specifies the correspondence between the two types. The methods are proved sound and (jointly) complete for a nondeterministic procedural programming language slightly more powerful than \textit{E. W. Dijkstra}'s [A discipline of programming (Englewood Cliffs 1976; Zbl 0368.68005)]. Operations (in general, nondeterministic) are represented by relations, and significant use is made of prespecification and postspecification [\textit{C. A. R. Hoare} and \textit{J. He}, Ann. Soc. Math. Polon., Ser. IV, Fundam. Inf. 9, 51-84 (1986; Zbl 0603.68009)].