suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

started integrating the contracts guide into the plt scheme guide

Browse Source 
svn: r8199
This commit is contained in:
Robby Findler 2008-01-03 22:23:45 +00:00
parent 17c6b00f44
commit fdb9c14eb8
16 changed files with 2084 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

84
collects/scribblings/guide/contract-examples.scrbl Normal file
View File

@ -0,0 +1,84 @@
NOTE: this section needs the files in contract-examples/*ss
to be added to it (presumably programmatically).
<section title="Examples" tag="text-examples" />
<blockquote>
<p>
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].
</p>
</blockquote>
<question title="How do I design data structures with contracts?" tag="0">
<p>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):
</p>
<ol>
<li><b>Separate queries from commands.</b>
<p>A <em>query</em> returns a result but does not change the observable
properties of an object. A <em>command</em> 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.</p>
</li>
<li><b>Separate basic queries from derived queries.</b>
<p>A <em>derived query</em> returns a result that is computable in
terms of basic queries.</p>
</li>
<li><b>For each derived query, write a post-condition contract that
specifies the result in terms of the basic queries.</b>
<p />
</li>
<li><b>For each command, write a post-condition contract that specifies the
changes to the observable properties in terms of the basic queries.</b>
<p />
</li>
<li><b>For each query and command, decide on suitable pre-condition contract.</b>
<p />
</li>
</ol>
</question>
<blockquote>
<p>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
color="purple">font</font> so that they are easy to find. Implementations
are presented ahead of the interface in <font color="navy">navy.</font>
Finally, tests are included in <font "a0a0aa">a light shade.</font> We
recommend that you read the contracts first, then the implementation, and
then the test module.
</p>
<p>
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). </p>
<p>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).
</p>
</blockquote>

123
collects/scribblings/guide/contract-examples/1.ss Normal file
View File

@ -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?)])
<font color="red">;; A pre-post condition contract must use a side-effect
;; to express this contract via post-conditions</font>
(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)

105
collects/scribblings/guide/contract-examples/2.ss Normal file
View File

@ -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"
<font color="red">;; Noel & Ryan: this is how things should work:
#;(assert-exn exn:fail:contract?
(push (initialize (flat-contract integer?)) 'a))</font>
;; 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)

107
collects/scribblings/guide/contract-examples/3.ss Normal file
View File

@ -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)

102
collects/scribblings/guide/contract-examples/5.ss Normal file
View File

@ -0,0 +1,102 @@
;; chapter 5: A Queue
;; --- queue -------------------------------------------------------------------
;; <font color="blue">Note: this queue doesn't implement the capacity restriction
;; of McKim and Mitchell's queue but this is really minor and easy to add.</font>
(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
;; <font color="red">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. </font>
[items (->d queue? (compose listof queue-p?))]
;; derived queries
[count (->r ([q queue?])
;; <font color="red">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). </font>
(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)

20
collects/scribblings/guide/contract-examples/6.ss Normal file
View File

@ -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 <b>implies</b> postcondition1
;; and
;; ...
;; and
;; preconditionN <b>implies</b> postconditionN
;; [Note: I am not sure about this one yet.]

7
collects/scribblings/guide/contracts-class.scrbl Normal file
View File

@ -0,0 +1,7 @@
<section title="Interfaces: Contracts on Classes" tag="ifs" />
<blockquote>
<!-- waiting for interface/contract -->
</blockquote>

667
collects/scribblings/guide/contracts-general-function.scrbl Normal file
View File

@ -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))
<section title="Contracts on Functions in General" tag="genfunc" />
<question title="Why do the error messages contain "..."?" tag="flat-named-contract">
<p>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:
<scheme>
(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) ...))
</scheme>
Several clients used your module. Others used their modules. And all of a sudden
one of them sees this error message:
<blockquote>
<pre><font color="red">
bank-client broke the contract (-> ??? any)
it had with myaccount on deposit;
expected &lt;???>, given: -10
</font></pre>
</blockquote>
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?
<p>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:
<scheme>
(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) ...))
</scheme>
With this little change, the error message becomes all of sudden quite readable:
<blockquote>
<pre><font color="red">
bank-client broke the contract (-> amount any)
it had with myaccount on deposit;
expected &lt;amount>, given: -10
</font></pre>
</blockquote>
</question>
<question title="Can a contract specify that the result depends on the arguments?" tag="arrow-d">
<p>Here is an excerpt from an imaginary (pardon the pun) <a
name="numerics-module">numerics module</a>:
<scheme>
(module numerics mzscheme
(require (lib "contract.ss"))
(provide/contract
[sqrt.v1 (->d (lambda (x) (>= x 1))
(lambda (argument)
(lambda (result)
(<= result argument))))]
...)
...)
</scheme>
The contract for the exported function @scheme[sqrt.v1] uses the
@scheme[->d] rather than @scheme[->] function contract. The "d"
stands for <em>dependent</em> contract, meaning the contract for the
function range depends on the value of the argument.
<p>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.]
<p>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.
<p>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:
<a name="deposit" />
<scheme>
(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)))))))]
... )
...
)
</scheme>
<p>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.
<p>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 <em>before</em> the range-checking function was
produced.
</question>
<question title="See: currying would help with contracts!" tag="curry">
<p>Exactly!
<p>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].
<p>Here is a revision of <a href="#numerics-module">the
@scheme[numerics] module</a> that exploits these special contract
combinators:
<scheme>
(module numerics mzscheme
(require (lib "contract.ss"))
(provide/contract
[sqrt.2 (->d (>=/c 1.0) <=/c)]
...)
...)
</scheme>
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.
<p>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.
<p>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.
</question>
<question title="Can a contract specify that arguments depend on each other?" tag="arrow-r">
<p>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.
<p>Suppose the account module provides the following two functions:
<scheme>
;; balance : Account -> Amount
;; withdraw : Account Amount -> Account
</scheme>
Then, informally, the proper precondition for @scheme[withdraw] is that
<blockquote>
"the balance of the given account is greater than or equal to the given (withdrawal) amount."
</blockquote>
The postcondition is similar to the one for <a
href="#deposit">@scheme[deposit]</a>:
<blockquote>
"the balance of the resulting account is larger than (or equal to) than the one of the
given account."
</blockquote>
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.
<p>The following module implements accounts imperatively and specifies the
conditions we just discussed:
<table>
<tr><td>
<scheme>
(module account mzscheme
(require (lib "contract.ss"))
<font color="deeppurple">
(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))</font>
<font color="purple">
(provide/contract
[create (amount . -> . account?)]
[balance (account? . -> . amount)]
[withdraw (->r ([acc account?]
[amt (and/c amount (&lt;/c (balance acc)))])
(mk-account-contract acc amt > msg>))]
[deposit (->r ([acc account?]
[amt amount])
(mk-account-contract acc amt < msg<))])
</font>
(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))
</scheme>
<td bgcolor="beige" valign="top">
<pre>
the contract definitions
the exports
the function definitions
</pre>
</table>
The purple part is the export interface:
<ol>
<li>@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).
</li>
<li>@scheme[balance] consumes an account and computes its current balance.
</li>
<li>@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.
<p>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.
</li>
<li>@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.
</li>
</ol>
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.
</question>
<question title="What about rest arguments?" tag="rest-args">
<p>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:
<scheme>
(define (plus fst snd . rst)
(foldr + (+ fst snd) rst))
</scheme>
Describing this function via a contract is difficult because of the rest
argument (@scheme[rst]).
<p>Here is the contract:
<scheme>
(provide/contract
[plus (->* (number? number?) (listof number?) (number?))])
</scheme>
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.
<p>The contracts for the required arguments are enclosed in an additional
pair of parentheses:
<scheme>
(number? number?)
</scheme>
For @scheme[plus] they demand two numbers. The contract for the
rest argument follows:
<scheme>
(listof number?)
</scheme>
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.
<p>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.
</question>
<question title="What about case-lambda?" tag="case-lambda">
<p><a href="http://www.scheme.com/csug/binding.html">Dybvig</a> explains
the meaning and pragmatics of @scheme[case-lambda] with the following
example (among others):
<scheme>
(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)]))
</scheme>
This version of @scheme[substring] has one of the following signature:
<ol>
<li>just a string, in which case it copies the string;
<li>a string and an index into the string, in which case it extracts the
suffix of the string starting at the index; or
<li>a string a start index and an end index, in which case it extracts the
fragment of the string between the two indices.
</ol>
<p>The contract for such a function is formed with the @scheme[case->]
combinator, which combines as many functional contracts as needed:
<scheme>
(provide/contract
[substring1 (case->
(string? . -> . string?)
(string? natural-number/c . -> . string?)
(string? natural-number/c natural-number/c . -> . string?))])
</scheme>
As you can see, the contract for @scheme[substring1] combines three
function contracts, just as many clauses as the explanation of its
functionality required.
<p>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:
<scheme>
(provide/contract
[substring1 (case->
(string? . -> . string?)
(->r ([s string?]
[_ (and/c natural-number/c (</c (string-length s)))])
string?)
(->r ([s string?]
[a (and/c natural-number/c (</c (string-length s)))]
[o (and/c natural-number/c
(>=/c a)
(</c (string-length s)))])
string?))])
</scheme>
Here we used @scheme[->r] to name the parameters and express the
numeric constraints on them.
</question>
<question title="What about multiple values?" tag="multiple">
<p>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:
<scheme>
(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 '()))
</scheme>
It is a typical multiple-value function, returning two values by
traversing a single list.
<p>
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:
<scheme>
(provide/contract
[split (-> (listof char?)
(values string? (listof char?)))])
</scheme>
</p>
<p>The contract for such a function can also be written
using @scheme[->*], just like
@scheme[plus]:
<scheme>
(provide/contract
[split (->* ((listof char?))
(string? (listof char?)))])
</scheme>
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.
</p>
<p>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:
<scheme>
(provide/contract
[splitp (->d* ((listof char?))
(lambda (fl)
(define wd (list->string fl))
(values (and/c string? (lambda (w) (string<=? w wd)))
(listof char?))))])
</scheme>
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.
<p>This contract is expensive to check of course. Here is a slightly
cheaper version:
<scheme>
(provide/contract
[splitl (->d* ((listof char?))
(lambda (fl)
(values (and/c string? (string/len (add1 (length fl))))
(listof char?))))])
</scheme>
Check the help desk for an explanation of @scheme[string/len].
</question>
<question title="What about procedures of any specific arity?" tag="no-domain">
<p>
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.
</p>
<p>Consider this @scheme[n-step] function:
<scheme>
;; (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)))))
</scheme>
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.
</p>
Here are two uses:
<table>
<tr>
<td width="20" />
<td valign="top">
<pre>@scheme[
;; Nat -> Nat
(define (f x)
(printf "~s \n" x)
(if (= x 0) #f -1))
(n-step f '(2))
]</pre></td>
<td width="150" />
<td valign="top" width="150"><pre>@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))
]</pre></td></tr>
</table>
</center>
<p>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
<em>variable-arity</em> to @scheme[proc]:
@scheme[
(->* ()
(listof any/c)
(or/c number? false/c))
]
This contract, however, says that the function must accept <em>any</em>
number of arguments, not a <em>specific</em> but
<em>undetermined</em> 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.
</p>
<p>
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:
<scheme>
(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)])
</scheme>
</p>
</question>
<question title="What about opt-lambda?" tag="opt-lambda">
<p>Take a look at this excerpt from a string-processing module, inspired by the
Scheme cookbook:
<scheme>
(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))))
</scheme>
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.
<p>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:
<ol>
<li>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].
<li>The second one is a parenthesized group of contracts for all optional
arguments: @scheme[char?].
<li>The last one is a single contract: the result of the function.
</ol>
Note if a default value does not satisfy a contract, you won't get a contract
error for this interface. We do trust <em>you</em>; 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.

62
collects/scribblings/guide/contracts-gotchas.scrbl Normal file
View File

@ -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))
<section title="Gotchas" tag="gotchas" />
<question> What about @scheme[set!] on variables provided via @scheme[provide/contract]?
</question>
<p>
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:
<scheme>
(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)
</scheme>
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]).
</p>
<p>
To work around this, export accessor functions, rather than
exporting the function directly, like this:
<scheme>
(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?)]))
</scheme>
</p>
<p>
This is a bug we hope to address in a future release.
</p>

183
collects/scribblings/guide/contracts-intro.scrbl Normal file
View File

@ -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.
==================================================
<question title="Example" tag="example">
<table src="simple.ss">
<tr><td bgcolor="e0e0fa">
<scheme>
;; 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) <font color="red">(set! amount -4)</font>))
(module b mzscheme
(require a)
(printf "~s~n" amount)
<font color="red">(do-it)</font>
(printf "~s~n" amount))
(require b)
</scheme>
<td bgcolor="beige" valign="top">
<pre>
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)
</pre> </table>
<p><strong>Note:</strong> 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 <strong>not</strong> 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>
}
@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.

7
collects/scribblings/guide/contracts-objects.scrbl Normal file
View File

@ -0,0 +1,7 @@
<section title="Contracts on Objects" tag="objs" />
<blockquote>
<!-- waiting for <code>this</code> in contracts -->
</blockquote>

273
collects/scribblings/guide/contracts-simple-function.scrbl Normal file
View File

@ -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))))))])
]

313
collects/scribblings/guide/contracts-structure.scrbl Normal file
View File

@ -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))
<section title="Contracts on Structures" tag="structs" />
<p>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.
<question title="Can a module promise something about a specific struct?" tag="single-struct">
<p>Yes. If your module defines a variable to be a structure, then on export you
can specify the structures shape:
<scheme>
(module geometry mzscheme
(require (lib "contract.ss"))
(require posn)
(define origin (make-posn 0 0))
...
(provide/contract
[origin (struct/c posn zero? zero?)]
...)
... )
</scheme>
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.
</question>
<question title="Can a module promise something about a specific vector?" tag="single-vector">
<p>Yes, again. See the help desk for information on @scheme[vector/c] and
similar contract combinators for (flat) compound data.
</question>
<question title="Can a contract enforce that all structs are well-formed?" tag="define-struct">
<p>"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:
<scheme>
(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)))
</scheme>
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.
<p>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.
<p>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 <em>not</em> enforce that the fields of
@scheme[p-sick] are numbers.
<p>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:
<scheme>
(module client mzscheme
(require posn)
... (posn-x p-sick) ...)
</scheme>
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.
<p>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
<scheme>
(define p-sick (make-posn 'a 'b))
</scheme>
to the module. So, when you are looking for bugs based on contract violations,
keep this example in mind.
<p><strong>Exercise 2:</strong> Use your knowledge from the <a href="#single-struct">
section on exporting specific structs</a> and change the contract for
@scheme[p-sick] so that the error is caught when clients refer to the
structure. <a href="#exercise2">Solution</a>
</question>
<question title="What about contracts that check properties of data structures?" tag="lazy-contracts">
<p>
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.
</p>
<p> 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. </p>
<p>
We can implement implement a search
function @scheme[in?] that takes advantage of the
structure of the binary search tree.
<scheme>
(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?)]))
</scheme>
In a full binary search tree, this means that
the @scheme[in?] function only has to explore a
logarithmic number of nodes.
</p>
<p>
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.
</p>
<p>
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.
</p>
<p>
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.
</p>
<p>
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:
<scheme>
(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?)]))
</scheme>
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.
</p>
<p>
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.
<scheme>
(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)])))
</scheme>
</p>
</question>
<question title="Solution to Exercise 2" tag="exercise2">
<p>A single change suffices:
<scheme>
(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 <font color="red">(struct/c posn number? number?)</font>])
(define p-okay (make-posn 10 20))
(define p-sick (make-posn 'a 'b)))
</scheme>
Instead of exporting @scheme[p-sick] as a plain @scheme[posn?], we use a
@scheme[struct/c] contract to enforce constraints on its components.
</question>

11
collects/scribblings/guide/contracts-utils.ss Normal file
View File

@ -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))

18
collects/scribblings/guide/contracts.scrbl Normal file
View File

@ -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"]
}

9
collects/scribblings/guide/guide.scrbl
View File

@ -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"]