Modular Semantics and Logics of Classes

The semantics of class-based languages can be defined in terms of objects only [8, 7, 1] if classes are viewed as objects with a constructor method. One obtains a store in which method closures are held together with field values. Such a store is also called “higher-order” and does not come for free [13]. It is much harder to prove properties of such stores and as a consequence (soundness of) programming logics can become rather contrived (see [2]). A simpler semantics separates methods from the object store [4, 12]. But again, there is a drawback. Once the semantics of a package of classes is computed it is impossible to add other classes in a compositional way. Modular reasoning principles are therefore not obtainable either. In this paper we improve a simple class-based semantics to deal with extensions compositionally and derive modular reasoning principles for a logic of classes. The domain theoretic reasoning principle behind this is fixpoint induction. Modularity is obtai...

• Type: Conference
• Year: 2003
• Where: CSL
• Authors: Bernhard Reus
• Keywords: CSL 2003, Modular Reasoning Principles, Reasoning Principle, Semantics