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 - http://www.scopus.com/inward/record.url?scp=34250221169&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34250221169&partnerID=8YFLogxK
U2 - 10.1007/s00165-006-0020-5
DO - 10.1007/s00165-006-0020-5
M3 - Article
AN - SCOPUS:34250221169
SN - 0934-5043
VL - 19
SP - 205
EP - 224
JO - Formal Aspects of Computing
JF - Formal Aspects of Computing
IS - 2
ER -