Article

Modular set-based analysis from contracts

Authors:

Philippe Meunier,

Robert Bruce Findler,

Matthias FelleisenAuthors Info & Claims

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 218 - 231

https://doi.org/10.1145/1111037.1111057

Published: 11 January 2006 Publication History

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]

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.

Digital Library

[2]

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.

Digital Library

[3]

Amadio, R. M. and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575--631, September 1993.

Digital Library

[4]

Bourdoncle, F. Abstract debugging of higher-order imperative languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 46--55, 1993.

Digital Library

[5]

Cartwright, R. and M. Fagan. Soft typing. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 278--292, 1991.

Digital Library

[6]

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.

Digital Library

[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]

Findler, R. B. and M. Felleisen. Contracts for higher-order functions. In ACM SIGPLAN International Conference on Functional Programming, 2002.

Digital Library

[9]

Flanagan, C. Hybrid type checking. In Proceedings of the symposium on Principles of Programming Languages, 2006. In this volume.

Digital Library

[10]

Flanagan, C. and M. Felleisen. Componential set-based analysis. ACM Trans. on Programming Languages and Systems, 21(2):369--415, Feb. 1999.

Digital Library

[11]

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.

Digital Library

[12]

Flatt, M. Composable and compilable macros: You want it when? In ACM SIGPLAN International Conference on Functional Programming, 2002.

Digital Library

[13]

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.

Digital Library

[14]

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.

Digital Library

[15]

Haack, C. and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Sci. Comput. Programming, 50:189--224, 2004.

Digital Library

[16]

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.

Digital Library

[17]

Henglein, F. Dynamic typing. In Proceedings of the 4th European Symposium on Programming, pages 233--253, London, UK, 1992. Springer-Verlag.

Digital Library

[18]

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.

Digital Library

[19]

Leroy, X., D. Doligez, J. Garrigue, D. Rémy and J. Vouillon. The Objective Caml system -- documentation and user's manual, 2005.

[20]

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.

Digital Library

[21]

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.

Digital Library

[22]

Milner, R., M. Tofte, R. Harper and D. Macqueen. The Definition of Standard ML - Revised. MIT Press, Cambridge, MA, USA, 1997.

Digital Library

[23]

Palsberg, J. Closure analysis in constraint form. Proc. ACM Trans. on Programming Languages and Systems, 17(1):47--62, Jan. 1995.

Digital Library

[24]

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.

Digital Library

[25]

Palsberg, J. and M. I. Schwartzbach. Object-Oriented Type Systems. Wiley Professional Computing. Wiley, Chichester, 1994.

Digital Library

[26]

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.

Digital Library

[27]

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.

Digital Library

[28]

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.

Digital Library

[29]

Wand, M. Finding the source of type errors. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 38--43, 1986.

Digital Library

[30]

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.

Digital Library

[31]

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.

Digital Library

[32]

Wright, A. K. and S. Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst., 20(1):166--207, 1998.

Digital Library

Cited By

Qian KSmith SStride BWeng SWu K(2024)Semantic-Type-Guided Bug FindingProceedings of the ACM on Programming Languages10.1145/36897888:OOPSLA2(2183-2210)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689788
Campora JKhan MChen S(2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632931
Moy CNguyễn PTobin-Hochstadt SVan Horn D(2021)Corpse reviver: sound and efficient gradual typing via contract verificationProceedings of the ACM on Programming Languages10.1145/34343345:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434334
Show More Cited By

Index Terms

Modular set-based analysis from contracts

Recommendations

Modular set-based analysis from contracts
Proceedings of the 2006 POPL Conference

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 ...
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 Manipulation

In 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2006

432 pages

ISBN:1595930272

DOI:10.1145/1111037

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Simon Peyton Jones
Microsoft Research, UK

ACM SIGPLAN Notices Volume 41, Issue 1
Proceedings of the 2006 POPL Conference
January 2006
421 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1111320
Issue’s Table of Contents

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL06

Sponsor:

POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006

January 11 - 13, 2006

South Carolina, Charleston, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

39
Total Citations
View Citations
434
Total Downloads

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

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Qian KSmith SStride BWeng SWu K(2024)Semantic-Type-Guided Bug FindingProceedings of the ACM on Programming Languages10.1145/36897888:OOPSLA2(2183-2210)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689788
Campora JKhan MChen S(2024)Type-Based Gradual Typing Performance OptimizationProceedings of the ACM on Programming Languages10.1145/36329318:POPL(2667-2699)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632931
Moy CNguyễn PTobin-Hochstadt SVan Horn D(2021)Corpse reviver: sound and efficient gradual typing via contract verificationProceedings of the ACM on Programming Languages10.1145/34343345:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434334
Greenman BFelleisen M(2018)A spectrum of type soundness and performanceProceedings of the ACM on Programming Languages10.1145/32367662:ICFP(1-32)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236766
NGUYÊN PTOBIN-HOCHSTADT SVAN HORN D(2016)Higher order symbolic execution for contract verification and refutationJournal of Functional Programming10.1017/S095679681600021627Online publication date: 21-Dec-2016
https://doi.org/10.1017/S0956796816000216
Ohori AUeno KHoshi KNozaki SSato TMakabe TIto Y(2014)SML# in industryACM SIGPLAN Notices10.1145/2692915.262816449:9(167-173)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628164
Nguyen PTobin-Hochstadt SVan Horn D(2014)Soft contract verificationACM SIGPLAN Notices10.1145/2692915.262815649:9(139-152)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628156
Mulligan DOwens SGray KRidge TSewell P(2014)LemACM SIGPLAN Notices10.1145/2692915.262814349:9(175-188)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628143
Breitner JEisenberg RPeyton Jones SWeirich S(2014)Safe zero-cost coercions for HaskellACM SIGPLAN Notices10.1145/2692915.262814149:9(189-202)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628141
Winograd-Cort DHudak P(2014)Settable and non-interfering signal functions for FRPACM SIGPLAN Notices10.1145/2692915.262814049:9(213-225)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628140
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