Christos Dimoulas
Matthias Felleisen
Skip Abstract Section
Abstract
Behavioral software contracts have become a popular mechanism for specifying and ensuring logical claims about a program's flow of values. While contracts for first-order functions come with a natural interpretation and are well understood, the various incarnations of higher-order contracts adopt, implicitly or explicitly, different views concerning the meaning of contract satisfaction. In this article, we define various notions of contract satisfaction in terms of observational equivalence and compare them with each other and notions in the literature. Specifically, we introduce a small model language with higher-order contracts and use it to formalize different notions of contract satisfaction. Each of them demands that the contract parties satisfy certain observational equivalences.
- Ahmed, A. 2006. Step-indexed syntactic logical relations for recursive and quantified types. In Proceedings of the 15th European Symposium on Programming (ESOP). 69--83. Google Scholar
Digital Library
- Barnett, M., Leino, K. R. M., and Schulte, W. 2004. The Spec# programming system: an overview. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices, 49--69. Google ScholarDigital Library
- Beugnard, A., Jézéquel, J.-M., Plouzeau, N., and Watkins, D. 1999. Making components contract aware. IEEE Computer 32, 7, 38--45. Google ScholarDigital Library
- Blume, M. and McAllester, D. 2006. Sound and complete models of contracts. J. Funct. Prog. 16, 4--5, 375--414. Google ScholarDigital Library
- Bravetti, M. and Zavattaro, G. 2007. Towards a unifying theory for choreography conformance and contract compliance. In Preproceedings of the 6th Symposium on Software Composition. 34--50. Google ScholarDigital Library
- Carpineti, S., Castagna, G., Laneve, C., and Padovani, L. 2006. A formal account of contracts for web services. In Proceedings of the 3rd International Workshop on Web Services and Formal Methods (WS-FM). 148--162. Google ScholarDigital Library
- Castagna, G., Gesbert, N., and Padovani, L. 2008. A theory of contracts for web services. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 261--272. Google ScholarDigital Library
- Castagna, G. and Padovani, L. 2009. Contracts for mobile processes. In Proceedings of the 20th International Conference in Concurrency Theory (CONCUR). 211--228. Google ScholarDigital Library
- Chitil, O., McNeill, D., and Runciman, C. 2003. Lazy assertions. In Revised Papers of the 15th International Workshop on Implementation of Functional Languages (IFL). 1--19. Google ScholarDigital Library
- de Alfaro, L. and Henzinger, T. A. 2001. Interface automata. In Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Egineering (ESEC/FSE). 109--120. Google ScholarDigital Library
- Degen, M., Thiemann, P., and Wehr, S. 2010. Eager and delayed contract monitoring for call-by-value and call-by-name evaluation. J. Logic Algeb. Prog. 79, 7(Oct.), 515--549.Google ScholarCross Ref
- Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998. Extended static checking. Tech. rep. 158, Compaq SRC Research Report.Google Scholar
- Felleisen, M., Findler, R. B., and Flatt, M. 2009. Semantics Engineering with PLT Redex. MIT Press. Google ScholarDigital Library
- Findler, R. B. and Blume, M. 2006. Contracts as pairs of projections. In Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS). 226--241. Google ScholarDigital Library
- Findler, R. B. and Felleisen, M. 2002. Contracts for higher-order functions. In Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming (ICFP). 48--59. Google ScholarDigital Library
- Findler, R. B., Felleisen, M., and Blume, M. 2004. An investigation of contracts as projections. Tech. rep. TR-2004-02, Computer Science Department, University of Chicago.Google Scholar
- Findler, R. B., Guo, S., and Rogers, A. 2007. Lazy contract checking for immutable data structures. In Revised Papers of the 16th International Workshop on Implementation of Functional Languages (IFL). 111--128. Google ScholarDigital Library
- Findler, R. B., Latendresse, M., and Felleisen, M. 2001. Behavioral contracts and behavioral subtyping. In Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Egineering (ESEC/FSE). 229--236. Google ScholarDigital Library
- Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for Java. In Proceedings of the ACM SIGPLAN 2002 Conference on Proramming Language Design and Implementation (PLDI). 234--245. Google ScholarDigital Library
- Flatt, M. and PLT. 2010. Reference: Racket. Tech. rep. PLT-TR-2010-1, PLT Inc. http://racket-lang.org/tr1/.Google Scholar
- Greenberg, M., Pierce, B. C., and Weirich, S. 2010. Contracts made manifest. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 353--364. Google ScholarDigital Library
- Gronski, J. and Flanagan, C. 2007. Unifying hybrid types and contracts. In Proceedings of the 8th Symposium on Trends in Functional Programming (TFP). 54--69.Google Scholar
- Hennessy, M. 1988. Algebraic Theory of Processes. MIT Press. Google ScholarDigital Library
- Hinze, R., Jeuring, J., and Löh, A. 2006. Typed contracts for functional programming. In Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS). 208--235. Google ScholarDigital Library
- Knowles, K., Tomb, A., Gronski, J., Freund, S. N., and Flanagan, C. 2006. SAGE: Unified hybrid checking for first-class types, general refinement types, and dynamic. http://sage.soe.ucsc.edu/sage-tr.pdf.Google Scholar
- Koutavas, V. 2008. Reasoning about imperative and higher-order programs. Ph.D. thesis, Northeastern University. Google ScholarDigital Library
- Meyer, B. 1988. Object-oriented Software Construction. Prentice-Hall. Google ScholarDigital Library
- Meyer, B. 1991. Design by contract. In Advances in Object-Oriented Software Engineering, Prentice-Hall, 1--50.Google Scholar
- Meyer, B. 1992a. Applying design by contract. IEEE Computer 25, 10, 40--51. Google ScholarDigital Library
- Meyer, B. 1992b. Eiffel: The Language. Prentice-Hall. Google ScholarDigital Library
- Morris, J. H. 1968. Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology.Google Scholar
- Plotkin, G. D. 1975. Call-by-name, call-by-value, and the λ-calculus. Theoret. Comput. Sci. 1, 2, 125--159.Google ScholarCross Ref
- Plotkin, G. D. 1977. LCF considered as a programming language. Theoret. Comput. Sci. 5, 3, 223--255.Google ScholarCross Ref
- Rosenblum, D. S. 1995. A practical approach to programming with assertion. IEEE Trans. Softw. Eng. 21, 1, 15--31. Google ScholarDigital Library
- Sabry, A. and Felleisen, M. 1993. Reasoning about programs in continuation passing-style. Lisp Symb. Comput. 6, 3/4, 289--360. Google ScholarDigital Library
- Scott, D. S. 1976. Data types as lattices. SIAM J. Comput. 5, 3, 522--587.Google ScholarDigital Library
- Xu, D., Peyton Jones, S., and Claessen, K. 2009. Static contract checking for Haskell. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 41--52. Google ScholarDigital Library
Index Terms
- On contract satisfaction in a higher-order world
Recommendations
Blame assignment for higher-order contracts with intersection and union
ICFP '15We present an untyped calculus of blame assignment for a higher-order contract system with two new operators: intersection and union. The specification of these operators is based on the corresponding type theoretic constructions. This connection makes ...
Soft contract verification for higher-order stateful programs
Software contracts allow programmers to state rich program properties using the full expressive power of an object language. However, since they are enforced at runtime, monitoring contracts imposes significant overhead and delays error discovery. So ...
Higher-order symbolic execution via contracts
OOPSLA '12We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, thus enabling symbolic approximation of higher-order behavior.
Our approach is based on the idea ...
Comments