Article

Using data groups to specify and check side effects

Authors:

K. Rustan M. Leino,

Arnd Poetzsch-Heffter,

Yunhong ZhouAuthors Info & Claims

PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation

Pages 246 - 257

https://doi.org/10.1145/512529.512559

Published: 17 May 2002 Publication History

Abstract

Reasoning precisely about the side effects of procedure calls is important to many program analyses. This paper introduces a technique for specifying and statically checking the side effects of methods in an object-oriented language. The technique uses data groups, which abstract over variables that are not in scope, and limits program behavior by two alias-confining restrictions, pivot uniqueness and owner exclusion. The technique is shown to achieve modular soundness and is simpler than previous attempts at solving this problem.

References

[1]

A. Banerjee and D. A. Naumann. Representation independence, confinement and access control {extended abstract}. In Proc. 29th POPL, pages 166--177, Jan. 2002]]

Digital Library

[2]

J. Boyland. Alias burying: Unique variables without destructive reads. SP&E, 31(1):533--553, Jan. 2001]]

Digital Library

[3]

J. Boyland. The interdependence of effects and uniqueness. In 3rd workshop on Formal Techniques for Java Programs, 2001]]

[4]

R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In Proc. PLDI'01, volume 36 of SIGPLAN Notices 36(5), pages 59--69. ACM, May 2001]]

Digital Library

[5]

D. L. Detlefs, K. R. M. Leino, and G. Nelson. Wrestling with rep exposure. Research Report 156, Digital Equipment Corporation Systems Research Center, July 1998]]

[6]

D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq SRC, Dec. 1998]]

[7]

E. W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976]]

Digital Library

[8]

D. Evans, J. V. Guttag, J. J. Horning, and Y. M. Tan. LCLint: A tool for using specifications to check code. In D. S. Wile, editor, Proc. 2nd SIGSOFT, ACM SIGSOFT Software Eng. Notes 19(5), pages 87--96, Dec. 1994]]

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 Proc. PLDI'02, 2002]]

Digital Library

[10]

A. Greenhouse and J. Boyland. An object-oriented effects system. In Proc. 13th ECOOP, number 1628 in LNCS, pages 205--229. Springer, June 1999]]

Digital Library

[11]

J. V. Guttag and J. J. Horning, editors. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993. With S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing]]

Digital Library

[12]

D. Jackson. Aspect: Detecting bugs with abstract dependences. ACM Trans. Software Eng. and Methodology, 4(2):109--145, Apr. 1995]]

Digital Library

[13]

R. Joshi. Extended static checking of programs with cyclic dependencies. In J. Mason, editor, 1997 SRC Summer Intern Projects, Technical Note 1997-028. DEC SRC, 1997]]

[14]

P. Jouvelot and D. K. Gifford. Algebraic reconstruction of types and effects. In Proc. 18th POPL, pages 303--310, Jan. 1991]]

Digital Library

[15]

G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06f, Iowa State University, Department of Computer Science, July 1999]]

[16]

K. R. M. Leino. Toward Reliable Modular Programs. PhD thesis, Caltech, 1995. Technical Report Caltech-CS-TR-95-03]]

Digital Library

[17]

K. R. M. Leino. Data groups: Specifying the modification of extended state. In Proc. OOPSLA '98, pages 144--153. ACM, 1998]]

Digital Library

[18]

K. R. M. Leino. Applications of extended static checking. In P. Cousot, editor, Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of LNCS, pages 185--193. Springer, July 2001]]

Digital Library

[19]

K. R. M. Leino. Extended static checking: A ten-year perspective. In R. Wilhelm, editor, Informatics---10 Years Back, 10 Years Ahead, volume 2000 of LNCS, pages 157--175. Springer, Jan. 2001]]

Digital Library

[20]

K. R. M. Leino and G. Nelson. Data abstraction and information hiding. Research Report 160, Compaq SRC, Nov. 2000. To appear in TOPLAS]]

[21]

B. Liskov and J. Guttag. Abstraction and Specification in Program Development. MIT Electrical Engineering and Computer Science Series. MIT Press, 1986]]

Digital Library

[22]

J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In J.-T. Schwartz, editor, Proc. Symposia in Applied Mathematics. American Mathematical Society, 1967]]

[23]

C. Morgan. The specification statement. ACM Trans. Prog. Lang. Syst., 10(3):403--419, July 1988]]

Digital Library

[24]

P. Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of LNCS. Springer-Verlag, 2002. The author's PhD thesis, FernUniversität Hagen.]]

[25]

P. Müller and A. Poetzsch-Heffter. Modular specification and verification techniques for object-oriented software components. In G. T. Leavens and M. Sitaraman, editors, Foundations of Component-Based Systems, chapter~7, pages 137--159. Cambridge University Press, 2000]]

Digital Library

[26]

P. Müller and A. Poetzsch-Heffter. Universes: A type system for alias and dependency control. Technical Report 279, FernUniversität Hagen, 2001]]

[27]

