Unifying theories of objects

Conference item

We present an approach to modelling Abadi-Cardelli-style object calculi as Unifying Theories of Programming (UTP) designs. Here we provide a core object calculus with an operational small-step evaluation rule semantics, and a corresponding UTP model with a denotational relational predicate semantics. For clarity, the UTP model is defined in terms of an operand stack, which is used to store the results of subprograms. Models of a less operational nature are briefly discussed. The consistency of the UTP model is demonstrated by a structural induction proof over the operations of the core object calculus. Overall, our UTP model is intended to provide facilities for encoding both object-based and class-based languages. © Springer-Verlag Berlin Heidelberg 2007.

Authors: Smith, M; Gibbons, J

• Publication status: Published
• Host title: Integrated Formal Methods, Proceedings
• Volume: 4591
• Pages: 599-618
• Publication date: 2007-01-01
• EISSN: 1611-3349
• ISSN: 0302-9743
• ISBN: 9783540732099