Data refinement of mixed specifications |
| |
Authors: | Beverly A Sanders |
| |
Affiliation: | (1) Department of Computer and Information Science and Engineering, University of Florida, Gainesville, FL 32611-6120, USA (e-mail: sanders@cise.ufl.edu) , US |
| |
Abstract: | Using predicate transformers as a basis, we give semantics and refinement rules for mixed specifications that allow UNITY
style specifications to be written as a combination of abstract program and temporal properties. From the point of view of
the programmer, 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 predicate
transformers foundation allows known techniques for algorithmic and data-refinement for weakest precondition based programming
to be applied to both safety and progress properties. In this paper, we define the predicate transformer based specifications,
specialize the refinement techniques to them, demonstrate soundness, and illustrate the approach with a substantial example.
Received: 1 April 1996 / 6 March 1997 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|