research-article

Enhancing modular OO verification with separation logic

Authors:

Cristina David,

Huu Hai Nguyen,

Shengchao QinAuthors Info & Claims

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 87 - 99

https://doi.org/10.1145/1328438.1328452

Published: 07 January 2008 Publication History

Abstract

Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this.

References

[1]

P. America. Designing an object-oriented programming language with behavioural subtyping. In the REX School/Worshop on Foundations of Object-Oriented Languages, pages 60--90, 1991.

Digital Library

[2]

M. Barnet, R. DeLine, M. Fahndrich, K.R.M Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27--56, 2004.

[3]

M. Barnett, K.R.M. Leino, and W. Schulte. The Spec# programming system: An overview. In Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, 2004.

Digital Library

[4]

D.R. Cok and J. Kiniry. ESC/Java2: Uniting ESC/Java and JML. In Int'l Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pages 108--128, 2004.

Digital Library

[5]

K.K. Dhara and G.T. Leavens. Forcing behavioral subtyping through specification inheritance. In IEEE/ACM Intl. Conf. on Software Engineering, pages 258--267, 1996.

Digital Library

[6]

J.C. Filliâtre. Why: a multi-language multi-prover verification tool. Technical Report 1366, LRI, Université Paris Sud, March 2003.

[7]

R.B. Findler and M. Felleisen. Contract soundness for object--oriented languages. In SIGPLAN Object--Oriented Programming Systems, Languages and Applications, pages 1--15, 2001.

Digital Library

[8]

R.B. Findler, M. Latendresse, and M. Felleisen. Behavioral contracts and behavioral subtyping. In ESEC/SIGSOFT Foundations of Software Engr., 2001.

Digital Library

[9]

C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata. Extended Static Checking for Java. In ACM PLDI, June 2002.

Digital Library

[10]

J. Hatcliff, X. Deng, M.B. Dwyer, G. Jung, and V.P. Ranganath. Cadena: An integrated development, analysis, and verification environment for component-based systems. In IEEE/ACM Intl. Conf. on Software Engineering, 2003.

Digital Library

[11]

S. Isthiaq and P.W. O'Hearn. BI as an assertion language for mutable data structures. In ACM POPL, London, January 2001.

Digital Library

[12]

J. Kiniry, E. Poll, and D. Cok. Design by contract and automatic verification for Java with JML and ESC/Java2. ETAPS tutorial, 2005.

[13]

G.T. Leavens and Peter Muller. Information hiding and visibility in interface specifications. In IEEE/ACM Intl. Conf. on Software Engineering, pages 385--395, Washington, DC, USA, 2007. IEEE Computer Society.

Digital Library

[14]

G.T. Leavens and David A. Naumann. Behavioral subtyping is equivalent to modular reasoning for object-oriented programs. Technical Report 06-36, Department of Computer Science, Iowa State University, 2006.

[15]

G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 31 (3):1--38, 2006.

Digital Library

[16]

G.T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, P. Müller, and J. Kiniry. JML Reference Manual (DRAFT), February 2007.

[17]

K.R.M. Leino and P. Müller. Object invariants in dynamic contexts. In ECOOP, pages 491--516, 2004.

[18]

B.H. Liskov. Data abstraction and hierarchy. ACM SIGPLAN Notices, 23(5):17--34, May 1988. Revised version of the keynote address given at OOPSLA'87.

Digital Library

[19]

B.H. Liskov and J.M. Wing. A behavioral notion of subtyping. ACM Trans. on Programming Languages and Systems, 16 (6):1811--1841, 1994.

Digital Library

[20]

C. Marché and C. Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In 18th Int'l Conf. on Theorem Proving in Higher Order Logics. Springer, LNCS, August 2005.

Digital Library

[21]

C. Marché, C. Paulin-Mohring, and X. Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58 (1--2):89--106, 2004.

[22]

B. Meyer. Object-oriented Software Construction. Prentice Hall. Second Edition., 1997.

Digital Library

[23]

R. Middelkoop, C. Huizing, R. Kuiper, and E.J. Luit. Invariants for non-hierarchical object structures. In L. Ribeiro and A. Martins Moreira, editors, Proceedings of the 9th Brazilian Symposium on Formal Methods (SBMF'06), Natal, Brazil, 2006.

[24]

P. Muller. Modular specification and verification of object-oriented programs. Springer, New York, NY, USA, 2002. ISBN 3-540-43167-5.

Digital Library

[25]

H.H. Nguyen, C. David, S.C. Qin, and W.N. Chin. Automated Verification of Shape And Size Properties via Separation Logic. In Intl Conf. on Verification, Model Checking and Abstract Interpretation, Nice, France, January 2007.

Digital Library

[26]

J.W. Nimmer and M.D. Ernst. Invariant inference for static checking. In ESEC/SIGSOFT Foundations of Software Engr., pages 11--20, 2002.

Digital Library

[27]

P.W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1--3):271--307, 2007.

Digital Library

[28]

P.W. O'Hearn, H. Yang, and J.C. Reynolds. Separation and Information Hiding. In ACM POPL, Venice, Italy, January 2004.

Digital Library

[29]

J. Ostroff, C. Wang, E. Kerfoot, and F.A. Torshizi. Automated model--based verification of object-oriented code. Technical Report CS-2006-05, York University, Canada, May 2006.

[30]

M.J. Parkinson. Local Reasoning for Java. PhD thesis, Computer Laboratory, University of Cambridge, 2005. UCAM-CL-TR-654.

[31]

