Modular set-based analysis from contracts

ABSTRACT

In PLT Scheme, programs consist of modules with contracts. The latter describe the inputs and outputs of functions and objects via predicates. A run-time system enforces these predicates; if a predicate fails, the enforcer raises an exception that blames a specific module with an explanation of the fault.In this paper, we show how to use such module contracts to turn set-based analysis into a fully modular parameterized analysis. Using this analysis, a static debugger can indicate for any given contract check whether the corresponding predicate is always satisfied, partially satisfied, or (potentially) completely violated. The static debugger can also predict the source of potential errors, i.e., it is sound with respect to the blame assignment of the contract system.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Benjamin Pierce , Gordon Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.237-268, April 1991 [doi>10.1145/103135.103138]
• 2: Manuel Fahndrich , Alex Aiken, Making Set-Constraint Program Analyses Scale, University of California at Berkeley, Berkeley, CA, 1996
• 3: Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
• 4: François Bourdoncle, Abstract debugging of higher-order imperative languages, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.46-55, June 21-25, 1993, Albuquerque, New Mexico, United States
• 5: Robert Cartwright , Mike Fagan, Soft typing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.278-292, June 24-28, 1991, Toronto, Ontario, Canada
• 6: Patrick Cousot , Radhia Cousot, Modular Static Program Analysis, Proceedings of the 11th International Conference on Compiler Construction, p.159-178, April 08-12, 2002
• 7: Detlefs, D. L., K. R. M. Leino, G. Nelson and J. B. Saxe. Extended static checking. Technical Report 159, Compaq SRC Research Report, 1998.
• 8: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 9: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 10: Cormac Flanagan , Matthias Felleisen, Componential set-based analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.2, p.370-416, March 1999 [doi>10.1145/316686.316703]
• 11: Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Stephanie Weirich , Matthias Felleisen, Catching bugs in the web of program invariants, ACM SIGPLAN Notices, v.31 n.5, p.23-32, May 1996
• 12: Matthew Flatt, Composable and compilable macros:: you want it when?, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.72-83, October 04-06, 2002, Pittsburgh, PA, USA
• 13: Matthew Flatt , Robert Bruce Findler , Shriram Krishnamurthi , Matthias Felleisen, Programming languages as operating systems (or revenge of the son of the lisp machine), Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.138-147, September 27-29, 1999, Paris, France
• 14: Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
• 15: Christian Haack , J. B. Wells, Type error slicing in implicitly typed higher-order languages, Science of Computer Programming, v.50 n.1-3, p.189-224, March 2004 [doi>10.1016/j.scico.2004.01.004]
• 16: Nevin Heintze, Set-based analysis of ML programs, Proceedings of the 1994 ACM conference on LISP and functional programming, p.306-317, June 27-29, 1994, Orlando, Florida, United States
• 17: Fritz Henglein, Dynamic typing, Symposium proceedings on 4th European symposium on programming, p.233-253, January 1992, Rennes, France
• 18: Haruo Hosoya , Jérôme Vouillon , Benjamin C. Pierce, Regular expression types for XML, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.11-22, September 2000
• 19: Leroy, X., D. Doligez, J. Garrigue, D. Rémy and J. Vouillon. The Objective Caml system -- documentation and user's manual, 2005.
• 20: David MacQueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.198-207, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802036]
• 21: Philippe Meunier , Robert Bruce Findler , Paul Steckler , Mitchell Wand, Selectors Make Set-Based Analysis Too Hard, Higher-Order and Symbolic Computation, v.18 n.3-4, p.245-269, December 2005 [doi>10.1007/s10990-005-4876-5]
• 22: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 23: Jens Palsberg, Closure analysis in constraint form, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.1, p.47-62, Jan. 1995 [doi>10.1145/200994.201001]
• 24: Jens Palsberg , Christina Pavlopoulou, From polyvariant flow information to intersection and union types, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.197-208, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268963]
• 25: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
• 26: Christian W. Probst, Modular Control Flow Analysis for Libraries, Proceedings of the 9th International Symposium on Static Analysis, p.165-179, September 17-20, 2002
• 27: Olin Shivers, The semantics of Scheme control-flow analysis, Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.190-198, June 17-19, 1991, New Haven, Connecticut, United States
• 28: Yan Mei Tang , Pierre Jouvelot, Separate Abstract Interpretation for Control-Flow Analysis, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.224-243, April 19-22, 1994
• 29: Mitchell Wand, Finding the source of type errors, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-43, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512648]
• 30: Mitchell Wand , Galen B. Williamson, A Modular, Extensible Proof Method for Small-Step Flow Analyses, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.213-227, April 08-12, 2002
• 31: J. B. Wells , Allyn Dimock , Robert Muller , Franklyn Turbak, A calculus with polymorphic and polyvariant flow types, Journal of Functional Programming, v.12 n.3, p.183-227, May 2002 [doi>10.1017/S0956796801004245]
• 32: Andrew K. Wright , Suresh Jagannathan, Polymorphic splitting: an effective polyvariant flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.166-207, Jan. 1998 [doi>10.1145/271510.271523]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Programming by contract

General Terms:
Languages, Reliability, Verification

Keywords:
modular analysis, runtime contracts, set-based analysis, static debugging