Unifying Theories of Undefinedness in UTP

  • Jim Woodcock
  • Victor Bandur
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7681)


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.


Unify Theory Classical Logic Function Symbol Partial Function Predicate Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Agerholm, S., Frost, J.: An Isabelle-based Theorem Prover for VDM-SL. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 1–16. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  2. 2.
    Bergmann, M.: An Introduction to Many-Valued and Fuzzy Logic: Semantics, Algebras and Derivation Systems. Cambridge University Press (2008)Google Scholar
  3. 3.
    Bergstra, J.A., Bethke, I., Rodenburg, P.: A propositional logic with 4 values: true, false, divergent and meaningless. Journal of Applied NonClassical Logics 5, 199–217 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Bochvar, D.A., Bergmann, M.: On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus. History and Philosophy of Logic 2(1), 87–112 (1981)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Goldsmith, M.: FDR2 user’s manual. Technical Report Version 2.82. Formal Systems (Europe) Ltd. (2005)Google Scholar
  6. 6.
    Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)zbMATHCrossRefGoogle Scholar
  7. 7.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Series in Computer Science. Prentice Hall (1998)Google Scholar
  8. 8.
    Larsen, P.G., Battle, N., Ferreira, M.A., Fitzgerald, J.S., Lausdahl, K., Verhoef, M.: The Overture initiative: integrating tools for VDM. ACM SIGSOFT Software Engineering Notes 35, 1–6 (2010)CrossRefGoogle Scholar
  9. 9.
    Rose, A.: A lattice-theoretic characterisation of three-valued logic. Journal of the London Mathematical Society 25, 255–259 (1950)zbMATHCrossRefGoogle Scholar
  10. 10.
    Saaltink, M.: The Z/EVES System. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–85. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  11. 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. 12.
    Woodcock, J., Freitas, L.: Linking VDM and Z. In: Hinchey, M. (ed.) ICECCS, pp. 143–152. IEEE Computer Society (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Jim Woodcock
    • 1
  • Victor Bandur
    • 1
  1. 1.The University of YorkUK

Personalised recommendations