×

The interaction of contracts and laziness. (English) Zbl 1360.68325

Summary: Contract monitoring for strict higher-order functional languages has an intuitive meaning, an established theoretical basis, and a standard implementation. For lazy functional languages, the situation is less clear-cut. There is no agreed-upon intended meaning or theory, and there are competing implementations with subtle semantic differences.
This paper proposes meaning preservation and completeness as formally defined properties for evaluating implementations of contract monitoring. Both properties have definitions that can be checked by straightforward inductive proof. A survey of existing suggestions for lazy contract systems reveals that some are meaning preserving, some are complete, and some have neither property. The main result is that contract monitoring for lazy functional languages cannot be complete and meaning preserving at the same time, although each property can be achieved in isolation.

MSC:

68N18 Functional programming and lambda calculus
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Keywords:

contracts; laziness

Software:

Eiffel; Haskell; Racket
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abercrombie, P., Karaorman, M.: jContractor: design by contract for Java. http://jcontractor.sourceforge.net/ (2003) · Zbl 1086.68534
[2] Benton, N.; Kennedy, A., Monads, effects, and transformations, Paris, France, Sept. 1999, Amsterdam · Zbl 0958.68046
[3] Blume, M., McAllester, D.: Sound and complete models of contracts. J. Funct. Program. 16, 375-414 (2006) · Zbl 1122.68019 · doi:10.1017/S0956796806005971
[4] Chitil, O., A semantics for lazy assertions, PEPM ’11, Austin, Texas, USA, New York · doi:10.1145/1929501.1929527
[5] Chitil, O., Practical typed lazy contracts, Copenhagen, Denmark, New York · Zbl 1291.68112
[6] Chitil, O.; Huch, F.; Shao, Z. (ed.), Monadic prompt lazy assertions in Haskell, No. 4807, 38-53 (2007), Berlin
[7] Chitil, O.; Huch, F.; Horváth, Z. (ed.); Zsók, V. (ed.); Butterfield, A. (ed.), A pattern logic for prompt lazy assertions, Budapest, Hungary, Berlin
[8] Chitil, O.; McNeill, D.; Runciman, C.; Trinder, P. (ed.); Michaelson, G. (ed.); Pena, R. (ed.), Lazy assertions, Edinburgh, UK, Nov. 2004, Berlin · Zbl 1108.68346
[9] Degen, M.; Thiemann, P.; Wehr, S., True lies: lazy contracts for lazy languages, Lübeck, Germany
[10] Degen, M., Thiemann, P., Wehr, S.: Eager and delayed contract monitoring for call-by-value and call-by-name evaluation. J. Log. Algebr. Program. (2010). doi:10.1016/j.jlap.2010.07.006 · Zbl 1204.68071 · doi:10.1016/j.jlap.2010.07.006
[11] Degen, M.; Thiemann, P.; Wehr, S.; Kiselyov, O. (ed.); Thompson, S. (ed.), The interaction of contracts and laziness, Philadelphia, PA, USA, New York
[12] Dimoulas, C.; Tobin-Hochstadt, S.; Felleisen, M., Complete monitors for behavioral contracts, Tallinn, Estonia, Apr. 2012, Berlin · Zbl 1352.68031
[13] Fähndrich, M.; Barnett, M.; Logozzo, F.; Shin, S. Y. (ed.); Ossowski, S. (ed.); Schumacher, M. (ed.); Palakal, M. J. (ed.); Hung, C.-C. (ed.), Embedded contract languages, Sierre, Switzerland, New York
[14] Findler, R.B., Blume, M.: Contracts as pairs of projections. In: Wadler and Hagiya [31], pp. 226-241 · Zbl 1185.68193
[15] Findler, R.B., Blume, M., Felleisen, M.: An investigation of contracts as projections. Technical report TR-2004-02, University of Chicago, Computer Science Department (2004)
[16] Findler, R. B.; Felleisen, M.; Peyton-Jones, S. (ed.), Contracts for higher-order functions, Pittsburgh, PA, USA, Oct. 2002, New York · Zbl 1322.68039
[17] Flatt, M., PLT: Reference: Racket. Technical report PLT-TR-2010-1, PLT Inc, (2010) http://racket-lang.org/tr1/
[18] Greenberg, M.; Pierce, B. C.; Weirich, S.; Palsberg, J. (ed.), Contracts made manifest, Madrid, Spain, Jan. 2010, New York · Zbl 1312.68133
[19] Gronski, J.; Knowles, K.; Tomb, A.; Freund, S. N.; Flanagan, C., Sage: hybrid checking for flexible specifications (2006)
[20] Hanus, M., Lazy and faithful assertions for functional logic programs, Universidad Politécnica de Madrid
[21] Hinze, R., Jeuring, J., Löh, A.: Typed contracts for functional programming. In: Wadler and Hagiya [31], pp. 208-225 · Zbl 1185.68195
[22] Kinsey, Ø.S.: jsContract (2010). http://kinsey.no/projects/jsContract/
[23] Kramer, R., iContract — the Java design by contract tool, Santa Barbara, CA, USA, Los Alamitos
[24] Meyer, B.: Applying “Design by contract”. IEEE Comput. 25(10), 40-51 (1992) · doi:10.1109/2.161279
[25] Meyer, B.: Eiffel: the Language. Prentice-Hall, New York (1992) · Zbl 0779.68013
[26] Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Upper Saddle River (1997) · Zbl 0987.68516
[27] Ou, X.; Tan, G.; Mandelbaum, Y.; Walker, D.; Lévy, J.-J. (ed.); Mayr, E. W. (ed.); Mitchell, J. C. (ed.), Dynamic typing with dependent types, 437-450 (2004), Norwell · Zbl 1088.68531
[28] Peyton Jones, S. (ed.): Haskell 98 Language and Libraries, the Revised Report. Cambridge University Press, Cambridge (2003) · Zbl 1067.68041
[29] Sun Microsystems: Project Fortress website (2008). http://projectfortress.sun.com/
[30] Wadler, P.; Findler, R. B.; Castagna, G. (ed.), Well-typed programs can’t be blamed, York, UK, Berlin · Zbl 1234.68063
[31] Wadler, P., Hagiya, M. (eds.): Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, Fuji Susono, Japan, Apr. 2006. Springer, Berlin (2006) · Zbl 1103.68004
[32] Xu, D. N.; Peyton Jones, S.; Claessen, K.; Pierce, B. (ed.), Static contract checking for Haskell, Savannah, GA, USA, Jan. 2009, New York · Zbl 1315.68107
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.