Linking Unifying Theories of Program refinement |
| |
| Authors: | Ian J Hayes Steve E Dunne Larissa A Meinicke |
| |
| Affiliation: | 1. School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, 4072, Australia;2. School of Computing, University of Teesside, Middlesbrough, TS1 3BA, UK |
| |
| 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. |
| |
| Keywords: | Unifying theories of programming (UTP) Real-time refinement Program termination |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
