From fdb9c14eb86475c2b43f605b7c42dbb466b5dfb5 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Thu, 3 Jan 2008 22:23:45 +0000 Subject: [PATCH] started integrating the contracts guide into the plt scheme guide svn: r8199 --- .../scribblings/guide/contract-examples.scrbl | 84 +++ .../scribblings/guide/contract-examples/1.ss | 123 ++++ .../scribblings/guide/contract-examples/2.ss | 105 +++ .../scribblings/guide/contract-examples/3.ss | 107 +++ .../scribblings/guide/contract-examples/5.ss | 102 +++ .../scribblings/guide/contract-examples/6.ss | 20 + .../scribblings/guide/contracts-class.scrbl | 7 + .../guide/contracts-general-function.scrbl | 667 ++++++++++++++++++ .../scribblings/guide/contracts-gotchas.scrbl | 62 ++ .../scribblings/guide/contracts-intro.scrbl | 183 +++++ .../scribblings/guide/contracts-objects.scrbl | 7 + .../guide/contracts-simple-function.scrbl | 273 +++++++ .../guide/contracts-structure.scrbl | 313 ++++++++ collects/scribblings/guide/contracts-utils.ss | 11 + collects/scribblings/guide/contracts.scrbl | 18 + collects/scribblings/guide/guide.scrbl | 9 +- 16 files changed, 2084 insertions(+), 7 deletions(-) create mode 100644 collects/scribblings/guide/contract-examples.scrbl create mode 100644 collects/scribblings/guide/contract-examples/1.ss create mode 100644 collects/scribblings/guide/contract-examples/2.ss create mode 100644 collects/scribblings/guide/contract-examples/3.ss create mode 100644 collects/scribblings/guide/contract-examples/5.ss create mode 100644 collects/scribblings/guide/contract-examples/6.ss create mode 100644 collects/scribblings/guide/contracts-class.scrbl create mode 100644 collects/scribblings/guide/contracts-general-function.scrbl create mode 100644 collects/scribblings/guide/contracts-gotchas.scrbl create mode 100644 collects/scribblings/guide/contracts-intro.scrbl create mode 100644 collects/scribblings/guide/contracts-objects.scrbl create mode 100644 collects/scribblings/guide/contracts-simple-function.scrbl create mode 100644 collects/scribblings/guide/contracts-structure.scrbl create mode 100644 collects/scribblings/guide/contracts-utils.ss create mode 100644 collects/scribblings/guide/contracts.scrbl diff --git a/collects/scribblings/guide/contract-examples.scrbl b/collects/scribblings/guide/contract-examples.scrbl new file mode 100644 index 0000000000..6794b0e44c --- /dev/null +++ b/collects/scribblings/guide/contract-examples.scrbl @@ -0,0 +1,84 @@ +NOTE: this section needs the files in contract-examples/*ss +to be added to it (presumably programmatically). + +
+ +
+

+ 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): +

+ +
    +
  1. Separate queries from commands. + +

    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.

    +
    2. + +
  2. Separate basic queries from derived queries. + +

    A derived query returns a result that is computable in + terms of basic queries.

    +
    3. + +
  3. For each derived query, write a post-condition contract that + specifies the result in terms of the basic queries. + +

    +

    4. + +
  4. For each command, write a post-condition contract that specifies the + changes to the observable properties in terms of the basic queries. + +

    +

    5. + +
  5. For each query and command, decide on suitable pre-condition contract. + +

    +

    6. +
+ + +
+

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/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 @@ +
+ +
+ + + +
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: + +(module myaccount mzscheme + (require (lib "contract.ss")) + + (provide/contract + [deposit (-> (lambda (x) + (and (number? x) (integer? x) (>= x 0))) + any)]) + + (define this 0) + (define (deposit a) ...)) + + +Several clients used your module. Others used their modules. And all of a sudden +one of them sees this error message: + +

+

+bank-client broke the contract (-> ??? any)
+it had with myaccount on deposit; 
+expected <???>, given: -10
+
+
+ +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? + +

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: + + +(module myaccount mzscheme + (require (lib "contract.ss")) + + (define (amount? x) (and (number? x) (integer? x) (>= x 0))) + (define amount (flat-named-contract 'amount amount?)) + + (provide/contract + [deposit (amount . -> . any)]) + + (define this 0) + (define (deposit a) ...)) + + +With this little change, the error message becomes all of sudden quite readable: + +

+

+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: + + +(module numerics mzscheme + (require (lib "contract.ss")) + + (provide/contract + [sqrt.v1 (->d (lambda (x) (>= x 1)) + (lambda (argument) + (lambda (result) + (<= result argument))))] + ...) + ...) + + +The contract for the exported function @scheme[sqrt.v1] uses the +@scheme[->d] rather than @scheme[->] function contract. The "d" +stands for dependent contract, meaning the contract for the +function range depends on the value of the argument. + +

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: + + + +(module account mzscheme + (require (lib "contract.ss")) + + (define-struct account (balance)) + (define amount natural-number/c) + + (provide/contract + ;; create an account with the given initial deposit + [create (amount . -> . account?)] + + ;; what is the current balance of the account? + [balance (account . -> . amount)] + + ;; deposit the given amount into the given account + ;; account? amount -> account? + [deposit (->d account? + amount + (lambda (account amount) + (let ([balance0 (balance account)]) + (lambda (result) + (and (account? result) + (<= balance0 (balance result)))))))] + ... ) + + ... + ) + + +

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: + + +(module numerics mzscheme + (require (lib "contract.ss")) + + (provide/contract + [sqrt.2 (->d (>=/c 1.0) <=/c)] + ...) + ...) + + +The combinator @scheme[>=/c] consumes a number @scheme[x] and +produces a contract. This contract also consumes a second number, say +@scheme[y], and makes sure that @scheme[(>= y x)] holds. The +contract combinator @scheme[<=/c] works in an analogous fashion. + +

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: + +;; balance : Account -> Amount +;; withdraw : Account Amount -> Account + +Then, informally, the proper precondition for @scheme[withdraw] is that +

+"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: + +
+ +(module account mzscheme + (require (lib "contract.ss")) + + (define-struct account (balance)) + (define amount natural-number/c) + + (define msg> + "account a with balance larger than ~a expected") + (define msg< + "account a with balance less than ~a expected") + + (define (mk-account-contract acc amt op msg) + (define balance0 (balance acc)) + (define (ctr a) + (and (account? a) (op balance0 (balance a)))) + (flat-named-contract (format msg balance0) ctr)) + + (provide/contract + [create (amount . -> . account?)] + [balance (account? . -> . amount)] + [withdraw (->r ([acc account?] + [amt (and/c amount (</c (balance acc)))]) + (mk-account-contract acc amt > msg>))] + [deposit (->r ([acc account?] + [amt amount]) + (mk-account-contract acc amt < msg<))]) + + (define balance account-balance) + + (define (create amt) (make-account amt)) + + (define (withdraw acc amt) + (set-account-balance! acc (- (balance acc) amt)) + acc) + + (define (deposit acc amt) + (set-account-balance! acc (+ (balance acc) amt)) + acc)) + + +
+
+
+the contract definitions 
+
+
+
+
+
+
+
+
+
+
+
+
+
+the exports 
+
+
+
+
+
+
+
+
+
+
+the function definitions 
+
+
+
+ +The purple part is the export interface: +

    +
  1. @scheme[create] consumes an initial deposit and produces an +account. This kind of contract is just like a type in a statically typed +language, except that statically typed languages usually don't support the type +"natural numbers" (as a full-fledged subtype of numbers). +
    2. + +
  2. @scheme[balance] consumes an account and computes its current balance. +
    3. + +
  3. @scheme[withdraw] consumes an account, named @scheme[acc], and an +amount, @scheme[amt]. In addition to being an @scheme[amount], the +latter must also be less than @scheme[(balance acc)], i.e., the balance of +the given account. That is, the contract for @scheme[amt] depends on the +value of @scheme[acc], which is what the @scheme[->r] (r for recursive) +contract combinator expresses. + +

    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. +

    4. + +
  4. @scheme[deposit]'s contract has been reformulated using the +@scheme[->r] combinator. Strictly speaking, this isn't necessary and the use +of @scheme[->d] would suffice, because the contracts for the arguments do +not depend on each other. +
    5. +
+ +The code in deep purple defines all those pieces that are needed for the +formulation of the export contracts: @scheme[account?], @scheme[amount], +error messages (format strings), and @scheme[mk-account-contract]. The +latter is a function that extracts the current balance from the given account +and then returns a named contract, whose error message (contract name) is a +string that refers to this balance. The resulting contract checks whether an +account has a balance that is larger or smaller, depending on the given +comparison operator, than the original balance. + + + + + +

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: + +(define (plus fst snd . rst) + (foldr + (+ fst snd) rst)) + + Describing this function via a contract is difficult because of the rest + argument (@scheme[rst]). + +

Here is the contract: + +(provide/contract + [plus (->* (number? number?) (listof number?) (number?))]) + + The @scheme[->*] contract combinator empowers you to specify + functions that consume a variable number of arguments or functions like + @scheme[plus], which consume "at least this number" of arguments but + an arbitrary number of additional arguments. + +

The contracts for the required arguments are enclosed in an additional + pair of parentheses: + +(number? number?) + + For @scheme[plus] they demand two numbers. The contract for the + rest argument follows: + +(listof number?) + + Since the remainder of the actual arguments are collected in a list for + a @scheme[rest] parameter such as @scheme[rst], the contract + demands a list of values; in this specific examples, these values must be + number. + +

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): + + +(define substring1 + (case-lambda + [(s) (substring1 s 0 (string-length s))] + [(s start) (substring1 s start (string-length s))] + [(s start end) (substring s start end)])) + + This version of @scheme[substring] has one of the following signature: +

    +
  1. just a string, in which case it copies the string; +
  2. a string and an index into the string, in which case it extracts the + suffix of the string starting at the index; or +
  3. a string a start index and an end index, in which case it extracts the + fragment of the string between the two indices. +
+ +

The contract for such a function is formed with the @scheme[case->] + combinator, which combines as many functional contracts as needed: + +(provide/contract + [substring1 (case-> + (string? . -> . string?) + (string? natural-number/c . -> . string?) + (string? natural-number/c natural-number/c . -> . string?))]) + + As you can see, the contract for @scheme[substring1] combines three + function contracts, just as many clauses as the explanation of its + functionality required. + +

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: + +(provide/contract + [substring1 (case-> + (string? . -> . string?) + (->r ([s string?] + [_ (and/c natural-number/c (r ([s string?] + [a (and/c natural-number/c (=/c a) + ( + Here we used @scheme[->r] to name the parameters and express the + numeric constraints on them. + + + + + +

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: + +(define (split l) + (define (split l w) + (cond + [(null? l) (values (list->string (reverse w)) '())] + [(char=? #\newline (car l)) (values (list->string (reverse w)) (cdr l))] + [else (split (cdr l) (cons (car l) w))])) + (split l '())) + + It is a typical multiple-value function, returning two values by + traversing a single 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: + +(provide/contract + [split (-> (listof char?) + (values string? (listof char?)))]) + +

+ +

The contract for such a function can also be written +using @scheme[->*], just like + @scheme[plus]: + +(provide/contract + [split (->* ((listof char?)) + (string? (listof char?)))]) + + As before the contract for the single argument is wrapped + in an extra pair of parentheses (and must always be wrapped + like that); so are the contracts for the results: a string + and a list of characters. +

+ +

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: + +(provide/contract + [splitp (->d* ((listof char?)) + (lambda (fl) + (define wd (list->string fl)) + (values (and/c string? (lambda (w) (string<=? w wd))) + (listof char?))))]) + + Like @scheme[->d], the new combinator uses a function over the + argument to create the range contracts. Yes, it doesn't just return one + contract but as many as the function produces values: one contract per + value. In this case, the second contract is the same as before, ensuring + that the second result is a list of @scheme[char]s. In contrast, the + first contract strengthens the old one so that the result is a prefix of + the given word. + +

This contract is expensive to check of course. Here is a slightly + cheaper version: + +(provide/contract + [splitl (->d* ((listof char?)) + (lambda (fl) + (values (and/c string? (string/len (add1 (length fl)))) + (listof char?))))]) + + Check the help desk for an explanation of @scheme[string/len]. + + + + +

+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: + + +;; (Number ... -> (union #f number?)) (listof Number) -> Void +(define (n-step proc inits) + (let ([inc (apply proc inits)]) + (when inc + (n-step proc (map (λ (x) (+ x inc)) inits))))) + + +The argument of @scheme[n-step] is @scheme[proc], a function +@scheme[proc] whose results are either numbers or false, and a list. It +then applies @scheme[proc] to the list @scheme[inits]. As long as +@scheme[proc] returns a number, @scheme[n-step] treats that number +as an increment for each of the numbers in @scheme[inits] and +recurs. When @scheme[proc] returns @scheme[false], the loop stops. +

+ +Here are two uses: + + + + +
+ +
@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: + +(provide/contract + [n-step + (->r ([proc (and/c (unconstrained-domain-> (or/c false/c number?)) + (λ (f) (procedure-arity-includes? f (length inits))))] + [inits (listof number?)]) + any)]) + +

+ + + + + +

Take a look at this excerpt from a string-processing module, inspired by the +Scheme cookbook: + +(module string-pad mzscheme + (require (lib "contract.ss") (lib "etc.ss") (lib "string.ss" "srfi" "13")) + + (provide/contract + ;; pad the given str left and right with + ;; the (optional) char so that it is centered + [string-pad-center (opt-> (string? natural-number/c) (char?) + string?)]) + + (define string-pad-center + (opt-lambda (str width [pad #\space]) + (define field-width (min width (string-length str))) + (define rmargin (- width (floor (/ (- width field-width) 2)))) + (string-pad (string-pad-right str rmargin pad) width pad)))) + + + The module exports @scheme[string-pad-center], a function that creates a + string of a given @scheme[width] with the given string in the center. The + default fill character is @scheme[#\space]; if the client module requires + different character, it may call @scheme[string-pad-center] with a third + argument, a @scheme[char], overwriting the default. + +

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: +

    +
  1. The first one is a parenthesized group of contracts for all required +arguments. In this example, we see two: @scheme[string?] and +@scheme[natural-number/c]. + +
  2. The second one is a parenthesized group of contracts for all optional +arguments: @scheme[char?]. + +
  3. The last one is a single contract: the result of the function. +
+ Note if a default value does not satisfy a contract, you won't get a contract + error for this interface. We do trust you; if you can't trust + yourself, you need to communicate across boundaries for everything you write. + +The contract library does not have built-in combinators to +specify richer contracts for functions that have optional +arguments, like functions that have optional arguments where +the arguments depend on each other. + +To specify such contracts combine @scheme[case->] with +the other function contract combinators, like we did in +the @scheme[substring1] function above. + diff --git a/collects/scribblings/guide/contracts-gotchas.scrbl b/collects/scribblings/guide/contracts-gotchas.scrbl new file mode 100644 index 0000000000..bb1496dce8 --- /dev/null +++ b/collects/scribblings/guide/contracts-gotchas.scrbl @@ -0,0 +1,62 @@ +#lang scribble/doc +@require[scribble/manual] +@require[scribble/eval] +@require["guide-utils.ss"] +@require["contracts-utils.ss"] +@(require (for-label scheme/contract)) + +
+ + What about @scheme[set!] on variables provided via @scheme[provide/contract]? + + +

+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: + + +(module x mzscheme + (require (lib "contract.ss")) + (define (inc-x!) (set! x (+ x 1))) + (define x 0) + (provide/contract [inc-x! (-> void?)] + [x integer?])) + +(module client mzscheme + (require x) + (define (print-latest) (printf "x is ~s\n" x)) + + (print-latest) + (inc-x!) + (print-latest)) + +(require client) + + +When it runs, both calls to @scheme[print-latest] +print @scheme[0], even though the value +of @scheme[x] has been incremented (and the change is +visible inside the module @scheme[x]). +

+ +

+To work around this, export accessor functions, rather than +exporting the function directly, like this: + +(module x mzscheme + (require (lib "contract.ss")) + (define (get-x) x) + (define (inc-x!) (set! x (+ x 1))) + (define x 0) + (provide/contract [inc-x! (-> void?)] + [get-x (-> integer?)])) + + +

+ +

+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. + +================================================== + + + + +
+ +;; Language: Pretty Big +(module a mzscheme + (require (lib "contract.ss")) + + (provide/contract + [amount positive?]) + + (provide + ;; -> Void + ;; effect: sets variable a + do-it) + + (define amount 4) + + (define (do-it) (set! amount -4))) + +(module b mzscheme + (require a) + + (printf "~s~n" amount) + (do-it) + (printf "~s~n" amount)) + +(require b) + + +
+
+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. + + +} + +@question[#:tag "obligations"]{How can a "server" module impose obligations on its client?} + +On occasion, a module may want to enter a contract with +another module only if the other module abides by certain +rules. In other words, the module isn't just promising some +services, it also demands the client to deliver +something. This kind of thing happens when a module exports +a function, an object, a class or other values that enable +values to flow in both directions. diff --git a/collects/scribblings/guide/contracts-objects.scrbl b/collects/scribblings/guide/contracts-objects.scrbl new file mode 100644 index 0000000000..fa421a051f --- /dev/null +++ b/collects/scribblings/guide/contracts-objects.scrbl @@ -0,0 +1,7 @@ +

+ +
+ + + +
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: + +(module geometry mzscheme + (require (lib "contract.ss")) + (require posn) + + (define origin (make-posn 0 0)) + ... + + (provide/contract + [origin (struct/c posn zero? zero?)] + ...) + ... ) + + + In this example, the module imports a library for representing positions, which + exports a @scheme[posn] structure. One of the @scheme[posn]s it creates + and exports stands for the origin, i.e., (0,), of the grid. + + + + + +

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: + + +(module posn mzscheme + (require (lib "contract.ss")) + + (define-struct posn (x y)) + + (provide/contract + [struct posn ((x number?) (y number?))] + [p-okay posn?] + [p-sick posn?]) + + (define p-okay (make-posn 10 20)) + (define p-sick (make-posn 'a 'b))) + + +This module exports the entire structure definition: @scheme[make-posn], +@scheme[posn?], @scheme[posn-x], @scheme[posn-y], +@scheme[set-posn-x!], and @scheme[set-posn-y!]. Each function enforces +or promises that the two fields of a @scheme[posn] structure are +numbers---when the values flow across the module boundary. + +

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: + + +(module client mzscheme + (require posn) + + ... (posn-x p-sick) ...) + + + Using @scheme[posn-x] is the only way @scheme[client] can find out what + a @scheme[posn] contains in the @scheme[x] field. The application of + @scheme[posn-x] sends @scheme[p-sick] back into the + @scheme[posn]module and the result value -- @scheme['a] here -- back to + the client, again across the module boundary. At this very point, the contract + system discovers that a promise is broken. Specifically, @scheme[posn-x] + doesn't return a number but a symbol and is therefore blamed. + +

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 + + + (define p-sick (make-posn 'a 'b)) + + to the module. So, when you are looking for bugs based on contract violations, + keep this example in mind. + +

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. + +(module bst mzscheme + (require (lib "contract.ss")) + (define-struct node (val left right)) + + ;; determines if `n' is in the binary search tree `b', + ;; exploiting the binary search tree invariant + (define (in? n b) + (cond + [(null? b) #f] + [else (cond + [(= n (node-val b)) + #t] + [(< n (node-val b)) + (in? n (node-left b))] + [(> n (node-val b)) + (in? n (node-right b))])])) + + ;; a predicate that identifies binary search trees + (define (bst-between? b low high) + (or (null? b) + (and (<= low (node-val b) high) + (bst-between? (node-left b) low (node-val b)) + (bst-between? (node-right b) (node-val b) high)))) + + (define (bst? b) (bst-between? b -inf.0 +inf.0)) + + (provide (struct node (val left right))) + (provide/contract + [bst? (any/c . -> . boolean?)] + [in? (number? bst? . -> . boolean?)])) + +In a full binary search tree, this means that +the @scheme[in?] function only has to explore a +logarithmic number of nodes. +

+

+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: + +(module bst mzscheme (require (lib "contract.ss")) + (define-contract-struct node (val left right)) + + ;; determines if `n' is in the binary search tree `b' + (define (in? n b) ... as before ...) + + ;; bst-between : number number -> contract + ;; builds a contract for binary search trees + ;; whose values are betweeen low and high + (define (bst-between/c low high) + (or/c null? + (node/dc [val (between/c low high)] + [left (val) (bst-between/c low val)] + [right (val) (bst-between/c val high)]))) + + (define bst/c (bst-between/c -inf.0 +inf.0)) + + (provide make-node node-left node-right node-val node?) + (provide/contract + [bst/c contract?] + [in? (number? bst/c . -> . boolean?)])) + +In general, each use of @scheme[node/dc] must name the +fields and then specify contracts for each fields. In the +above, the @scheme[val] field is a contract that accepts +values between @scheme[low] and @scheme[high]. +The @scheme[left] and @scheme[right] fields are +dependent on the value of the @scheme[val] field, +indicated by their second sub-expressions. Their contracts +are built by recursive calls to +the @scheme[bst-between/c] function. Taken together, +this contract ensures the same thing that +the @scheme[bst-between?] function checked in the +original example, but here the checking only happens +as @scheme[in?] explores the tree. +

+ +

+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. + +(define-opt/c (bst-between/c low high) + (or/c null? + (node/dc [val (between/c low high)] + [left (val) (bst-between/c low val)] + [right (val) (bst-between/c val high)]))) + +

+ + + + +

A single change suffices: + + +(module posn mzscheme + (require (lib "contract.ss")) + + (define I (make-inspector)) + (provide I) + + (define-struct posn (x y) I) + + (provide/contract + [struct posn ((x number?) (y number?))] + [p-okay posn?] + [p-sick (struct/c posn number? number?)]) + + (define p-okay (make-posn 10 20)) + (define p-sick (make-posn 'a 'b))) + + +Instead of exporting @scheme[p-sick] as a plain @scheme[posn?], we use a +@scheme[struct/c] contract to enforce constraints on its components. + + + diff --git a/collects/scribblings/guide/contracts-utils.ss b/collects/scribblings/guide/contracts-utils.ss new file mode 100644 index 0000000000..817a5a299c --- /dev/null +++ b/collects/scribblings/guide/contracts-utils.ss @@ -0,0 +1,11 @@ +#lang scheme/base +(require scribble/basic) + +(provide question) + +(define (question #:tag [tag #f] . rest) + (keyword-apply section + '(#:tag) + (list (and tag (format "contracts-~a" tag))) + rest)) + diff --git a/collects/scribblings/guide/contracts.scrbl b/collects/scribblings/guide/contracts.scrbl new file mode 100644 index 0000000000..09111bec74 --- /dev/null +++ b/collects/scribblings/guide/contracts.scrbl @@ -0,0 +1,18 @@ +#lang scribble/doc +@require[scribble/manual] +@require[scribble/eval] +@require["guide-utils.ss"] + +@title[#:tag "contracts"]{Contracts} + +@local-table-of-contents[] + +@include-section["contracts-intro.scrbl"] +@include-section["contracts-simple-function.scrbl"] +@;{ +@include-section["contracts-general-function.scrbl"] +@include-section["contracts-structure.scrbl"] +@include-section["contracts-class.scrbl"] +@include-section["contracts-example.scrbl"] +@include-section["contract-gotchas.scrbl"] +} \ No newline at end of file diff --git a/collects/scribblings/guide/guide.scrbl b/collects/scribblings/guide/guide.scrbl index 75bb5e5aad..a91f9ba3c4 100644 --- a/collects/scribblings/guide/guide.scrbl +++ b/collects/scribblings/guide/guide.scrbl @@ -31,15 +31,10 @@ precise details to @|MzScheme| and other reference manuals. @include-section["modules.scrbl"] +@include-section["contracts.scrbl"] + @include-section["io.scrbl"] -@; ---------------------------------------------------------------------- -@section[#:tag "contracts"]{Contracts} - -In the reference manual, the documentation for each procedure -describes the acceptable arguments and the result of the procedure -using @idefterm{contracts}. - @; ---------------------------------------------------------------------- @include-section["class.scrbl"]