K. Rustan M. Leino
Skip Abstract Section
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.
- A. Banerjee and D. A. Naumann. Representation independence, confinement and access control {extended abstract}. In Proc. 29th POPL, pages 166--177, Jan. 2002]] Google Scholar
Digital Library
- J. Boyland. Alias burying: Unique variables without destructive reads. SP&E, 31(1):533--553, Jan. 2001]] Google ScholarDigital Library
- J. Boyland. The interdependence of effects and uniqueness. In 3rd workshop on Formal Techniques for Java Programs, 2001]]Google Scholar
- 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]] Google ScholarDigital Library
- 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]]Google Scholar
- D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq SRC, Dec. 1998]]Google Scholar
- E. W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976]] Google ScholarDigital Library
- 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]] Google ScholarDigital Library
- 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]] Google ScholarDigital Library
- A. Greenhouse and J. Boyland. An object-oriented effects system. In Proc. 13th ECOOP, number 1628 in LNCS, pages 205--229. Springer, June 1999]] Google ScholarDigital Library
- 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]] Google ScholarDigital Library
- D. Jackson. Aspect: Detecting bugs with abstract dependences. ACM Trans. Software Eng. and Methodology, 4(2):109--145, Apr. 1995]] Google ScholarDigital Library
- 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]]Google Scholar
- P. Jouvelot and D. K. Gifford. Algebraic reconstruction of types and effects. In Proc. 18th POPL, pages 303--310, Jan. 1991]] Google ScholarDigital Library
- 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]]Google Scholar
- K. R. M. Leino. Toward Reliable Modular Programs. PhD thesis, Caltech, 1995. Technical Report Caltech-CS-TR-95-03]] Google ScholarDigital Library
- K. R. M. Leino. Data groups: Specifying the modification of extended state. In Proc. OOPSLA '98, pages 144--153. ACM, 1998]] Google ScholarDigital Library
- 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]] Google ScholarDigital Library
- 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]] Google ScholarDigital Library
- K. R. M. Leino and G. Nelson. Data abstraction and information hiding. Research Report 160, Compaq SRC, Nov. 2000. To appear in TOPLAS]]Google Scholar
- B. Liskov and J. Guttag. Abstraction and Specification in Program Development. MIT Electrical Engineering and Computer Science Series. MIT Press, 1986]] Google ScholarDigital Library
- 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]]Google Scholar
- C. Morgan. The specification statement. ACM Trans. Prog. Lang. Syst., 10(3):403--419, July 1988]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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]] Google ScholarDigital Library
- P. Müller and A. Poetzsch-Heffter. Universes: A type system for alias and dependency control. Technical Report 279, FernUniversität Hagen, 2001]]Google Scholar
- G. Nelson. A generalization of Dijkstra's calculus. ACM Trans. Prog. Lang. Syst., 11(4):517--561, 1989]] Google ScholarDigital Library
- R. Page. Functional programming, and where you can put it. ACM SIGPLAN Notices, 36(9):19--24, Sept. 2001]] Google ScholarDigital Library
- A. Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitationsschrift, Technische Universität München, 1997]]Google Scholar
- J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, 2nd edition edition, 1992]] Google ScholarDigital Library
- J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245--271, July 1992]]Google ScholarCross Ref
- 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]]Google Scholar
- 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]] Google ScholarDigital Library
- H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. 26th POPL, pages 214--227, Jan. 1999]] Google ScholarDigital Library
Index Terms
- Using data groups to specify and check side effects
Recommendations
Using data groups to specify and check side effects
PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementationReasoning 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 SystemsAI 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 EngineeringWhen 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