More Web Proxy on the site http://driver.im/

editorial

Open access

On assertion-based encapsulation for object invariants and simulations

Author:

David A. NaumannAuthors Info & Claims

Formal Aspects of Computing, Volume 19, Issue 2

Pages 205 - 224

https://doi.org/10.1007/s00165-006-0020-5

Published: 01 June 2007 Publication History

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.

References

References

[1]

Aldrich J, Chambers C (2004) Ownership domains: separating aliasing policy from mechanism. In: European conference on object-oriented programming (ECOOP), pp 1–25

[2]

Apt KR and Olderog E-R Verification of sequential and concurrent Programs 1997 2 Berlin Heidelberg New York Springer

Digital Library

[3]

Biering B, Birkedal L, Torp-Smith N (2005) BI hyperdoctrines and higher-order separation logic. In: European symposium on programming (ESOP), vol. 3444 of LNCS, pp 233–247

[4]

Bornat R, Calcagno C, O’Hearn PW, Parkinson MJ (2005) Permission accounting in separation logic. In: ACM symposium on principles of programming languages (POPL), pp 259–270

[5]

Barnett M, DeLine R, Fähndrich M, Leino KRM, and Schulte W Verification of object-oriented programs with invariants J Object Technol 2004 3 6 27 Special issue: ECOOP 2003 workshop on formal techniques for Java-like Programs

[6]

Boyapati C, Lee R, Rinard M (2002) Ownership types for safe programming: preventing data races and deadlocks. In: Object-oriented programming, systems, languages, and applications (OOPSLA), pp 211–230

[7]

Boyapati C, Liskov B, Shrira L (2003) Ownership types for object encapsulation. In: ACM symposium on principles of programming languages (POPL), pp 213–223

[8]

Barnett M, Leino KRM, Schulte W (2005) The Spec# programming system: an overview. In: Barthe G, Burdy L, Huisman M, Lanet JL, Muntean T (eds) Construction and analysis of safe, secure, and interoperable smart devices, international workshop (CASSIS 2004), revised selected papers, Vol. 3362, of LNCS, pp 49–69

[9]

Banerjee A, Naumann DA (2002) Representation independence, confinement and access control. In: ACM symposium on principles of programming languages (POPL), pp 166–177

[10]

Barnett M, Naumann DA (2004) Friends need a bit more: maintaining invariants over shared state. In: Kozen D, Shankland C, (eds) Mathematics of program construction, Vol. 3125 of LNCS, pp 54–84

[11]

Banerjee A and Naumann DA Ownership confinement ensures representation independence for object-oriented programs J ACM 2005 52 6 894-960 Extended version of [BN02]

Digital Library

[12]

Banerjee A, Naumann DA (2005) State based ownership, reentrance, and encapsulation. In: European conference on object-oriented programming (ECOOP), pp 387–411

[13]

Barnett M, Naumann DA, Schulte W, Sun Q 99.44 pure: useful abstractions in specifications. In: ECOOP workshop on formal techniques for Java-like programs (FTfJP), 2004. Technical Report NIII-R0426, University of Nijmegen

[14]

Barnett M, Naumann DA, Schulte W, Sun Q (2006) Allowing state changes in specifications. In: International conference on emerging trends in information and communication security (ETRICS), Vol. 3995 of LNCS, Müller G, (ed) pp 321–336. Springer, Berlin Heidelberg New York Extended version of [BNSS04]

[15]

Bierman GM, Parkinson MJ (2005) Separation logic and abstraction. In: ACM symposium on principles of programming languages (POPL), pp. 247–258

[16]

Borba PHM, Sampaio ACA, Cornélio ML (2003) A refinement algebra for object-oriented programming. In: Cardelli L (ed) European conference on object-oriented programming (ECOOP), Vol. 2743 in LNCS, pp 457–482

[17]

Borba PHM, Sampaio A, Cavalcanti A, and Cornélio M Algebraic reasoning for object-oriented programming Sci Comput Program 2004 52 1–3 53-100

Digital Library

[18]

