Unifying Theories of Objects

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.

• Type: Conference
• Year: 2007
• Where: IFM
• Authors: Michael Anthony Smith, Jeremy Gibbons
• Keywords: Core Object Calculus, Corresponding Utp Model, IFM 2007, UTP Model