Higher-Order UTP for a Theory of Methods
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.
Keywordsobject-orientation semantics recursion consistency
Unable to display preview. Download preview PDF.
- 1.Abadi, M., Cardelli, L.: A Theory of Objects. Springer (1996)Google Scholar
- 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
- 7.Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall (February 1998)Google Scholar
- 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
- 16.Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. International Series in Computer Science. Prentice Hall (July 1996)Google Scholar
- 17.Zeyda, F.: A Theory of Methods: Validation of Laws. Technical report (July 2012), http://www.cs.york.ac.uk/circus/hijac/publication.html