Linking unifying theories of program refinement

Hayes, Ian J., Dunne, Steve E. and Meinicke, Larissa A. (2013) Linking unifying theories of program refinement. Science of Computer Programming, 78 11: 2086-2107. doi:10.1016/j.scico.2012.07.010

Author Hayes, Ian J.
Dunne, Steve E.
Meinicke, Larissa A.
Title Linking unifying theories of program refinement
Journal name Science of Computer Programming   Check publisher's open access policy
ISSN 0167-6423
Publication date 2013-11-01
Year available 2013
Sub-type Article (original research)
DOI 10.1016/j.scico.2012.07.010
Open Access Status Not yet assessed
Volume 78
Issue 11
Start page 2086
End page 2107
Total pages 22
Place of publication Amsterdam , The Netherlands
Publisher Elsevier
Language eng
Abstract In this paper we consider three theories of programs and specifications at different levels of abstraction. The theories we focus on are: the basic Unifying Theories of Programming(UTP) model, which corresponds to the theories of VDM, B, and the refinement calculus; an extended theory that distinguishes abort from nontermination; and a further extension that introduces (abstract) time. We define UTP-style designs (or specifications) in each theory and show how program constructors, such as nondeterministic choice and sequential composition, can be expressed as single designs in each theory. To examine the relationships between the theories, we construct mappings in both directions between pairs of theories and show that the pairs of mappings form Galois connections. This shows that the simpler (more abstract) models are sub-theories of the more complex extensions. The mappings preserve the program structure and hence are homomorphisms. An important property of a Galois connection is that both mappings preserve refinement. The Galois connections between the models can be exploited to translate properties, including refinement laws, between theories. In addition, we show how to define an iteration in the extended model in terms of an iteration in the timed model.
Keyword Unifying theories of programming (UTP)
Real time refinement
Program termination
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: Official 2014 Collection
School of Information Technology and Electrical Engineering Publications
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 1 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 2 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Sun, 20 Oct 2013, 10:09:54 EST by System User on behalf of School of Information Technol and Elec Engineering