article

Using data groups to specify and check side effects

Authors:

K. Rustan M. Leino,

Arnd Poetzsch-Heffter,

Yunhong ZhouAuthors Info & Claims

ACM SIGPLAN Notices, Volume 37, Issue 5

Pages 246 - 257

https://doi.org/10.1145/543552.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

Melicher DXu AZhao VPotanin AAldrich J(2022)Bounded Abstract EffectsACM Transactions on Programming Languages and Systems10.1145/349242744:1(1-48)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3492427
Fonseca ACabral BRafael JCorreia I(2016)Automatic ParallelizationInternational Journal of Parallel Programming10.1007/s10766-016-0426-544:6(1337-1358)Online publication date: 1-Dec-2016
https://dl.acm.org/doi/10.1007/s10766-016-0426-5
Stork SNaden KSunshine JMohr MFonseca AMarques PAldrich J(2014)ÆminiumACM Transactions on Programming Languages and Systems10.1145/254392036:1(1-42)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.1145/2543920
Show More Cited By

Index Terms

Recommendations

Using data groups to specify and check side effects
PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation

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 SIGPLAN Notices

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

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

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 May 2002

Published in SIGPLAN Volume 37, Issue 5

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

74
Total Citations
View Citations
498
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Melicher DXu AZhao VPotanin AAldrich J(2022)Bounded Abstract EffectsACM Transactions on Programming Languages and Systems10.1145/349242744:1(1-48)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3492427
Fonseca ACabral BRafael JCorreia I(2016)Automatic ParallelizationInternational Journal of Parallel Programming10.1007/s10766-016-0426-544:6(1337-1358)Online publication date: 1-Dec-2016
https://dl.acm.org/doi/10.1007/s10766-016-0426-5
Stork SNaden KSunshine JMohr MFonseca AMarques PAldrich J(2014)ÆminiumACM Transactions on Programming Languages and Systems10.1145/254392036:1(1-42)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.1145/2543920
Dietl WMüller P(2013)Object Ownership in Program VerificationAliasing in Object-Oriented Programming. Types, Analysis and Verification10.1007/978-3-642-36946-9_11(289-318)Online publication date: 2013
https://doi.org/10.1007/978-3-642-36946-9_11
Sun CLopes CFisher K(2011)Alternate annotation checkers using fractional permissionsProceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion10.1145/2048147.2048178(75-78)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2048147.2048178
Boyland J(2010)Semantics of fractional permissions with nestingACM Transactions on Programming Languages and Systems10.1145/1749608.174961132:6(1-33)Online publication date: 13-Aug-2010
https://dl.acm.org/doi/10.1145/1749608.1749611
Yorsh GSkidanov AReps TSagiv M(2005)Automatic Assume/Guarantee Reasoning for Heap-Manipulating ProgramsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.01.028131(125-138)Online publication date: 1-May-2005
https://dl.acm.org/doi/10.1016/j.entcs.2005.01.028
Müller PPoetzsch‐Heffter ALeavens G(2003)Modular specification of frame properties in JMLConcurrency and Computation: Practice and Experience10.1002/cpe.71315:2(117-154)Online publication date: 6-Jan-2003
https://doi.org/10.1002/cpe.713
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
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 Issue’s Table of Contents