M.J. Parkinson and G.M. Bierman. Separation logic and abstraction. In ACM POPL, pages 247--258, 2005.

Digital Library

[32]

M.J. Parkinson and G.M. Bierman. Separation logic, abstraction and inheritance. In ACM POPL, 2008.

Digital Library

[33]

C. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In SPIN Workshop, April 2004.

[34]

W. Pugh. The Omega Test: A fast practical integer programming algorithm for dependence analysis. Communications of the ACM, 8:102--114, 1992.

Digital Library

[35]

J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In IEEE Logic in Computer Science, Copenhagen, Denmark, July 2002.

Digital Library

[36]

Robby, M. B. Dwyer, and J. Hatcliff. Bogor: an extensible and highly-modular software model checking framework. In ESEC/SIGSOFT Foundations of Software Engr., pages 267--276, 2003.

Digital Library

Cited By

Yan CLi BVorobeychik YLaszka AFabbri DMalin B(2019)Database Audit Workload Prioritization via Game TheoryACM Transactions on Privacy and Security10.1145/332392422:3(1-21)Online publication date: 10-Jun-2019
https://dl.acm.org/doi/10.1145/3323924
Sharif MBhagavatula SBauer LReiter M(2019)A General Framework for Adversarial Examples with ObjectivesACM Transactions on Privacy and Security10.1145/331761122:3(1-30)Online publication date: 10-Jun-2019
https://dl.acm.org/doi/10.1145/3317611
Knechtel JLienig JElfadel I(2017)Multi-Objective 3D Floorplanning with Integrated Voltage AssignmentACM Transactions on Design Automation of Electronic Systems10.1145/314981723:2(1-27)Online publication date: 27-Nov-2017
https://dl.acm.org/doi/10.1145/3149817
Show More Cited By

Recommendations

Separation logic, abstraction and inheritance
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Inheritance is a fundamental concept in object-oriented programming, allowing new classes to be defined in terms of old classes. When used with care, inheritance is an essential tool for object-oriented programmers. Thus, for those interested in ...
Enhancing modular OO verification with separation logic
POPL '08

Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in ...
Verifying executable object-oriented specifications with separation logic
ECOOP'10: Proceedings of the 24th European conference on Object-oriented programming

Specifications of Object-Oriented programs conventionally employ Boolean expressions of the programming language for assertions. Programming errors can be discovered by checking at runtime whether an assertion, such as a precondition or class invariant, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2008

448 pages

ISBN:9781595936899

DOI:10.1145/1328438

General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

ACM SIGPLAN Notices Volume 43, Issue 1
POPL '08
January 2008
420 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1328897
Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL08

Sponsor:

POPL08: The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 7 - 12, 2008

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 773 of 3,910 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

73
Total Citations
View Citations
539
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)4

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yan CLi BVorobeychik YLaszka AFabbri DMalin B(2019)Database Audit Workload Prioritization via Game TheoryACM Transactions on Privacy and Security10.1145/332392422:3(1-21)Online publication date: 10-Jun-2019
https://dl.acm.org/doi/10.1145/3323924
Sharif MBhagavatula SBauer LReiter M(2019)A General Framework for Adversarial Examples with ObjectivesACM Transactions on Privacy and Security10.1145/331761122:3(1-30)Online publication date: 10-Jun-2019
https://dl.acm.org/doi/10.1145/3317611
Knechtel JLienig JElfadel I(2017)Multi-Objective 3D Floorplanning with Integrated Voltage AssignmentACM Transactions on Design Automation of Electronic Systems10.1145/314981723:2(1-27)Online publication date: 27-Nov-2017
https://dl.acm.org/doi/10.1145/3149817
Lin CWan LChen D(2017)C-MineACM Transactions on Design Automation of Electronic Systems10.1145/314453423:2(1-23)Online publication date: 29-Nov-2017
https://dl.acm.org/doi/10.1145/3144534
Yang KShen HForte DBhunia STehranipoor M(2017)Hardware-Enabled Pharmaceutical Supply Chain SecurityACM Transactions on Design Automation of Electronic Systems10.1145/314453223:2(1-26)Online publication date: 21-Dec-2017
https://dl.acm.org/doi/10.1145/3144532
Davis JAlvarado C(2017)Supporting undergraduates to make the most of conferencesACM Inroads10.1145/31236618:3(32-35)Online publication date: 28-Jul-2017
https://dl.acm.org/doi/10.1145/3123661
(2016)BibliographyFrom Action Systems to Distributed Systems10.1201/b20053-23(247-271)Online publication date: 20-Apr-2016
https://doi.org/10.1201/b20053-23
Owe O(2016)Reasoning About Inheritance and Unrestricted Reuse in Object-Oriented Concurrent SystemsProceedings of the 12th International Conference on Integrated Formal Methods - Volume 968110.1007/978-3-319-33693-0_14(210-225)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1007/978-3-319-33693-0_14
Leavens GNaumann D(2015)Behavioral Subtyping, Specification Inheritance, and Modular ReasoningACM Transactions on Programming Languages and Systems10.1145/276644637:4(1-88)Online publication date: 13-Aug-2015
https://dl.acm.org/doi/10.1145/2766446
Hu TWang SQiu Z(2015)Verifying Interaction between Methods in ClassesProceedings of the 2015 International Symposium on Theoretical Aspects of Software Engineering10.1109/TASE.2015.24(119-126)Online publication date: 12-Sep-2015
https://dl.acm.org/doi/10.1109/TASE.2015.24
Show More Cited By

View Options

Get Access

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents