Unifying Theories of Objects
Michael Anthony Smith and Jeremy Gibbons
Abstract
We present an approach to modelling Abadi–Cardelli-style object calculi as 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.
Details
| Book Title |
Integrated Formal Methods |
| Editor |
Jim Davies and Jeremy Gibbons |
| Pages |
599−618 |
| Publisher |
Springer−Verlag |
| Series |
Lecture Notes in Computer Science |
| Volume |
4591 |
| Year |
2007 |
Links
Related pages
|
People |
|
|
Projects |