Birkedal L, Torp-Smith N (2005) Higher order separation logic and abstraction (submitted)

[19]

Birkedal L, Torp-Smith N, Yang H (2005) Semantics of separation-logic typing and higher-order frame rules. In: IEEE symposium on logic in computer science (LICS), pp 260–269

[20]

Clarke D (2001) Object ownership and containment. Dissertation, Computer Science and Engineering, University of New South Wales

[21]

Cavalcanti ALC, Naumann DA (2002) Forward simulation for data refinement of classes. In: Eriksson L, Lindsay PA (eds) Formal Methods Europe, Vol. 2391 of LNCS, pp 471–490

[22]

Clarke DG, Noble J, Potter JM (2001) Simple ownership types for object containment. In: Knudsen JL (ed) ECOOP 2001—object oriented programming, pp 53–76

[23]

Calcagno C, O’Hearn PW, and Bornat R Program logic and equivalence in the presence of garbage collection Theoret Comput Sci 2003 298 3 557-581

Digital Library

[24]

de Boer FS, Pierik C (2002) Computer-aided specification and verification of annotated object-oriented programs. In: Jacobs B, Rensink A (eds) Formal methods for open object-based distributed systems, pp 163–177

[25]

DeLine R, Fähndrich M (2001) Enforcing high-level protocols in low-level software. In: ACM Conference on Programing Languages on Design and implementation (PLDI), pp 59–69

[26]

Detlefs DL, Leino KRM, Nelson G (1998) Wrestling with rep exposure. Research 156, DEC Systems Research Center

[27]

de Roever W-P, Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. Cambridge University Press

[28]

Gamma E, Helm R, Johnson R, Vlissides J (1995) Design patterns: elements of reusable object-oriented software. Addison-Wesley

[29]

Gries D Broy M Data refinement and the tranform Program design calculi. International Summer School at Marktoberdorf 1993 Berlin Heidelberg New York Springer

[30]

Hoare CAR Proofs of correctness of data representations Acta Inf 1972 1 271-281

Digital Library

[31]

Hogg J (1991) Islands: aliasing protection in object-oriented languages. In: OOPSLA ’91 conference proceedings, Vol. 26(11) of SIGPLAN, ACM

[32]

Jacobs B, Kiniry J, Warnier M (2003) Java program verification challenges. In: de Boer F, Bonsangue M, Graf S, de Roever W-P (eds) Formal methods for components and objects (FMCO 2002), Vol. 2852 of LNCS, pp 202–219

[33]

Jacobs B, Leino KRM, Schulte W (2004) Multithreaded object-oriented programs with invariants. In: SAVCBS

[34]

Jones CB Accomodating interference in the formal design of concurrent object-based programs Formal Methods Syst Des 1996 8 2 105-122

Digital Library

[35]

Kassios IT (2006) Dynamic framing: Support for framing, dependencies and sharing without restriction: Formal Methods, vol 4085 in LNCS, pp 268–283

[36]

Kassios IT (2006) A theory of object oriented refinement. PhD dissertation, University of Toronto

[37]

Leavens GT, Cheon Y, Clifton C, Ruby C, and Cok DR de Boer FS, Bonsangue MM Grafs, and de Roever WP How the design of JML accommodates both runtime assertion checking and formal verification Formal Methods for Components and Objects (FMCO 2002) 2003 Berlin Heidelberg New York Springer 262-284 Vol. 2852 of LNCS

[38]

Liskov B and Guttag J Abstraction and specification in program development 1986 Cambridge MIT Press

Digital Library

[39]

Leino KRM, Müller P (2004) Object invariants in dynamic contexts. In: European conference on object-oriented programming (ECOOP), pp 491–516

[40]

Leino KRM, Müller P (2005) Modular verification of static class invariants. In: Proceedings, formal methods, Vol. 3582 of LNCS, pp 26–42

[41]

Leino KRM, Poetzsch-Heffter A, Zhou Y (2002) Using data groups to specify and check side effects. In: ACM Conference on Programming Language Design and Implementation (PLDI), pp 246–257

[42]

Lynch N and Vaandrager F Forward and backward simulations part I: untimed systems Inf Comput 1995 121 2 214-233

Digital Library

[43]

Liskov BH and Wing JM A behavioral notion of subtyping ACM Trans Program Lang Syst 1994 16 6 254-280

Digital Library

[44]

Meyer B Object-oriented software construction 1997 2 New York Prentice Hall

Digital Library

[45]

Milner R (1971) An algebraic definition of simulation between programs. In: Proceedings of 2nd International Joint Conference on Artificial Intelligence, pp 481–489

[46]

Mitchell JC (1986) Representation independence and data abstraction. In: ACM symposium on principles of programming languages (POPL), pp 263–276

[47]

Müller P, Poetzsch-Heffter A, Leavens GT (2004) Modular invariants for layered object structures. Technical Report 424, Department of Computer Science, ETH Zurich

[48]

Mijajlovic I, Torp-Smith N, O’Hearn PW (2004) Refinement and separation contexts. In: Foundations of Software Technology and Theoretical Computer Science (FST&TCS)

[49]

Müller P Modular specification and verification of object-oriented programs 2002 Berlin Heidelberg New York Springer Vol. 2262 of LNCS

[50]

Mijajlović I, Yang H (2005) Data refinement with low-level pointer operations. In: Asian symposium on programming languages and systems (APLAS), pp 19–36

[51]

Naumann DA (2001) Ideal models for pointwise relational and state-free imperative programming. In: Sondergaard H (ed) ACM international conference on principles and practice of declarative programming, pp 4–15

[52]

Naumann DA (2001) Patterns and lax lambda laws for relational and imperative programming. Technical Report 2001–2, Computer Science, Stevens Institute of Technology

[53]

Naumann DA Soundness of data refinement for a higher order imperative language Theoret Comput Sci 2002 278 1–2 271-301

Digital Library

[54]

Naumann DA (2005) Assertion-based encapsulation, object invariants and simulations. In: de Boer FS, Bonsangue MM, Graf S, de Roever WP (eds) Post-proceedings, formal methods for components and objects (FMCO 2004), Vol. 3657 of LNCS, pp 251–273

[55]

Naumann DA (2005) Observational purity and encapsulation. In: Fundamental aspects of software engineering (FASE), pp 190–204. Best Software Science Paper by the European Association of Software Sciences and Technology at the European Joint Conferences on Theory and Practice of Software (ETAPS)

[56]

Naumann DA (2006) From coupling relations to mated invariants for secure information flow. In: European symposium on research in computer security (ESORICS), Vol. 4189 in LNCS, pp 279–296

[57]

Naumann DA (2006) Observational purity and encapsulation. Theoret Comput Sci (to appear) Extended version of [Nau05b]

[58]

Naumann DA, Barnett M (2004) Towards imperative modules: Reasoning about invariants and sharing of mutable state (extended abstract). In: IEEE symposium on logic in computer science (LICS), pp 313–323

[59]

Naumann DA and Barnett M Towards imperative modules: reasoning about invariants and sharing of mutable state Theoret Comput Sci 2006 365 143-168 Extended version of [NB04]

Digital Library

[60]

O’Hearn PW (2005) Scalable specification and reasoning: technical challenges for program logic. In: Meyer B, Woodcock JCP (eds) Verified software: theories, tools, and experiments (VSTTE), Post-proceedings, (to appear)

[61]

O’Hearn PW and Tennent RD Parametricity and local variables J ACM 1995 42 3 658-709

Digital Library

[62]

O’Hearn PW, Yang H, Reynolds JC (2004) Separation and information hiding. In: ACM symposium on principles of programming languages (POPL), pp 268–280

[63]

Parkinson MJ Local reasoning for Java. Technical Report 654. Dissertation,University of Cambridge Computer Laboratory

[64]

Pierik C, Clarke D, de Boer FS (2005) Controlling object allocation using creation guards. In: Proceedings, formal methods, Vol. 3582 of LNCS, pp 59–74

[65]

