DATA REFINEMENT OF MIXED SPECIFICATIONS - A GENERALIZATION OF UNITY

Using predicate transformers as a basis, we give semantics and refinem ent rules for mixed specifications that allow UNITY style specificatio ns to be written as a combination of abstract program and temporal pro perties. From the point of view of the programmer, mixed specification s may be considered a generalization of the UNITY specification notati on to allow safety properties to be specified by abstract programs in addition to temporal properties. Alternatively, mixed specifications m ay be viewed as a generalization of the UNITY programming notation to allow arbitrary safety and progress properties in a generalized 'alway s section'. The UNITY substitution axiom is handled in a novel way by replacing it with a refinement rule. The predicate transformers founda tion allows known techniques for algorithmic and data-refinement for w eakest precondition based programming to be applied to both safety and progress properties. In this paper, we define the predicate transform er based specifications, specialize the refinement techniques to them, demonstrate soundness, and illustrate the approach with a substantial example.