Composition of Assumption-commitment Specifications in a Unity Style
(1994) Colloquium on Formal Approaches of Software Engineering, at the 5th TAPSOFT Conference — Location: ORSAY(France) (April.1993)
Files
pdfdocument.pdf
Restricted Access - Adobe PDF
- 1.33 MB
Details
- Authors
- Abstract
- The problem of composing assumption-commitment specifications arises in the hierarchical development of reactive or concurrent systems. Abadi and Lamport's composition principle has been proposed as a logic-independent solution to that problem. In this paper, we apply it to derive a parallel rule for UNITY-like assumption-commitment specifications. For that purpose, we first interpret UNITY formulas in Abadi and Lamport's compositional model. Then, the premises of the parallel rule are reduced to proof obligations that can be carried with rules inherited from the UNITY logic. The approach is illustrated by an example.
- Affiliations
Citations
Collette, P. (1994). Composition of Assumption-commitment Specifications in a Unity Style. Science of Computer Programming, 23(2-3), 107-125. https://doi.org/10.1016/0167-6423(94)00017-4 (Original work published 1994)