University of Sussex
Browse

File(s) not publicly available

Modular semantics and logics of classes

presentation
posted on 2023-06-08, 05:29 authored by Bernhard ReusBernhard Reus
The semantics of class-based languages can be defined in terms of objects only [1, 7, 8] 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 obtained by endowing the denotations of classes with an additional parameter that accounts for those classes added "later at linkage time." Local class definitions (inner classes) are possible but for dynamic class-loading one cannot do without higher-order store.

History

Publication status

  • Published

ISSN

0302-9743

Publisher

Springer, Berlin

Volume

2803

Pages

14.0

Presentation Type

  • paper

Event name

12th Annual Conference of the European-Association-for-Computer-Logic/8th Kurt Godel Colloquium/17th International Workshop on Computer Science Logic

Event location

Vienna, Austria

Event type

conference

ISBN

3-540-40801-0

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Editors

M Baatz, J Makowsky

Legacy Posted Date

2012-02-06

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC