On assertion-based encapsulation for object invariants and simulations

TY - JOUR

T1 - On assertion-based encapsulation for object invariants and simulations

AU - Naumann, David A.

PY - 2007/6

Y1 - 2007/6

N2 - 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.

AB - 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.

KW - Encapsulation and abstraction

KW - Object invariants

KW - Separation and alias control

UR - https://www.scopus.com/pages/publications/34250221169

UR - https://www.scopus.com/pages/publications/34250221169#tab=citedBy

U2 - 10.1007/s00165-006-0020-5

DO - 10.1007/s00165-006-0020-5

M3 - Article

SN - 0934-5043

VL - 19

SP - 205

EP - 224

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 2

ER -