PLT MzLib: Libraries Manual

MzLib's contract.ss library defines new forms of expression that specify contracts and new forms of expression that attach contracts to values.

This section describes two classes of contracts: contracts for flat values (described in section 12.1) and contracts for functions (described in section 12.2).

In addition, this section describes two forms for establishing a contract on a value (described in section 12.4).

12.1 Flat Contracts

A contract for a flat value can be a predicate that accepts the value and returns a boolean indicating if the contract holds.

For better error reporting, a flat contract can be constructed with flat-named-contract, a procedure that accepts two arguments. The first argument must be a string that describes the type that the predicate checks for. The second argument is the predicate itself.

In addition, this library provides many helper functions for constructing contracts.

union accepts any number of predicates and at most one function contract and returns a contract that corresponds to the union of them all.

and/f accepts a list of predicates and returns a predicate that is the conjunction of those predicates.

or/f accepts a list of predicates and returns a predicate that is the disjuction of those predicates.

>=/c accepts a number and returns a predicate that requires the input to be a number and greater than or equal to the original input.

<=/c accepts a number and returns a predicate that requires the input to be a number and less than or equal to the original input.

>/c accepts a number and returns a predicate that requires the input to be a number and greater than the original input.

</c accepts a number and returns a predicate that requires the input to be a number and less than the original input.

integer-in accepts two numbers and returns a predicate that recognizes if integers between the two inputs.

real-in accepts two numbers and returns a predicate that recognizes real numbers between the two inputs.

natural-number? returns #t if the input is a natural number and #f otherwise.

string/len accepts a number and returns a predicate that recognizes strings that have fewer than that number of characters.

printable? returns #t for any value that can be written out and read back in.

any? is a predicate that always returns #t. If you are using this predicate as the result portion of a function contract, consider using any instead. It behaves the same, in that one restrictive context, but has better memory performance.

symbols accepts any number of symbols and returns a predicate that checks for those symbols.

is-a?/c accepts a class or interface and returns a predicate that checks if objects are subclasses of the class or implement the interface.

implementation?/c accepts an interface and returns a predicate that checks if classes are implement the given interface.

subclass?/c accepts a class and returns a predicate that checks if classes are subclasses of the original class.

listof accepts a flat contract and returns a predicate that checks for lists whose elements match the original predicate.

vectorof accepts a flat contract and returns a predicate that checks for vectors whose elements match the original predicate.

vector/p accepts any number of flat contract and returns a predicate that checks for vectors. The number of elements in the vector must match the number of arguments supplied to vector/p and the elements of the vector must match the corresponding flat contract.

box/p accepts a flat contract and returns a flat contract that checks for boxes whose contents match box/p's argument.

cons/p accepts two predicates and returns a predicate that checks for cons cells whose car and cdr correspond to cons/p's two arguments.

list/p accepts an arbitrary number of arguments and returns a predicate that checks for lists whose length is the same as the number of arguments to list/p and whose elements match those arguments.

mixin-contract is a contract that matches mixins. It is a function contract. It guarantees that the input to the function is a class and the result of the function is a subclass of the input.

make-mixin-contract is a function that constructs mixins contracts. It accepts any number of classes and interfaces and returns a function contract. The function contract guarantees that the input to the function implements the interfaces and is derived from the classes and that the result of the function is a subclass of the input.

12.2 Function Contracts

This section describes the contract constructors for function contracts. This is their shape:

contract-expr ::==
 | (case-> arrow-contract-expr ...)
 | arrow-contract-expr

arrow-contract-expr ::== 
 | (-> expr ... expr)
 | (-> expr ... any)
 | (-> expr ... (values expr ...))
 | (->* (expr ...) (expr ...))
 | (->* (expr ...) expr (expr ...))
 | (->* (expr ...) expr any)
 | (->d expr ... expr)
 | (->*d (expr ...) expr)
 | (->*d (expr ...) expr expr)
 | (opt-> (expr ...) (expr ...) expr)
 | (opt->* (expr ...) (expr ...) (expr ...))

The -> contract is for functions that accept a fixed number of arguments and return a single result. The last argument to -> is the contract on the result of the function and the other arguments are the contracts on the arguments to the function. Each of the arguments to -> must be another contract expression or a predicate. For example, this expression:

(integer? boolean? . -> . integer?)

