++ ++ This section illustrates the current state of PLT Scheme's contract + implementation with a series of examples from Mitchell and McKim's text + book "Design by Contract, by Example" [Addison and Wesley, 2002]. +
+
Mitchell and McKim's principles for design by contract DbC are derived + from the 1970s style algebraic specifications. The overall goal of DbC is + to specify the constructors of an algebra in terms of its + observers. While we reformulate Mitchell and McKim's terminology, we + retain their terminology of "classes" and "objects" even though we + reformulate their examples in an applicative style (as well as an + imperative one): +
+ +A query returns a result but does not change the observable + properties of an object. A command changes the visible + properties of an object, but does not return a result. In applicative + implementation a command typically returns an new object of the same + class.
+A derived query returns a result that is computable in + terms of basic queries.
++diff --git a/collects/scribblings/guide/contract-examples/1.ss b/collects/scribblings/guide/contract-examples/1.ss new file mode 100644 index 0000000000..1ecb08ac7d --- /dev/null +++ b/collects/scribblings/guide/contract-examples/1.ss @@ -0,0 +1,123 @@ +;; chapter 1: A Customer Manager Component for Managing Customer Relationships + +;; --- common data definitions ------------------------------------------------ + +(module basic-customer-details mzscheme + (require (lib "contract.ss")) + + ;; data definitions + + (define id? symbol?) + (define id-equal? eq?) + (define-struct basic-customer (id name address)) + + ;; interface + (provide/contract + [id? (-> any/c boolean?)] + [id-equal? (-> id? id? boolean?)] + [struct basic-customer ((id id?) (name string?) (address string?))]) + ;; end of interface + ) + +;; --- the customer manager ---------------------------------------------------- + +(module customer-manager mzscheme + (require (lib "contract.ss") (lib "etc.ss") (lib "list.ss")) + + (require basic-customer-details) + + ;; implementation + ;; [listof (list basic-customer? secret-info)] + (define all '()) + + (define (find c) + (define (has-c-as-key p) (id-equal? (basic-customer-id (car p)) c)) + (define x (filter has-c-as-key all)) + (if (pair? x) (car x) x)) + + (define (active? c) + (define f (find c)) + (pair? (find c))) + + (define not-active? (compose not active? basic-customer-id)) + + (define count 0) + + (define (add c) + (set! all (cons (list c 'secret) all)) + (set! count (+ count 1))) + + (define (name id) + (define bc-with-id (find id)) + (basic-customer-name (car bc-with-id))) + + (define (set-name id name) + (define bc-with-id (find id)) + (set-basic-customer-name! (car bc-with-id) name)) + + (define c0 0) + ;; end of implementation + + ;; interface + (provide/contract + ;; how many customers are in the db? + [count natural-number/c] + ;; is the customer with this id active? + [active? (-> id? boolean?)] + ;; what is the name of the customer with this id? + [name (-> (and/c id? active?) string?)] + ;; change the name of the customer with this id + [set-name (->pp ([id id?] [nn string?]) + #t ;; no additional precondition + any/c ;; result contract + ____ ;; the result's name (irrelevant) + ;; the postcondition + (string=? (name id) nn))] + ;; add a customer + [add (->d (and/c basic-customer? not-active?) + (lambda (bc) + (let ([c0 count]) + (lambda (void) (> count c0)))))] + #; + [add (->pp ([bc (and/c basic-customer? not-active?)]) + ;; A pre-post condition contract must use a side-effect + ;; to express this contract via post-conditions + (set! c0 count) ;; pre + any/c ;; result contract + _____ ;; result name + (> count c0))]) + ;; end of interface + ) + +;; --- tests ------------------------------------------------------------------- + +(module test mzscheme + (require (planet "test.ss" ("schematics" "schemeunit.plt" 1 2)) + (planet "text-ui.ss" ("schematics" "schemeunit.plt" 1 2))) + (require basic-customer-details customer-manager) + + (add (make-basic-customer 'mf "matthias" "brookstone")) + (add (make-basic-customer 'rf "robby" "beverly hills park")) + (add (make-basic-customer 'fl "matthew" "pepper clouds town")) + (add (make-basic-customer 'sk "shriram" "i city")) + + (test/text-ui + (make-test-suite + "manager" + (make-test-case + "id lookup" + (assert equal? "matthias" (name 'mf))) + (make-test-case + "count" + (assert = 4 count)) + (make-test-case + "active?" + (assert-true (active? 'mf))) + (make-test-case + "active? 2" + (assert-false (active? 'kk))) + (make-test-case + "set name" + (assert-true (void? (set-name 'mf "matt"))))))) + +(require test) diff --git a/collects/scribblings/guide/contract-examples/2.ss b/collects/scribblings/guide/contract-examples/2.ss new file mode 100644 index 0000000000..b38b627050 --- /dev/null +++ b/collects/scribblings/guide/contract-examples/2.ss @@ -0,0 +1,105 @@ +;; chapter 2: A Parameteric (Simple) Stack + +;; --- stack ------------------------------------------------------------------- + +(module stack mzscheme + (require (lib "contract.ss") (lib "etc.ss")) + + ;; a contract utility + (define (eq/c x) (lambda (y) (eq? x y))) + + ;; implementation + (define-struct stack (list p? eq)) + + (define (initialize p? eq) (make-stack '() p? eq)) + (define (push s x) + (make-stack (cons x (stack-list s)) (stack-p? s) (stack-eq s))) + (define (item-at s i) (list-ref (reverse (stack-list s)) (- i 1))) + (define (count s) (length (stack-list s))) + (define (is-empty? s) (null? (stack-list s))) + (define not-empty? (compose not is-empty?)) + (define (pop s) (make-stack (cdr (stack-list s)) (stack-p? s) (stack-eq s))) + (define (top s) (car (stack-list s))) + ;; end of implementation + + ;; interface + (provide/contract + ;; predicate + [stack? (-> any/c boolean?)] + ;; primitive queries + ;; how many items are on the stack? + [count (-> stack? natural-number/c)] + ;; which item is at the given position? + [item-at (->r ([s stack?][i (and/c positive? (<=/c (count s)))]) + (stack-p? s))] + ;; derived queries + ;; is the stack empty? + [is-empty? (->d stack? (lambda (s) (eq/c (= (count s) 0))))] + ;; which item is at the top of the stack + [top (->pp ([s (and/c stack? not-empty?)]) + #t ;; no precondition + (stack-p? s) ;; a stack item + t ;; the name of the result + ;; the postcondition + ([stack-eq s] t (item-at s (count s))))] + ;; creation + [initialize (->r ([p contract?][s (p p . -> . boolean?)]) + ;; Mitchel and McKim use (= (count s) 0) here to express + ;; the post-condition in terms of a primitive query + (and/c stack? is-empty?))] + ;; commands + ;; add an item to the top of the stack + [push (->pp ([s stack?][x (stack-p? s)]) + #t ;; pre + stack? ;; result kind + sn ;; name of result + ;; post: + (and (= (+ (count s) 1) (count sn)) + ([stack-eq s] x (top sn))))] + ;; remove the item at the top of the stack + [pop (->pp ([s (and/c stack? not-empty?)]) + #t ;; pre + stack? ;; result kind + sn ;; name of result + ;; post: + (= (- (count s) 1) (count sn)))]) + ;; end of interface + ) + +;; --- tests ------------------------------------------------------------------- + +(module test mzscheme + (require (planet "test.ss" ("schematics" "schemeunit.plt" 1 2)) + (planet "text-ui.ss" ("schematics" "schemeunit.plt" 1 2))) + (require (lib "contract.ss")) + (require stack) + + (define s (push (push (initialize (flat-contract integer?) =) 2) 1)) + + (test/text-ui + (make-test-suite + "stack" + (make-test-case + "empty" + (assert-true (is-empty? (initialize (flat-contract integer?) =)))) + (make-test-case + "push" + (assert-true (stack? s))) + (make-test-case + "push exn" + ;; Noel & Ryan: this is how things should work: + #;(assert-exn exn:fail:contract? + (push (initialize (flat-contract integer?)) 'a)) + ;; this is what I have to do: + (assert-true (with-handlers ([exn:fail:contract? (lambda _ #t)]) + (push (initialize (flat-contract integer?)) 'a) + #f))) + (make-test-case + "pop" + (assert-true (stack? (pop s)))) + (make-test-case + "top" + (assert = (top s) 1)))) + ) + +(require test) diff --git a/collects/scribblings/guide/contract-examples/3.ss b/collects/scribblings/guide/contract-examples/3.ss new file mode 100644 index 0000000000..4249a0a80c --- /dev/null +++ b/collects/scribblings/guide/contract-examples/3.ss @@ -0,0 +1,107 @@ +;; chapter 3: A Dictionary + +;; --- dictionary -------------------------------------------------------------- + +(module dictionary mzscheme + (require (lib "contract.ss") (lib "etc.ss")) + + ;; a contract utility + (define-syntax => + (syntax-rules () + [(=> antecedent consequent) (if antecedent consequent #t)])) + + + ;; implementation + (define-struct dictionary (l value? eq?)) + ;; the keys should probably be another parameter (exercise) + + (define (initialize p eq) (make-dictionary '() p eq)) + (define (put d k v) + (make-dictionary (cons (cons k v) (dictionary-l d)) + (dictionary-value? d) + (dictionary-eq? d))) + (define (remove d k) + (make-dictionary + (let loop ([l (dictionary-l d)]) + (cond + [(null? l) l] + [(eq? (caar l) k) (loop (cdr l))] + [else (cons (car l) (loop (cdr l)))])) + (dictionary-value? d) + (dictionary-eq? d))) + (define (count d) (length (dictionary-l d))) + (define (value-for d k) (cdr (assq k (dictionary-l d)))) + (define (has? d k) (pair? (assq k (dictionary-l d)))) + (define (not-has? d) (lambda (k) (not (has? d k)))) + ;; end of implementation + + ;; interface + (provide/contract + ;; predicates + [dictionary? (-> any/c boolean?)] + ;; basic queries + ;; how many items are in the dictionary? + [count (-> dictionary? natural-number/c)] + ;; does the dictionary define key k? + [has? (->pp ([d dictionary?][k symbol?]) + #t ;; pre + boolean? + result + ((zero? (count d)) . => . (not result)))] + ;; what is the value of key k in this dictionary? + [value-for (->r ([d dictionary?] + [k (and/c symbol? (lambda (k) (has? d k)))]) + (dictionary-value? d))] + ;; initialization + ;; post condition: for all k in symbol, (has? d k) is false. + [initialize (->r ([p contract?][eq (p p . -> . boolean?)]) + (and/c dictionary? (compose zero? count)))] + ;; commands + ;; Mitchell and McKim say that put shouldn't consume Void (null ptr) for v. + ;; We allow the client to specify a contract for all values via initialize. + ;; We could do the same via a key? parameter (exercise). + ;; add key k with value v to this dictionary + [put (->pp ([d dictionary?] + [k (and symbol? (not-has? d))] + [v (dictionary-value? d)]) + #t + dictionary? + result + (and (has? result k) + (= (count d) (- (count result) 1)) + ([dictionary-eq? d] (value-for result k) v)))] + ;; remove key k from this dictionary + [remove (->pp ([d dictionary?] + [k (and/c symbol? (lambda (k) (has? d k)))]) + #t + (and/c dictionary? not-has?) + result + (= (count d) (+ (count result) 1)))]) + ;; end of interface + ) + +;; --- tests ------------------------------------------------------------------- + +(module test mzscheme + (require (planet "test.ss" ("schematics" "schemeunit.plt" 1 2)) + (planet "text-ui.ss" ("schematics" "schemeunit.plt" 1 2))) + (require (lib "contract.ss")) + (require dictionary) + + (define d + (put (put (put (initialize (flat-contract integer?) =) 'a 2) 'b 2) 'c 1)) + + (test/text-ui + (make-test-suite + "dictionaries" + (make-test-case + "value for" + (assert = (value-for d 'b) 2)) + (make-test-case + "has?" + (assert-false (has? (remove d 'b) 'b))) + (make-test-case + "count" + (assert = 3 (count d)))))) + +(require test) diff --git a/collects/scribblings/guide/contract-examples/5.ss b/collects/scribblings/guide/contract-examples/5.ss new file mode 100644 index 0000000000..a80e63d4a9 --- /dev/null +++ b/collects/scribblings/guide/contract-examples/5.ss @@ -0,0 +1,102 @@ +;; chapter 5: A Queue + +;; --- queue ------------------------------------------------------------------- + +;; Note: this queue doesn't implement the capacity restriction +;; of McKim and Mitchell's queue but this is really minor and easy to add. + +(module queue mzscheme + (require (lib "contract.ss") (lib "etc.ss")) + + ;; a contract utility + (define (all-but-last l) (reverse (cdr (reverse l)))) + (define (eq/c x) (lambda (y) (eq? x y))) + + ;; implementation + (define-struct queue (list p? eq)) + + (define (initialize p? eq) (make-queue '() p? eq)) + (define items queue-list) + (define (put q x) + (make-queue (append (queue-list q) (list x)) (queue-p? q) (queue-eq q))) + (define (count s) (length (queue-list s))) + (define (is-empty? s) (null? (queue-list s))) + (define not-empty? (compose not is-empty?)) + (define (remove s) (make-queue (cdr (queue-list s)) (queue-p? s) (queue-eq s))) + (define (head s) (car (queue-list s))) + + ;; interface + (provide/contract + ;; predicate + [queue? (-> any/c boolean?)] + ;; primitive queries + ;; Imagine providing this 'query' for the interface of the module + ;; only. Then in Scheme, there is no reason to have count or is-empty? + ;; around (other than providing it to clients). After all items is + ;; exactly as cheap as count. + [items (->d queue? (compose listof queue-p?))] + ;; derived queries + [count (->r ([q queue?]) + ;; We could express this second part of the post + ;; condition even if count were a module "attribute" + ;; in the language of Eiffel; indeed it would use the + ;; exact same syntax (minus the arrow and domain). + (and/c natural-number/c (=/c (length (items q)))))] + [is-empty? (->r ([q queue?]) + (and/c boolean? (eq/c (null? (items q)))))] + [head (->r ([q (and/c queue? (compose not is-empty?))]) + (and/c (queue-p? q) (eq/c (car (items q)))))] + ;; creation + [initialize (-> contract? (contract? contract? . -> . boolean?) + (and/c queue? (compose null? items)))] + ;; commands + [put (->r ([oldq queue?][i (queue-p? oldq)]) + (and/c queue? + (lambda (q) + (define old-items (items oldq)) + (equal? (items q) (append old-items (list i))))))] + [remove (->r ([oldq (and/c queue? (compose not is-empty?))]) + (and/c queue? + (lambda (q) + (equal? (cdr (items oldq)) (items q)))))]) + ;; end of interface + ) + +;; --- tests ------------------------------------------------------------------- + +(module test mzscheme + (require (planet "test.ss" ("schematics" "schemeunit.plt" 1 2)) + (planet "text-ui.ss" ("schematics" "schemeunit.plt" 1 2))) + (require (lib "contract.ss")) + (require queue) + + (define s (put (put (initialize (flat-contract integer?) =) 2) 1)) + + (test/text-ui + (make-test-suite + "queue" + (make-test-case + "empty" + (assert-true (is-empty? (initialize (flat-contract integer?) =)))) + (make-test-case + "put" + (assert-true (queue? s))) + (make-test-case + "count" + (assert = (count s) 2)) + (make-test-case + "put exn" + #;(assert-exn exn:fail:contract? + (push (initialize (flat-contract integer?)) 'a)) + (assert-true (with-handlers ([exn:fail:contract? (lambda _ #t)]) + (put (initialize (flat-contract integer?)) 'a) + #f))) + (make-test-case + "remove" + (assert-true (queue? (remove s)))) + (make-test-case + "head" + (assert = (head s) 2)))) + ) + +(require test) diff --git a/collects/scribblings/guide/contract-examples/6.ss b/collects/scribblings/guide/contract-examples/6.ss new file mode 100644 index 0000000000..b347a2715a --- /dev/null +++ b/collects/scribblings/guide/contract-examples/6.ss @@ -0,0 +1,20 @@ +;; chapter 6: Subclassing and Contracts + +;; In a subclass, an Eiffel programmer must use +;; ... require else ... +;; for preconditions, which or-s them together, and +;; ... ensure then ... +;; for postconditions, which and-s them together. + +;; See Findler's papers on inheritance and contracts for +;; an analysis of these mechanisms and their problems. + +;; prepare for subclassing with postconditions of the shape: + +;; precondition1 implies postcondition1 +;; and +;; ... +;; and +;; preconditionN implies postconditionN + +;; [Note: I am not sure about this one yet.] diff --git a/collects/scribblings/guide/contracts-class.scrbl b/collects/scribblings/guide/contracts-class.scrbl new file mode 100644 index 0000000000..a4cfaf0cfc --- /dev/null +++ b/collects/scribblings/guide/contracts-class.scrbl @@ -0,0 +1,7 @@ + + +Each of the followong questions (sections) corresponds to a chapter in + Mitchell and McKim's book (but not all chapters show up here). The + contracts have a colored background and appear in font so that they are easy to find. Implementations + are presented ahead of the interface in navy. + Finally, tests are included in a light shade. We + recommend that you read the contracts first, then the implementation, and + then the test module. +
+ ++ Mitchell and McKim use Eiffel as the underlying programming language and + employ a conventional imperative programming style. Our long-term goal is + to transliterate their examples into applicative Scheme, + structure-oriented imperative Scheme, and PLT Scheme's class system (when + contracts for those become available).
+ +Note: To mimic Mitchell and McKim's informal notion of parametericity + (parametric polymorphism), we use first-class contracts. At several + places, this use of first-class contracts improves on Mitchell and McKim's + design (see comments in interfaces). +
+ +
+ + + +diff --git a/collects/scribblings/guide/contracts-general-function.scrbl b/collects/scribblings/guide/contracts-general-function.scrbl new file mode 100644 index 0000000000..0df4769c0a --- /dev/null +++ b/collects/scribblings/guide/contracts-general-function.scrbl @@ -0,0 +1,667 @@ +#lang scribble/doc +@require[scribble/manual] +@require[scribble/eval] +@require["guide-utils.ss"] +@require["contracts-utils.ss"] +@(require (for-label scheme/contract)) + + + +
You wrote your module. You added contracts. You put them into the interface
+so that client programmers have all the information from interfaces. It's a
+piece of art:
+
++ +Clearly, @scheme[bank-client] is a module that uses @scheme[myaccount] +but what are the '?' doing there? Wouldn't it be nice if we had a name for this +class of data much like we have string, number, and so on? + ++bank-client broke the contract (-> ??? any) +it had with myaccount on deposit; +expected <???>, given: -10 ++
For this situation, PLT Scheme provides "flat named contracts". The use of
+"contract" shows that contracts are first-class values. The "flat" means that
+the collection of data is a subset of the built-in atomic classes of data; they
+are described by a predicate that consumes all Scheme values and produces a
+boolean. The "named" part says what we want to do: name the contract so that
+error messages become intelligible:
+
+
++ ++bank-client broke the contract (-> amount any) +it had with myaccount on deposit; +expected <amount>, given: -10 ++
Here is an excerpt from an imaginary (pardon the pun) numerics module:
+
+
In this particular case, the argument of @scheme[sqrt.v1] is greater +or equal to 1. Hence a very basic correctness check is that the result is +smaller than the argument. [Naturally, if this function is critical, one +could strengthen this check with additional clauses.] + +
In general, a dependent function contract checks the argument, then +applies the function in the range position to the argument, and uses the +result of this application (usually a closure) as the range check. + +
Let's look at a second example to see how this closure creating business
+works so well here. Take a look at the following module, which exports
+(among other things) a @scheme[deposit] function for a bank
+account. Whether the programmer implements this bank account imperatively
+or functionally, the balance of the account should increase when a customer
+deposits money:
+
+
+
The module implements the creation of accounts, balance checks, account +deposits, and many other functions presumably. In principle, the +@scheme[deposit] function consumes an account and an amount, adds the +amount to the account, and returns the (possibly modified) account. + +
To ensure the increase in the account's balance, the contract is a +dependent contract. The function on the right of the @scheme[->d] +contract combinator consumes the two argument values: an account and an +amount. It then returns a function that checks @scheme[deposit]'s +result. In this case, it checks whether the result is an account and +whether @scheme[balance0] is smaller than the account's balance. Note +that @scheme[balance0] is the value that @scheme[balance] extracted +from the given account before the range-checking function was +produced. + +
Exactly! + +
The contract for @scheme[sqrt.v1] suggests that curried versions of +the numeric comparison operators would come in handy for defining contracts +and combining them with contract combinators such as @scheme[->d]. + +
Here is a revision of the
+@scheme[numerics] module that exploits these special contract
+combinators:
+
+
Thus in the above example, the contract for @scheme[sqrt.v2] makes +sure that its argument is greater or equal to 1.0 and that its result is +less than or equal to its argument. + +
Yes, there are many other contract combinators such as @scheme[<=/c] +and @scheme[>=/c], and it pays off to look them up in the contract +report section (of the mzlib manual). They simplify contracts tremendously +and make them more accessible to potential clients. + +
Eventually bank customers want their money back. Hence, a module that +implements a bank account must include a method for withdrawing money. Of +course, ordinary accounts don't let customers withdraw an arbitrary amount of +money but only as much as they have in the account. + +
Suppose the account module provides the following two functions:
+
+"the balance of the given account is greater than or equal to the given (withdrawal) amount." ++The postcondition is similar to the one for @scheme[deposit]: +
+"the balance of the resulting account is larger than (or equal to) than the one of the +given account." ++You could of course also formulate a full-fledged correctness condition, namely, +that the balance of the resulting account is equal to the balance of the given +one, plus the given amount. + +
The following module implements accounts imperatively and specifies the +conditions we just discussed: +
|
+ |
++ + +the contract definitions + + + + + + + + + + + + + +the exports + + + + + + + + + + +the function definitions + ++ |
The result contract is formed on the fly: @scheme[(mk-account-contract acc amt +> msg>)]. It is an application of a contract-producing function that +consumes an account, an amount, a comparison operator, and an error message (a +format string). The result is a contract. +
We all know that @scheme[+] in Beginner Scheme is a function that
+ consumes at least two numbers but, in principle, arbitrary
+ manner. Defining the function is easy:
+
Here is the contract:
+
The contracts for the required arguments are enclosed in an additional
+ pair of parentheses:
+
Finally, you may have noticed that the contract for the function range + of @scheme[plus] is also wrapped in a pair of parentheses. The reason + for those is that functions can return multiple values not just one, and + this is our next topic in this guide. +
Dybvig explains
+ the meaning and pragmatics of @scheme[case-lambda] with the following
+ example (among others):
+
+
The contract for such a function is formed with the @scheme[case->]
+ combinator, which combines as many functional contracts as needed:
+
In the case of @scheme[substring1], we also know that the indices
+ that it consumes ought to be natural numbers less than the length of the
+ given string. Since @scheme[case->] just combines arrow contracts,
+ adding such constraints is just a matter of strengthening the individual
+ contracts:
+
The function @scheme[split] consumes a list of @scheme[char]s
+ and delivers the string that occurs before the first occurrence of
+ @scheme[#\newline] (if any) and the rest of the list:
+
+The contract for such a function can use the ordinary
+function arrow @scheme[->], since it
+treats @scheme[values] specially, when it appears as the
+last result:
+
The contract for such a function can also be written
+using @scheme[->*], just like
+ @scheme[plus]:
+
Now suppose we also want to ensure that the first result of
+ @scheme[split] is a prefix of the given word in list format. In that
+ case, we need to combine the @scheme[->*] contract combinator with the
+ @scheme[->d] combinator, which is of course the @scheme[->d*]
+ combinator:
+
This contract is expensive to check of course. Here is a slightly
+ cheaper version:
+
+Imagine yourself writing a contract for a function that accepts some other +function and a list of numbers that eventually applies the former to the +latter. Unless the arity of the given function matches the length of the +given list, your procedure is in trouble. +
+ + +Consider this @scheme[n-step] function:
+
+
| + |
+@scheme[ +;; Nat -> Nat +(define (f x) + (printf "~s \n" x) + (if (= x 0) #f -1)) + +(n-step f '(2)) +] |
++ | @scheme[ +;; Nat Nat -> Nat +(define (g x y) + (define z (+ x y)) + (printf "~s\n" (list x y z)) + (if (= z 0) #f -1)) + +(n-step g '(1 1)) +] |
A contract for @scheme[n-step] must specify two aspects of +@scheme[proc]'s behavior: its arity must include the number of elements +in @scheme[inits], and it must return either a number of +@scheme[#f]. The latter is easy, the former is difficult. At first +glance, this appears to suggest a contract that assigns a +variable-arity to @scheme[proc]: +@scheme[ +(->* () + (listof any/c) + (or/c number? false/c)) +] +This contract, however, says that the function must accept any +number of arguments, not a specific but +undetermined number. Thus, applying @scheme[n-step] to +@scheme[(lambda (x) x)] and @scheme[(list 1)] breaks the contract +because the given function accepts only one argument. +
+ +
+ The correct contract uses the @scheme[unconstrained-domain->]
+ combinator, which specifies only the range of a function, not its
+ domain. It is then possible to combine this contract with an arity test to
+ specify the correct @scheme[n-step]'s contract:
+
Take a look at this excerpt from a string-processing module, inspired by the
+Scheme cookbook:
+
The function definition uses @scheme[opt-lambda], which is appropriate +for this kind of functionality. The interesting point here is the formulation of +the contract for @scheme[opt-lambda]. Like the contract combinator for +@scheme[->*], i.e., rest arguments, @scheme[opt->] demands several +groups of contracts: +
+The contract library assumes that variables exported
+via @scheme[provide/contract] are not assigned to, but
+does not enforce it. Accordingly, if you try
+to @scheme[set!] those variables, you may find
+unexpected behavior. As an example, consider this program:
+
+
+To work around this, export accessor functions, rather than
+exporting the function directly, like this:
+
+This is a bug we hope to address in a future release. +
diff --git a/collects/scribblings/guide/contracts-intro.scrbl b/collects/scribblings/guide/contracts-intro.scrbl new file mode 100644 index 0000000000..d559a7dcd7 --- /dev/null +++ b/collects/scribblings/guide/contracts-intro.scrbl @@ -0,0 +1,183 @@ +#lang scribble/doc +@require[scribble/manual] +@require[scribble/eval] +@require["guide-utils.ss"] +@require["contracts-utils.ss"] +@(require (for-label scheme/contract)) + +@title[#:tag "contract-boundaries"]{Contracts and Boundaries} + +Like a contract between two business partners, a software +contract is an agreement between two parties. The agreement +specifies obligations and guarantees for each party. + +A contract thus establishes a boundary between the two parties. Whenever a +value crosses this boundary, the contract monitoring system performs contract +checks, making sure the partners abide by the established contract. + +In this spirit, PLT Scheme supports contracts only at module +boundaries. Specifically, programmers may attach contracts to +@scheme[provide] clauses and thus impose constraints and promises on the use +of exported values. For example, the export specification +@schememod[ +scheme/base + +(require scheme/contract) (code:comment "now we can write contracts") + +(provide/contract + [amount positive?]) +(define amount ...) +] + +promises to all clients of @scheme[a] that amount will always be a +positive number. The contract system monitors @scheme[a]'s obligation +carefully. Every time a client refers to @scheme[amount], the monitor checks +that the value of @scheme[amount] is indeed a positive number. + +@question[#:tag "amount0"]{What happens if @scheme[a] sets @scheme[amount] to 0?} + +Suppose the creator of @scheme[a] had written +@schememod[ +scheme/base + +(require scheme/contract) + +(provide/contract + [amount positive?]) + +(define amount 0)] + +When module @scheme[a] is required, the monitoring +system will signal a violation of the contract and +blame @scheme[a] for breaking its promises. + +@question[#:tag "qamount"]{What happens if @scheme[a] sets @scheme[amount] to @scheme['amount]?} + +Suppose the creator of @scheme[a] had written +@schememod[ +scheme/base + +(provide/contract + [amount positive?]) + +(define amount 'amount) +] + +In that case, @scheme[positive?] will report an error, since +its domain is only numbers. To make the contract capture our +intentions for all Scheme values, we can ensure that the +value is both a number and is positive, using an +@scheme[and/c] contract: + +@schemeblock[ +(provide/contract + [amount (and/c number? positive?)]) +] + +@;{ + +================================================== + +The section below discusses assigning to variables that are +provide/contract'd. This is currently buggy so this +discussion is elided. Here's the expansion of +the requiring module, just to give an idea: + +(module m mzscheme + (require (lib "contract.ss")) + (provide/contract [x x-ctc])) + +(module n mzscheme (require m) (define (f) ... x ...)) +==> +(module n mzscheme + (require (rename m x x-real)) + (define x (apply-contract x-real x-ctc ...)) + (define (f) ... x ...)) + +The intention is to only do the work of applying the +contract once (per variable reference to a +provide/contract'd variable). This is a significant +practical savings for the contract checker (this +optimization is motivated by my use of contracts while I was +implementing one of the software construction projects +(scrabble, I think ...)) + +Of course, this breaks assignment to the provided variable. + +================================================== + +|
+ |
++ +the "server" module +this allows us to write contracts + +export @scheme[amount] with a contract + + +export @scheme[do-it] without contract + + + +set amount to 4, + which satisfies contract + + +the "client" module +requires functionality from a + +first reference to @scheme[amount] (okay) +a call to @scheme[do-it], +second reference to @scheme[amount] (fail) + + |
Note: The above example is mostly self-explanatory. Take a +look at the lines in red, however. Even though the call to @scheme[do-it] +sets @scheme[amount] to -4, this action is not a contract +violation. The contract violation takes place only when the client module +(@scheme[b]) refers to @scheme[amount] again and the value flows across +the module boundary for a second time. + +
+ + + +diff --git a/collects/scribblings/guide/contracts-simple-function.scrbl b/collects/scribblings/guide/contracts-simple-function.scrbl new file mode 100644 index 0000000000..347e86e1bc --- /dev/null +++ b/collects/scribblings/guide/contracts-simple-function.scrbl @@ -0,0 +1,273 @@ +#lang scribble/doc +@require[scribble/manual] +@require[scribble/eval] +@require["guide-utils.ss"] +@require["contracts-utils.ss"] +@(require (for-label scheme/contract)) + +@title[#:tag "contract-func"]{Simple Contracts on Functions} + +When a module exports a function, it establishes two channels of +communication between itself and the client module that imports the +function. If the client module calls the function, it sends a value into the +"server" module. Conversely, if such a function call ends and the function +returns a value, the "server" module sends a value back to the "client" module. + +It is important to keep this picture in mind when you read the explanations +of the various ways of imposing contracts on functions. + +@question[#:tag "argcontract"]{How does a contract restrict the arguments of a function?} + +Functions usually don't work on all possible Scheme values but only on a +select subset such as numbers, booleans, etc. Here is a module that may +represent a bank account: + +@schememod[ +scheme/base +(require scheme/contract) + +(provide/contract + [create (-> string? number? any)] + [deposit (-> number? any)]) + +(define amount 0) +(define (create name initial-deposit) ...) +(define (deposit a) (set! amount (+ amount a))) +] + +It exports two functions: +@itemize{ + +@item{@scheme[create]: The function's contract says that it consumes two +arguments, a string and a number, and it promises nothing about the return value. }} + +@item{@scheme[deposit]: The function's contract demands from the client modules +that they apply it to numbers. It promises nothing about the return value. } + +If a "client" module that were to apply @scheme[deposit] to +@scheme['silly], it would violate the contract. The contract monitoring +system would flag this violation and blame "client" for breaking the contract +with @scheme[myaccount]. + +@bold{Note:} Instead of @scheme[any] you could also use the +more specific contract @scheme[void?], which says that the function will +always return the @scheme[(void)] value. This contract, however, would require +the contract monitoring system to check the return value every time the function +is called, even though the "client" module can't do much with this value +anyway. In contrast, @scheme[any] tells the monitoring system @italic{not} +to check the return value. Additionally, it tells a potential client that the +"server" module @italic{makes no promises at all} about the function's return +value. + +@question[#:tag "arrow"]{What does the arrow do?} + +It is natural to use an arrow to say that an exported value is a +function. In decent high schools, you learn that a function has a domain +and a range, and that you write this fact down like this: +@schemeblock[ +f : A -> B +] +Here the @scheme[A] and @scheme[B] are sets; @scheme[A] is the +domain and @scheme[B] is the range. + +Functions in a programming language have domains and ranges, too. In +statically typed languages, you write down the names of types for each +argument and for the result. When all you have, however, is a Scheme name, +such as @scheme[create] or @scheme[deposit], you want to tell the +reader what the name represents (a function) and, if it is a function (or +some other complex value) what the pieces are supposed to be. This is why +we use a @scheme[->] to say "hey, expect this to be a function." + +So @scheme[->] says "this is contract for a function." What follows +in a function contracts are contracts (sub-contracts if you wish) that tell +the reader what kind of arguments to expect and what kind of a result the +function will produce. For example, +@schemeblock[ +(provide/contract + [create (-> string? number? boolean? account?)]) +] +says that @scheme[create] is a function of three arguments: a string, a +number, and a boolean. Its result is an account. + +In short, the arrow @scheme[->] is a @italic{contract +combinator}. Its purpose is to combine other contracts into a contract +that says "this is a function @italic{and} its arguments and its result are +like that." + +@question[#:tag "dots"]{What are the dots in contracts about?} + +If you are used to mathematics, you like the arrow in between the domain + and the range of a function, not at the beginning. If you have read "How + to Design Programs," you have seen this many times. Indeed, you may have + seen contracts such as these in other people's code: + +@schemeblock[ +(provide/contract + [create (string? number? boolean? . -> . account?)]) +] + +If a PLT Scheme S-expression contains two dots with a symbol in the middle, +the reader re-arranges the S-expression and place the symbol at the front. Thus, +@schemeblock[ +(string? number? boolean? . -> . account?) +] +is really just a short-hand for +@schemeblock[ +(-> string? number? boolean? account?) +] +Of course, placing the arrow to the left of the range follows not only +mathematical tradition but also that of typed functional languages. + +@question[#:tag "own"]{Can I make my own contracts for arguments?} + +The @scheme[deposit] function adds the given number to the value of +@scheme[amount]. While the function's contract prevents clients from +applying it to non-numbers, the contract still allows them to apply the function +to complex numbers, negative numbers, or inexact numbers, all of which do not +represent amounts of money. + +To this end, the contract system allows programmers to define their own +contracts: + +@schememod[ +scheme/base +(require scheme/contract) + +(define (amount? a) + (and (number? a) (integer? a) (exact? a) (>= a 0))) + +(provide/contract + (code:comment "an amount is a natural number of cents") + (code:comment "is the given number an amount?") + [deposit (-> amount? any)] + [amount? (-> any/c boolean?)]) + +(define this 0) +(define (deposit a) (set! this (+ this a))) +] + +The module introduces a +predicate, @scheme[amount?]. The @scheme[provide] +clause refers to this predicate, as a contract, for its +specification of the contract of +@scheme[deposit]. + +Of course it makes no sense to restrict a channel of +communication to values that the client doesn't +understand. Therefore the module also exports +the @scheme[amount?] predicate itself, with a contract +saying that it accepts an arbitrary value and returns a +boolean. + +In this case, we could also have used @scheme[natural-number/c], which is +a contract defined in "contract.ss" that is equivalent to @scheme[amount] +(modulo the name): + +@schememod[ +scheme/base + +(require scheme/contract) + +(provide/contract + (code:comment "an amount is a natural number of cents") + [deposit (-> natural-number/c any)]) + +(define this 0) +(define (deposit a) (set! this (+ this a))) +] + +Lesson: look up the built-in contracts. + +@question[#:tag "and-or"]{Are and/c and or/c contract combinators? What of listof?} + +The short answer is yes. Both @scheme[and/c] and @scheme[or/c] +ombine contracts and they do what you expect them to do. + +For example, if we didn't have @scheme[natural-number/c], the +@scheme[amount?] contract is a bit opaque. Instead, we would define it +as follows: + +@schememod[ +scheme/base +(require scheme/contract) + +(define amount + (and/c number? integer? exact? (or/c positive? zero?))) + +(provide/contract + (code:comment "an amount is a natural number of cents") + (code:comment "is the given number an amount?") + [deposit (-> amount any)]) + +(define this 0) +(define (deposit a) (set! this (+ this a))) +] + +That is, amount is a contract that enforces the following conditions: the +value satisfies @scheme[number?] and @scheme[integer?] and +@scheme[exact?] and is either @scheme[positive?] or +@scheme[zero?]. + +Oh, we almost forgot. What do you think @scheme[(listof char?)] +means? Hint: it is a contract! + +@question[#:tag "range"]{How does a contract restrict the range of a function?} + +Consider a utility module for creating strings from banking records: + +@schememod[scheme/base +(require scheme/contract) + +(provide/contract + ... + (code:comment "convert a random number to a string") + [format-number (-> number? string?)] + + (code:comment "convert an amount into a dollar based string") + [format-nat (-> natural-number/c + (lambda (result) + (define L (string-length result)) + (and (string? result) + (>= L 3) + (char=? #\. (string-ref result (- L 3))))))]) +... +] +The contract of the exported function @scheme[format-number] specifies that +the function consumes a number and produces a string. + +The contract of the exported function @scheme[format-nat] is more +interesting than the one of @scheme[format-number]. It consumes only +natural numbers. Its range contract promises a string that has a dot "." in the +third position from the right. + +@bold{Exercise 1} Strengthen the promise of the range contract for +@scheme[format-nat] so that it admits only strings with digits and a single +dot. + +@question[#:tag "exercise1"]{Solution to Exercise 1} + +@schememod[scheme/base +(require scheme/contract) + +(define (digit-char? x) + (member x '(#\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9 #\0))) + +(provide/contract + ... + (code:comment "convert a random number to a string") + [format-number (-> number? string?)] + + (code:comment "convert an amount (natural number) of cents") + (code:comment "into a dollar based string") + [format-nat (-> natural-number/c + (lambda (result) + (define L (string-length result)) + (and (string? result) + (andmap digit-char? + (string->list (substring result 0 (- L 3)))) + (andmap digit-char? + (string->list (substring result (- L 2) L))) + (char=? #\. (string-ref result (- L 3))))))]) +] + + diff --git a/collects/scribblings/guide/contracts-structure.scrbl b/collects/scribblings/guide/contracts-structure.scrbl new file mode 100644 index 0000000000..afd6088e6a --- /dev/null +++ b/collects/scribblings/guide/contracts-structure.scrbl @@ -0,0 +1,313 @@ +#lang scribble/doc +@require[scribble/manual] +@require[scribble/eval] +@require["guide-utils.ss"] +@require["contracts-utils.ss"] +@(require (for-label scheme/contract)) + + + +
Modules deal with structures in two ways. First they export
+@scheme[struct] definitions, i.e., the ability to create structs of a
+certain kind, to access their fields, to modify them, and to distinguish structs
+of this kind against every other kind of value in the world. Second, on occasion
+a module exports a specific struct and wishes to promise that its fields contain
+values of a certain kind. This section explains how to protect structs with
+contracts for both uses.
+
+ Yes. If your module defines a variable to be a structure, then on export you
+can specify the structures shape:
+ Yes, again. See the help desk for information on @scheme[vector/c] and
+similar contract combinators for (flat) compound data.
+
+ "How to Design Programs" teaches that @scheme[posn]s should contain only
+numbers in their two fields. With contracts we would enforce this informal data
+definition as follows:
+
+ Thus, if a client calls @scheme[make-posn] on @scheme[10] and
+@scheme['a], the contract system will signal a contract
+violation. Similarly, if @scheme[(set-posn-x! (make-posn 10 10) 'a)] causes
+an error.
+
+ The creation of @scheme[p-sick] inside of the @scheme[posn] module,
+however, does not violate the contracts. The function @scheme[make-posn] is
+internal so @scheme['a] and @scheme['b] don't cross the module
+boundary. Similarly, when @scheme[p-sick] crosses the boundary of
+@scheme[posn], the contract promises a @scheme[posn?] and nothing
+else. In particular, this check does not enforce that the fields of
+@scheme[p-sick] are numbers.
+
+ The association of contract checking with module boundaries implies that
+@scheme[p-okay] and @scheme[p-sick] look alike from a client's
+perspective until the client extracts the pieces:
+
+ This specific example shows that the explanation for a contract violation
+ doesn't always pinpoint the source of the error. The good news is that the
+ error is located in the @scheme[posn] module. The bad news is that the
+ explanation is misleading. Although it is true that @scheme[posn-x]
+ produced a symbol instead of a number, it is the fault of the programmer who
+ created a @scheme[posn] from symbols, i.e., the programmer who added
+
+ Exercise 2: Use your knowledge from the
+section on exporting specific structs and change the contract for
+@scheme[p-sick] so that the error is caught when clients refer to the
+structure. Solution
+
+
+Contracts written using @scheme[struct/c] immediately
+check the fields of the data structure, but sometimes this
+can have disastrous effects on the performance of a program
+that does not, itself, inspect the entire data structure.
+ As an example, consider the the binary search tree
+search algorithm. A binary search tree is like a binary
+tree, except that the numbers are organized in the tree to
+make searching the tree fast. In particular, for each
+interior node in the tree, all of the numbers in the left
+subtree are smaller than the number in the node, and all of
+the numbers in the right subtree are larger than the number
+in the node.
+We can implement implement a search
+function @scheme[in?] that takes advantage of the
+structure of the binary search tree.
+
+The contract on @scheme[in?] guarantees that its input
+is a binary search tree. But a little careful thought
+reveals that this contract defeats the purpose of the binary
+search tree algorithm. In particular, consider the
+inner @scheme[cond] in the @scheme[in?]
+function. This is where the @scheme[in?] function gets
+its speed: it avoids searching an entire subtree at each
+recursive call. Now compare that to the @scheme[bst-between?]
+function. In the case that it returns @scheme[#t], it
+traverses the entire tree, meaning that the speedup
+of @scheme[in?] is lost.
+
+In order to fix that, we can employ a new strategy for
+checking the binary search tree contract. In particular, if
+we only checked the contract on the nodes
+that @scheme[in?] looks at, we can still guarantee that
+the tree is at least partially well-formed, but without
+the performance loss.
+
+To do that, we need to
+use @scheme[define-contract-struct] in place
+of @scheme[define-struct]. Like @scheme[define-struct],
+@scheme[define-contract-struct] defines a maker,
+predicate, and selectors for a new
+structure. Unlike @scheme[define-struct], it also
+defines contract combinators, in this
+case @scheme[node/c] and @scheme[node/dc]. Also unlike
+@scheme[define-struct], it does not define mutators, making
+its structs immutable.
+
+The @scheme[node/c] function accepts a contract for each
+field of the struct and returns a contract on the
+struct. More interestingly, the syntactic
+form @scheme[node/dc] allows us to write dependent
+contracts, i.e., contracts where some of the contracts on
+the fields depend on the values of other fields. We can use
+this to define the binary search tree contract:
+
+Although this contract improves the performance
+of @scheme[in?], restoring it to the logarithmic
+behavior that the contract-less version had, it is still
+imposes a fairly large constant overhead. So, the contract
+library also provides @scheme[define-opt/c] that brings
+down that constant factor by optimizing its body. Its shape
+is just like the @scheme[define] above. It expects its
+body to be a contract and then optimizes that contract.
+ A single change suffices:
+
+