AbstractThis paper formalizes 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.
Categories and Subject Descriptors: D.3 [Programming Languages]; D.3.1 [Programming Languages]: Formal Definitions and Theory
Additional Key Words and Phrases: programming logic, object-oriented programs, recursive object types, program correctness, axiomatic semantics, soundness
Selected references
- Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575-631, September 1993.
- Pierre America and Frank de Boer. Reasoning about dynamically evolving process structures. Formal Aspects of Computing, 6(3):269-316, 1994.
- Greg Nelson. Verifying reachability invariants of linked structures. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 38-47, Austin, Texas, January 1983.