is a contract on functions of two arguments. The first must be an integer and the second a boolean and the function must return an integer. (This example uses MzScheme's infix notation so that the -> appears in a suggestive place; see section 14.3 in PLT MzScheme: Language Manual).

If any is used as the last argument to ->, no contract checking is performed on the result of the function, and tail-recursion is preserved. Except for the memory performance, this is the same as using any? in the result.

The final case of -> expressions treats values as a local keyword - that is, you may not return multiple values to this position, instead if the word values syntactically appears in the in the last argument to -> the function is treated as a multiple value return (this is a shorthand for the two argument variant on ->*).

The ->* expression is for functions that return multiple results and/or have rest arguments. If two arguments are supplied, the first is the contracts on the arguments to the function and the second is the contract on the results of the function. If three arguments are supplied, the first argument contains the contracts on the arguments to the function (excluding the rest argument), the second contains the contract on the rest argument to the function and the final argument is the contracts on the results of the function. The final argument can be any which, like -> means that no contract is enforced on the result of the function and tail-recursion is preserved.

The ->d and ->*d contract constructors are like their d-less counterparts, except that the result portion is a function that accepts the original arguments to the function and returns the range contracts. The range contract function for ->*d must return multiple values: one for each result of the original function. As an example, this is the contract for sqrt:

(number? 
 . ->d .
 (lambda (in)
   (lambda (out)
     (and (number? out)
          (abs (- (* out out) in) 0.01)))))

It says that the input must be a number and that the difference between the square of the result and the original number is less than 0.01.

The case-> expression constructs a contract for case-lambda function. It's arguments must all be function contracts, built by one of ->, ->d, ->*, or ->*d.

The opt-> expression constructs a contract for an opt-lambda function. The first arguments are the required parameters, the second arguments are the optional parameters and the final argument is the result. Each opt-> expression expands into case->.

The opt->* expression constructs a contract for an opt-lambda function. The only difference between opt-> and opt->* is that multiple return values are permitted with opt->* and they are specified in the last clause of an opt->* expression.

12.3 Class contracts

This section describes the contract constructors for class contracts. This is their shape:

contract-expr ::== ...
 | (class-contract 
     (method-spec method-name arrow-contract-spec) ...)

method-spec ::==
   public
 | override

These contracts protect class expressions and the invocation of their methods. In addition to the argument and result checks performed when methods are called and returned, these contracts aslo ensure behavioral substitutability for derived classes. That is, an instance of a subclass should be substitutable in contexts expecting the original class. This means that the pre-condition contract of the original class must imply the pre-condition contract of the subclass and the post-condition contract of the subclass must imply the post-condition contract of the original class.

12.4 Attaching Contracts to Scheme Values

There are four special forms that attach contract specification to values: provide/contract, define/contract, contract, and contract-=>.

p/c-item is one of
  (struct identifier ((identifier contract-expr) ...))
  (id contract-expr)

A provide/contract form can only appear at the top-level of a module (see section 5 in PLT MzScheme: Language Manual). As with provide, each identifier is provided from the module. In addition, clients of the module must live up to the contract specified by expr.

The provide/contract form treats modules as units of blame. The module that defines the provided variable is expected to meet the position (co-variant) positions of the contract. Each module that imports the provided variable must obey the negative (contract-variant) positions of the contract.

The struct form of a provide/contract clause provides a structure definition. Each field has a contract that dictates the contents of the fields.

The define/contract form attaches the contract contract-expr to init-value-expr and binds that to id.

The define/contract form treats individual definitions as units of blame. The definition itself is responsible for positive (co-variant) positions of the contract and each reference to id (including those in the initial value expression) must meet the negative positions of the contract.

Error messages with define/contract are not as clear as those provided by provide/contract because define/contract cannot detect the name of the definition where the reference to the defined variable occurs. Instead, it uses the source location of the reference to the variable as the name of that definition.

(contract contract-expr to-protect-expr positive-blame negative-blame) SYNTAX

(contract contract-expr to-protect-expr positive-blame negative-blame contract-source) SYNTAX

The contract special form is the primitive mechanism for attaching a contract to a value. Its purpose is as a target for the expansion of some higher-level contract specifying form.

(contract expr to-protect-expr positive-blame negative-blame contract-source)

The contract expression adds the contract specified by the first argument to the value in the second argument. The result of a contract expression is the result of the to-protect-expr expression, but with the contract specified by contract-expr enforced on to-protect-expr. The expressions positive-blame and negative-blame must be symbols indicating how to assign blame for positive and negative positions of the contract specified by contract-expr. Finally, contract-source, if specified, indicates where the contract was assumed. It must be a syntax object specifying the source location of the location where the contract was assumed. If the syntax object wraps a symbol, the symbol is used as the name of the primitive whose contract was assumed. If absent, it defaults to the source location of the contract expression.

(contract-=> contract-antecedent-expr contract-consequent-expr to-test-expr to-be-blamed) SYNTAX

(contract-=> contract-antecedent-expr contract-consequent-expr to-test-expr to-be-blamed contract-source) SYNTAX

Like the contract form, this is a primitive contract checking form that is intended for using by higher-level contract checking macros only.

This form checks that the contract-antecedent-expr contract implies the contract-consequent-expr, at least for the value of to-test-expr. If the implication does not hold, to-be-blamed is blamed for the contract violation.

12.5 Contract Utility

The procedure contract? returns #t if its argument was constructed with one of the arrow constructors described earlier in this section, or if its argument is a procedure of arity 1.

Chapter 12 contract.ss: Contracts

12.1 Flat Contracts

12.2 Function Contracts

12.3 Class contracts

12.4 Attaching Contracts to Scheme Values

12.5 Contract Utility

Chapter 12

`contract.ss`: Contracts