G. Nelson. A generalization of Dijkstra's calculus. ACM Trans. Prog. Lang. Syst., 11(4):517--561, 1989]]

Digital Library

[28]

R. Page. Functional programming, and where you can put it. ACM SIGPLAN Notices, 36(9):19--24, Sept. 2001]]

Digital Library

[29]

A. Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitationsschrift, Technische Universität München, 1997]]

[30]

J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, 2nd edition edition, 1992]]

Digital Library

[31]

J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245--271, July 1992]]

[32]

M. Utting. Reasoning about aliasing. In Proc. 4th Australasian Refinement Workshop, pages 195--211. School of Comp. Sci. and Eng., The Univ. of New South Wales, Apr. 1995]]

[33]

M. T. Vandevoorde. Exploiting Specifications to Improve Program Performance. PhD thesis, Massachusetts Institute of Technology, Feb. 1994. Available as Technical Report MIT/LCS/TR-598]]

Digital Library

[34]

H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. 26th POPL, pages 214--227, Jan. 1999]]

Digital Library

Cited By

Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Banerjee ANaumann DNikouei M(2018)A Logical Analysis of Framing for Specifications with Pure Method CallsACM Transactions on Programming Languages and Systems10.1145/317480140:2(1-90)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3174801
Bao YLeavens GErnst G(2018)Unifying separation logic and region logic to allow interoperabilityFormal Aspects of Computing10.1007/s00165-018-0455-530:3-4(381-441)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s00165-018-0455-5
Show More Cited By

Index Terms

Recommendations

Using data groups to specify and check side effects

Reasoning precisely about the side effects of procedure calls is important to many program analyses. This paper introduces a technique for specifying and statically checking the side effects of methods in an object-oriented language. The technique uses ...
Epistemic Side Effects: An AI Safety Problem
AAMAS '23: Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems

AI safety research has investigated the problem of negative side effects -- undesirable changes made by AI systems in pursuit of an underspecified objective. However, the focus has been on physical side effects, such as a robot breaking a vase while ...
Detecting and exploring side effects when repairing model inconsistencies
SLE 2019: Proceedings of the 12th ACM SIGPLAN International Conference on Software Language Engineering

When software models change, developers often fail in keeping them consistent. Automated support in repairing inconsistencies is widely addressed. Yet, merely enumerating repairs for developers is not enough. A repair can as a side effect cause new ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation

June 2002

338 pages

ISBN:1581134630

DOI:10.1145/512529

General Chair:
Jens Knoop
Universität Dortmund, Germany
,
Program Chair:
Laurie J. Hendren
McGill University, Canada

ACM SIGPLAN Notices Volume 37, Issue 5
May 2002
326 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/543552
Issue’s Table of Contents

Copyright © 2002 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 May 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI02

Sponsor:

SIGPLAN

PLDI02: ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation

June 17 - 19, 2002

Berlin, Germany

Acceptance Rates

PLDI '02 Paper Acceptance Rate 28 of 169 submissions, 17%;

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

74
Total Citations
View Citations
501
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Banerjee ANaumann DNikouei M(2018)A Logical Analysis of Framing for Specifications with Pure Method CallsACM Transactions on Programming Languages and Systems10.1145/317480140:2(1-90)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3174801
Bao YLeavens GErnst G(2018)Unifying separation logic and region logic to allow interoperabilityFormal Aspects of Computing10.1007/s00165-018-0455-530:3-4(381-441)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s00165-018-0455-5
Polikarpova NTschannen JFuria C(2018)A fully verified container libraryFormal Aspects of Computing10.1007/s00165-017-0435-130:5(495-523)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s00165-017-0435-1
Furia CNordio MPolikarpova NTschannen J(2017)AutoProofInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0419-019:6(697-716)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1007/s10009-016-0419-0
Polikarpova NTschannen JFuria C(2015)A Fully Verified Container LibraryFM 2015: Formal Methods10.1007/978-3-319-19249-9_26(414-434)Online publication date: 2015
https://doi.org/10.1007/978-3-319-19249-9_26
Geffken MThiemann PKolodziej JChilders B(2014)Side effect monitoring for Java using bytecode rewritingProceedings of the 2014 International Conference on Principles and Practices of Programming on the Java platform: Virtual machines, Languages, and Tools10.1145/2647508.2647515(87-98)Online publication date: 23-Sep-2014
https://dl.acm.org/doi/10.1145/2647508.2647515
Dietl WMüller P(2013)Object ownership in program verificationAliasing in Object-Oriented Programming10.5555/2554511.2554528(289-318)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554528
Bocchino R(2013)Alias control for deterministic parallelismAliasing in Object-Oriented Programming10.5555/2554511.2554521(156-195)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554521
Flanagan CLeino KLillibridge MNelson GSaxe JStata R(2013)PLDI 2002ACM SIGPLAN Notices10.1145/2502508.250252048:4S(22-33)Online publication date: 9-Jul-2013
https://dl.acm.org/doi/10.1145/2502508.2502520
Show More Cited By

View Options

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