Recursive object types in a logic of object-oriented programs. (English) Zbl 0913.68025

Leino, K. Rustan M.

Nord. J. Comput. 5, No. 4, 330-360 (1998).

Summary: This paper formalize a small object-oriented programming notation. The notation features imperative commands where objects can be shared (aliased), and is rich enough to allow subtypes and recursive object types. The syntax, type checking rules, axiomatic semantics, and operational semantics of the notation are given. A soundness theorem showing the consistency between the axiomatic and operational semantics is stated and proved. A simple corollary of the soundness theorem demonstrates the soundness of the type system. Because of the way types, fields, and methods are declared, no extra effort is required to handle recursive object types.

MSC:

68N01	General topics in the theory of software
68T27	Logic in artificial intelligence

Keywords:

object-oriented programming