Philippe Meunier
Robert Bruce Findler
Matthias Felleisen
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.
- Abadi, M., L. Cardelli, B. Pierce and G. Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237--268, 1991. Google Scholar
Digital Library
- Aiken, A. S. and M. Fähndrich. Making set-constraint based program analyses scale. Technical Report CSD-96-917, University of California, Berkeley, September 1996. Google ScholarDigital Library
- Amadio, R. M. and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575--631, September 1993. Google ScholarDigital Library
- Bourdoncle, F. Abstract debugging of higher-order imperative languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 46--55, 1993. Google ScholarDigital Library
- Cartwright, R. and M. Fagan. Soft typing. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 278--292, 1991. Google ScholarDigital Library
- Cousot, P. and R. Cousot. Modular static program analysis, invited paper. In Horspool, R., editor, Proceedings of the Eleventh International Conference on Compiler Construction (CC 2002), pages 159--178, Grenoble, France, April 6--14 2002. LNCS 2304, Springer, Berlin. Google ScholarDigital Library
- Detlefs, D. L., K. R. M. Leino, G. Nelson and J. B. Saxe. Extended static checking. Technical Report 159, Compaq SRC Research Report, 1998.Google Scholar
- Findler, R. B. and M. Felleisen. Contracts for higher-order functions. In ACM SIGPLAN International Conference on Functional Programming, 2002. Google ScholarDigital Library
- Flanagan, C. Hybrid type checking. In Proceedings of the symposium on Principles of Programming Languages, 2006. In this volume. Google ScholarDigital Library
- Flanagan, C. and M. Felleisen. Componential set-based analysis. ACM Trans. on Programming Languages and Systems, 21(2):369--415, Feb. 1999. Google ScholarDigital Library
- Flanagan, C., M. Flatt, S. Krishnamurthi, S. Weirich and M. Felleisen. Catching bugs in the web of program invariants. ACM SIGPLAN Notices, 31(5):23--32, 1996. Google ScholarDigital Library
- Flatt, M. Composable and compilable macros: You want it when? In ACM SIGPLAN International Conference on Functional Programming, 2002. Google ScholarDigital Library
- Flatt, M., R. B. Findler, S. Krishnamurthi and M. Felleisen. Programming languages as operating systems (or revenge of the son of the Lisp machine). In ACM SIGPLAN International Conference on Functional Programming, pages 138--147, September 1999. Google ScholarDigital Library
- Foster, J. S., M. Fähndrich and A. Aiken. A theory of type qualifiers. In PLDI '99: Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, pages 192--203, New York, NY, USA, 1999. ACM Press. Google ScholarDigital Library
- Haack, C. and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Sci. Comput. Programming, 50:189--224, 2004. Google ScholarDigital Library
- Heintze, N. Set-based analysis of ml programs. In LFP '94: Proceedings of the 1994 ACM conference on LISP and functional programming, pages 306--317, New York, NY, USA, 1994. ACM Press. Google ScholarDigital Library
- Henglein, F. Dynamic typing. In Proceedings of the 4th European Symposium on Programming, pages 233--253, London, UK, 1992. Springer-Verlag. Google ScholarDigital Library
- Hosoya, H., J. Vouillon and B. C. Pierce. Regular expression types for xml. In Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pages 11--22. ACM Press, 2000. Google ScholarDigital Library
- Leroy, X., D. Doligez, J. Garrigue, D. Rémy and J. Vouillon. The Objective Caml system -- documentation and user's manual, 2005.Google Scholar
- MacQueen, D. B. Modules for Standard ML. In Proceedings of the 1984 ACM Conference on LISP and Functional Programming, pages 198--207, New York, 1984. ACM Press. Google ScholarDigital Library
- Meunier, P., R. B. Findler, P. A. Steckler and M. Wand. Selectors make set-based analysis too hard. Higher Order and Symbolic Computation, 2005. To appear. Google ScholarDigital Library
- Milner, R., M. Tofte, R. Harper and D. Macqueen. The Definition of Standard ML - Revised. MIT Press, Cambridge, MA, USA, 1997. Google ScholarDigital Library
- Palsberg, J. Closure analysis in constraint form. Proc. ACM Trans. on Programming Languages and Systems, 17(1):47--62, Jan. 1995. Google ScholarDigital Library
- Palsberg, J. and C. Pavlopoulou. From polyvariant flow information to intersection and union types. In Conference Record of POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, pages 197--208, New York, NY, 1998. Google ScholarDigital Library
- Palsberg, J. and M. I. Schwartzbach. Object-Oriented Type Systems. Wiley Professional Computing. Wiley, Chichester, 1994. Google ScholarDigital Library
- Probst, C. W. Modular control flow analysis for libraries. In SAS '02: Proceedings of the 9th International Symposium on Static Analysis, pages 165--179, London, UK, 2002. Springer-Verlag. Google ScholarDigital Library
- Shivers, O. The semantics of Scheme control-flow analysis. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, volume 26(9), pages 190--198, New Haven, CN, June 1991. Google ScholarDigital Library
- Tang, Y. M. and P. Jouvelot. Separate abstract interpretation for control-flow analysis. In Hagiya, M. and J. C. Mitchell, editors, Theoretical Aspects of Computer Software, pages 224--243. Springer, Berlin, Heidelberg, 1994. Google ScholarDigital Library
- Wand, M. Finding the source of type errors. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 38--43, 1986. Google ScholarDigital Library
- Wand, M. and G. B. Williamson. A modular, extensible proof method for small-step flow analyses. In Métayer, D. L., editor, Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, Grenoble, France, April 8-12, 2002, Proceedings, volume 2305 of Lecture Notes in Computer Science, pages 213--227, Berlin, 2002. Springer-Verlag. Google ScholarDigital Library
- Wells, J. B., A. Dimock, R. Muller and F. Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Programming, 12(3):183--227, May 2002. Google ScholarDigital Library
- Wright, A. K. and S. Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst., 20(1):166--207, 1998. Google ScholarDigital Library
Index Terms
- Modular set-based analysis from contracts
Recommendations
Modular set-based analysis from contracts
Proceedings of the 2006 POPL ConferenceIn 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 ...
From Contracts to E-Contracts: Modeling and Enactment
Contracts are complex to understand, represent and process electronically. Usually, contracts involve various entities such as parties, activities and clauses. An e-contract is a contract modeled, specified, executed and enacted (controlled and ...
Visualization of Exception Propagation for Java Using Static Analysis
SCAM '02: Proceedings of the Second IEEE International Workshop on Source Code Analysis and ManipulationIn this paper, we first present a static analysis based on set-based framework, which estimates exception propagation paths of Java programs. We construct an exception propagation graph from the static analysis information, which includes the origin of ...
Comments