Prespecification in data refinement

In data refinement, a concrete data type replaces an abstract data type used in the design of an algorithm or system (Gries and Prins, 1985; Hoare, 1972; Jones, 1980). 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 (Milner, 1980; Park, 1981), 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 Dijkstra's (1976). Operations (in general, nondeterministic) are represented by relations, and significant use is made of prespecification and postspecification (Hoare and He, Jifeng, 1987).