Unifying Theories of Undefinedness in UTP
In previous work, based on an original idea due to Saaltink, we proposed a unifying theory of undefined expressions in logics used for formally specifying software systems. In our current paper, we instantiate these ideas in Hoare and He’s Unifying Theories of Programming, with each different treatment of undefinedness formalized as a UTP theory. In this setting, we show how to use classical logic to prove facts in a monotonic partial logic with guards, and we describe the guards for several different UTP theories. We show how classical logic can be used to prove semi-classical facts. We apply these ideas to the COMPASS Modelling Language (CML), which is an integration of VDM and CSP in the Circus tradition. We link CML, which uses McCarthy’s left-to-right expression evaluation, and to VDM, which uses Jones’s three-valued Logic of Partial Functions.
KeywordsUnify Theory Classical Logic Function Symbol Partial Function Predicate Symbol
Unable to display preview. Download preview PDF.
- 2.Bergmann, M.: An Introduction to Many-Valued and Fuzzy Logic: Semantics, Algebras and Derivation Systems. Cambridge University Press (2008)Google Scholar
- 5.Goldsmith, M.: FDR2 user’s manual. Technical Report Version 2.82. Formal Systems (Europe) Ltd. (2005)Google Scholar
- 7.Hoare, C.A.R., He, J.: Unifying Theories of Programming. Series in Computer Science. Prentice Hall (1998)Google Scholar
- 11.Woodcock, J., Saaltink, M., Freitas, L.: Unifying theories of undefinedness. In: Summer School Marktoberdorf 2008: Engineering Methods and Tools for Software Safety and Security. NATO ASI Series F. IOS Press, Amsterdam (2009)Google Scholar
- 12.Woodcock, J., Freitas, L.: Linking VDM and Z. In: Hinchey, M. (ed.) ICECCS, pp. 143–152. IEEE Computer Society (2008)Google Scholar