Data refinement of predicate transformers (Q1177155)

Data refinement is the systematic substitution of one data type, given in a rather abstract formulation, for another, more concrete one in a program. This transformation, conceived to path the way for a mathematically guided and secure transition from abstract specification to concrete implementation, hinges upon the concept of predicate transformers introduced by Dijkstra. In this theoretical framework the extension of Dijkstra's guarded commands with constructs for specification settles the environment for the kind of data refinement in question. It is developed as a transformation on local blocks of a program and shown to yield an algorithmic refinement of the whole program. Methods for data refinement are presented and abstract data types are at hand to delineate its scope. At least a particular transformer is used to illustrated elaborately data refinement of a simple program.