Pierik C, de Boer FS (2005) On behavioral subtyping and completeness. In: J. Vitek, F. Logozzo (eds) ECOOP workshop on formal techniques for Java-like programs (to appear)

[66]

Pierik C and de Boer FS A proof outline logic for object-oriented programming Theoret Comput Sci 2005 343 413-442

Digital Library

[67]

Pitts AM (1996) Reasoning about local variables with operationally-based logical relations. In: O’Hearn PW, Tennent RD (eds) Algol-like languages, Vol. 2, chap 17, pp 173–193. Birkhauser, 1997. In: Reprinted from proceedings 11th annual IEEE symposium on logic in computer science, Brunswick, 1996, pp 152–163

[68]

Pitts AM Parametric polymorphism and operational equivalence Math Struct Comput Sci 2000 10 321-359

Digital Library

[69]

Plotkin G (1973) Lambda definability and logical relations. Technical Report SAI-RM-4, University of Edinburgh, School of Artificial Intelligence

[70]

Reynolds JC The craft of programming 1981 Englewood Cliffs Prentice-Hall

Digital Library

[71]

Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: LICS, pp 55–74

[72]

Rehof J and Mogensen T Tractable constraints in finite semilattices Sci Comput Program 1999 35 2–3 191-221

Digital Library

[73]

Szyperski C, Gruntz D, and Murer S Component software: beyond object-oriented programming 2002 2 New York ACM Press and Addison-Wesley

Digital Library

[74]

Skalka C, Smith S (2005) Static use-based object confinement. Springer Int J Inf Sec 4(1–2)

[75]

Yang H, O’Hearn PW (2002) A semantic basis for local reasoning. In: Proceedings, FOSSACS

Cited By

Filipović IO’Hearn PTorp-Smith NYang H(2010)Blaming the client: on data refinement in the presence of pointersFormal Aspects of Computing10.1007/s00165-009-0125-822:5(547-583)Online publication date: 1-Sep-2010
https://dl.acm.org/doi/10.1007/s00165-009-0125-8
O'Hearn PYang HReynolds J(2009)Separation and information hidingACM Transactions on Programming Languages and Systems10.1145/1498926.149892931:3(1-50)Online publication date: 21-Apr-2009
https://dl.acm.org/doi/10.1145/1498926.1498929

Index Terms

On assertion-based encapsulation for object invariants and simulations

Index terms have been assigned to the content through auto-classification.

Recommendations

Assertion-based encapsulation, object invariants and simulations
FMCO'04: Proceedings of the Third international conference on Formal Methods for Components and Objects

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 ...
Object-oriented encapsulation for dynamically typed languages
OOPSLA '04: Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications

Encapsulation in object-oriented languages has traditionally been based on static type systems. As a consequence, dynamically-typed languages have only limited support for encapsulation. This is surprising, considering that encapsulation is one of the ...
Encapsulation and inheritance in object-oriented programming languages
OOPSLA '86: Conference proceedings on Object-oriented programming systems, languages and applications

Object-oriented programming is a practical and useful programming methodology that encourages modular design and software reuse. Most object-oriented programming languages support data abstraction by preventing an object from being manipulated except ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 19, Issue 2

Jun 2007

134 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2006.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 June 2007

Accepted: 31 October 2006

Revision received: 15 September 2006

Received: 16 August 2006

Published in FAC Volume 19, Issue 2

Author Tags

Qualifiers

Editorial

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
62
Total Downloads

Downloads (Last 12 months)47
Downloads (Last 6 weeks)14

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Filipović IO’Hearn PTorp-Smith NYang H(2010)Blaming the client: on data refinement in the presence of pointersFormal Aspects of Computing10.1007/s00165-009-0125-822:5(547-583)Online publication date: 1-Sep-2010
https://dl.acm.org/doi/10.1007/s00165-009-0125-8
O'Hearn PYang HReynolds J(2009)Separation and information hidingACM Transactions on Programming Languages and Systems10.1145/1498926.149892931:3(1-50)Online publication date: 21-Apr-2009
https://dl.acm.org/doi/10.1145/1498926.1498929

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents