188宝金博页面版

Contracts for Higher-Order FunctionsRobert Bruce Findler1Matthias FelleisenNortheastern UniversityCollege of Computer ScienceBoston, Massachusetts 021 1 5, USAAbstractAssertions play an important role in the construction ofrobust soft-ware. Their use in programming languages dates back to the 1970s.Eiffel, an object-oriented programming language, wholeheartedlyadopted assertions and developed the “Design by Contract” philos-ophy. Indeed, the entire object-oriented community recognizes thevalue of assertion-based contracts on methods.In contrast, languages with higher-order functions do not supportassertion-based contracts.Because predicates on functions are,in general, undecidable, specifying such predicates appears to bemeaningless.Instead, the functional languages community de-veloped type systems that statically approximate interesting pred-icates.In this paper, we show how to support higher-order function con-tracts in a theoretically well-founded and practically viable man-ner. Specifically, we introduce λCON, a typed lambda calculus withassertions for higher-order functions. The calculus models the as-sertion monitoring system that we employ in DrScheme. We es-tablish basic properties of the model (type soundness, etc.) andillustrate the usefulness of contract checking with examples fromDrScheme’s code base.We believe that the development of an assertion system for higher-order functions serves two purposes. On one hand, the system hasstrong practical potential because existing type systems simply can-not express many assertions that programmers would like to state.On the other hand, an inspection of a large base of invariants mayprovide inspiration for the direction of practical future type systemresearch.Categories & Subject Descriptors: D.3.3, D.2.1; General Terms: De-sign, Languages, Reliability; Keywords: Contracts, Higher-order Func-tions, Behavioral Specifications, Predicate Typing, Software Reliability1Work partly conducted at Rice University, Houston TX. Address as of9/2002: University of Chicago; 1100 E 58th Street; Chicago, IL 60637Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.ICFP’02, October 4-6, 2002, Pittsburgh, Pennsylvania, USA.Copyright 2002 ACM 1-58113-487-8/02/0010 ...$5.001IntroductionDynamically enforced pre- and post-condition contracts have beenwidely used in procedural and object-oriented languages [11, 14,17, 20, 21, 22, 25, 31]. As Rosenblum [27] has shown, for example,these contracts have great practical value in improving the robust-ness ofsystems in procedural languages. Eiffel [22] even developedan entire philosophy of system design based on contracts (“Designby Contract”). Although Java [12] does not support contracts, it isone ofthe most requested extensions.1With one exception, higher-order languages have mostly ignoredassertion-style contracts. The exception is Bigloo Scheme [28],where programmers can write down first-order, type-like con-straints on procedures. These constraints are used to generate moreefficient code when the compiler can prove they are correct and areturned into runtime checks when the compiler cannot prove themcorrect.First-order procedural contracts have a simple interpretation. Con-sider this contract, written in an ML-like syntax:f : int[9]int[0,99]val rec fλ x.It states that the argument to f must be an int greater than 9 andthat f produces an int between 0 and 99. To enforce this contract, acontract compiler inserts code to check that x is in the proper rangewhen f is called and that f’s result is in the proper range when freturns. If x is not in the proper range, f’s caller is blamed fora contractual violation. Symmetrically, if f’s result is not in theproper range, the blame falls on f itself. In this world, detectingcontractual violations and assigning blame merely means checkingappropriate predicates at well-defined points in the program’s eval-uation.This simple mechanism for checking contracts does not generalizeto languages with higher-order functions. Consider this contract:g : (int[val rec g9]int[0,99])λ proc.int[0,99]The contract’s domain states that g accepts intmust apply them to ints larger than 9. In turn, these functions mustproduce ints between 0 and 99. The contract’s range obliges g toproduce ints between 0 and 99.int functions and1http://developer.java.sun.com/developer/bugParade/top25rfes.html