Higher-Order UTP for a Theory of Methods

  • Frank Zeyda
  • Ana Cavalcanti
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7681)


Higher-order programming admits the view of programs as values and has been shown useful to give a semantics to object-oriented languages. In building a UTP theory for object-orientation, one faces four major challenges: consistency of the program model, redefinition of methods in subclasses, recursion and mutual recursion, and simplicity. In this paper, we discuss how the UTP treatment of higher-order programs impacts on these issues and propose solutions to emerging problems. Our solutions give rise to a novel UTP theory of methods.


object-orientation semantics recursion consistency 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Cardelli, L.: A Theory of Objects. Springer (1996)Google Scholar
  2. 2.
    Back, R.-J., Preoteasa, V.: Reasoning About Recursive Procedures with Parameters. In: Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding. ACM (August 2003)Google Scholar
  3. 3.
    Cavalcanti, A., Wellings, A., Woodcock, J.: The Safety-Critical Java Memory Model: A Formal Account. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 246–261. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  4. 4.
    Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Enhancing Modular OO Verification with Separation Logic. ACM SIGPLAN Not 43(1), 87–99 (2008)CrossRefGoogle Scholar
  5. 5.
    Harwood, W., Cavalcanti, A., Woodcock, J.: A Theory of Pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 141–155. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    He, J., Li, X., Liu, Z.: rCOS: A refinement calculus for object systems. Theoretical Computer Science 365(1-2), 109–142 (2006)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 7.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall (February 1998)Google Scholar
  8. 8.
    Kassios, I.T.: Decoupling in Object Orientation. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 43–58. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Naumann, D.: Predicate Transformer Semantics of an Oberon-Like Language. In: Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi, PROCOMET 1994, pp. 467–487 (1994)Google Scholar
  10. 10.
    Naumann, D.: Predicate transformers and higher-order programs. Theoretical Computer Science 150(1), 111–159 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHCrossRefGoogle Scholar
  12. 12.
    Nuka, G., Woodcock, J.: Mechanising a Unifying Theory. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 217–235. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying Theories in ProofPower-Z. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 123–140. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Santos, T., Cavalcanti, A., Sampaio, A.: Object-Orientation in the UTP. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 18–37. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Spivey, M.: The Consistency Theorem for Free Type Definitions in Z. Formal Aspects of Computing 8, 369–375 (1996)zbMATHCrossRefGoogle Scholar
  16. 16.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall (July 1996)Google Scholar
  17. 17.
    Zeyda, F.: A Theory of Methods: Validation of Laws. Technical report (July 2012),
  18. 18.
    Zeyda, F., Cavalcanti, A.: Mechanical reasoning about families of UTP theories. Science of Computer Programming 77(4), 444–479 (2012)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Frank Zeyda
    • 1
  • Ana Cavalcanti
    • 1
  1. 1.University of YorkYorkUK

Personalised recommendations