|
Abstract : |
Data refinement is an important and widely used technique for program development. In this paper, we give predicate transformer based semantics and refinement rules for mixed specifications that allow specifications to be written as a combination of abstract program and temporal properties. Mixed specifications may be considered a generalization of the UNITY specification notation to allow safety properties to be specified by abstract programs in addition to temporal properties. Alternatively, mixed specifications may be viewed as a generalization of the UNITY programming notation to allow arbitrary safety and progress properties in a generalized `always section'. The UNITY substitution axiom is handled in a novel way by replacing it with a refinement rule. The derivation of a distributed mutual exclusion algorithm is given to illustrate the method on a non-trivial example. 1, |
