On assertion-based encapsulation for object invariants and simulations

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

Abstract

In object-oriented programming, reentrant method invocations and shared references make it difficult to achieve adequate encapsulation for sound modular reasoning. This tutorial paper surveys recent progress using auxiliary state (ghost fields) to describe and achieve encapsulation. It also compares this technique with encapsulation in the forms provided by separation logic. Encapsulation is assessed in terms of modular reasoning about invariants and simulations.

Original languageEnglish
Pages (from-to)205-224
Number of pages20
JournalFormal Aspects of Computing
Volume19
Issue number2
DOIs
StatePublished - Jun 2007

Keywords

  • Encapsulation and abstraction
  • Object invariants
  • Separation and alias control

Fingerprint

Dive into the research topics of 'On assertion-based encapsulation for object invariants and simulations'. Together they form a unique fingerprint.

Cite this