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

a little more work on the contracts guide

Browse Source 
svn: r8254
This commit is contained in:
Robby Findler 2008-01-08 05:43:41 +00:00
parent eeb62f47f7
commit 1b31b38e1e
17 changed files with 643 additions and 492 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

71
collects/scribblings/guide/contracts-examples.scrbl
View File

@ -1,64 +1,48 @@
NOTE: this section needs the files in contract-examples/*ss
to be added to it (presumably programmatically).
#lang scribble/doc
@require[scribble/manual]
@require[scribble/eval]
@require["guide-utils.ss"]
@require["contracts-utils.ss"]
@(require (for-label scheme/contract)
(for-label scheme/gui))
<section title="Examples" tag="text-examples" />
@title{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
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>
@itemize{
@item{@bold{Separate queries from commands.}
<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
A @italic{query} returns a result but does not change the observable
properties of an object. A @italic{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.</p>
</li>
class.}
<li><b>Separate basic queries from derived queries.</b>
@item{@bold{Separate basic queries from derived queries}
<p>A <em>derived query</em> returns a result that is computable in
terms of basic queries.</p>
</li>
A @italic{derived query} returns a result that is computable in
terms of basic queries.}
<li><b>For each derived query, write a post-condition contract that
specifies the result in terms of the basic queries.</b>
@item{@bold{For each derived query, write a post-condition contract that
specifies the result in terms of the basic queries.}}
<p />
</li>
@item{@bold{For each command, write a post-condition contract that specifies the
changes to the observable properties in terms of the basic queries.}}
<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>
@item{@bold{For each query and command, decide on suitable pre-condition contract.}}}
<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
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
@ -66,19 +50,16 @@ to be added to it (presumably programmatically).
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>
contracts for those become available).
<p>Note: To mimic Mitchell and McKim's informal notion of parametericity
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/contracts-examples/1-test.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)

125
collects/scribblings/guide/contracts-examples/1.ss
View File

@ -2,122 +2,21 @@
;; --- common data definitions ------------------------------------------------
(module basic-customer-details mzscheme
(require (lib "contract.ss"))
#lang scheme
;; 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
)
;; data definitions
;; --- the customer manager ----------------------------------------------------
(define id? symbol?)
(define id-equal? eq?)
(define-struct basic-customer (id name address) #:mutable)
;; interface
(provide/contract
[id? (-> any/c boolean?)]
[id-equal? (-> id? id? boolean?)]
[struct basic-customer ((id id?) (name string?) (address string?))])
;; end of interface
(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)

61
collects/scribblings/guide/contracts-examples/1b.ss Normal file
View File

@ -0,0 +1,61 @@
;; --- the customer manager ----------------------------------------------------
#lang scheme
(require "1.ss")
;; 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 (->d ([id id?] [nn string?])
()
[result any/c] ;; result contract
#:post-cond
(string=? (name id) nn))]
[add (->d ([bc (and/c basic-customer? not-active?)])
()
;; A pre-post condition contract must use a side-effect
;; to express this contract via post-conditions
#:pre-cond (set! c0 count) ;; pre
[result any/c] ;; result contract
#:post-cond (> count c0))])
;; end of interface

105
collects/scribblings/guide/contracts-examples/2-test.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)

157
collects/scribblings/guide/contracts-examples/2.ss
View File

@ -1,105 +1,66 @@
;; chapter 2: A Parameteric (Simple) Stack
one-of
;; --- stack -------------------------------------------------------------------
(module stack mzscheme
(require (lib "contract.ss") (lib "etc.ss"))
;; a contract utility
(define (eq/c x) (lambda (y) (eq? x y)))
#lang scheme
;; implementation
(define-struct stack (list p? eq))
;; a contract utility
(define (eq/c x) (lambda (y) (eq? x y)))
(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
)
;; implementation
(define-struct stack (list p? eq))
;; --- 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))
(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
(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)
;; 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 (->d ([s stack?][i (and/c positive? (<=/c (count s)))])
()
[result (stack-p? s)])]
;; derived queries
;; is the stack empty?
[is-empty? (->d ([s stack?])
()
[result (eq/c (= (count s) 0))])]
;; which item is at the top of the stack
[top (->d ([s (and/c stack? not-empty?)])
()
[t (stack-p? s)] ;; a stack item, t is its name
#:post-cond
([stack-eq s] t (item-at s (count s))))]
;; creation
[initialize (->d ([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
[result (and/c stack? is-empty?)])]
;; commands
;; add an item to the top of the stack
[push (->d ([s stack?][x (stack-p? s)])
()
[sn stack?] ;; result kind
#:post-cond
(and (= (+ (count s) 1) (count sn))
([stack-eq s] x (top sn))))]
;; remove the item at the top of the stack
[pop (->d ([s (and/c stack? not-empty?)])
()
[sn stack?] ;; result kind
#:post-cond
(= (- (count s) 1) (count sn)))])
;; end of interface

22
collects/scribblings/guide/contracts-examples/3-test.ss Normal file
View File

@ -0,0 +1,22 @@
(module 3-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 "3.ss")
(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))))))

171
collects/scribblings/guide/contracts-examples/3.ss
View File

@ -2,106 +2,79 @@
;; --- dictionary --------------------------------------------------------------
(module dictionary mzscheme
(require (lib "contract.ss") (lib "etc.ss"))
#lang scheme
;; a contract utility
(define-syntax =>
(syntax-rules ()
[(=> antecedent consequent) (if antecedent consequent #t)]))
;; 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
;; implementation
(define-struct dictionary (l value? eq?))
;; the keys should probably be another parameter (exercise)
;; 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
)
(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 (rem 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
;; --- 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)
;; 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? (->d ([d dictionary?][k symbol?])
()
[result boolean?]
#:post-cond
((zero? (count d)) . ⇒ . (not result)))]
;; what is the value of key k in this dictionary?
[value-for (->d ([d dictionary?]
[k (and/c symbol? (lambda (k) (has? d k)))])
()
[result (dictionary-value? d)])]
;; initialization
;; post condition: for all k in symbol, (has? d k) is false.
[initialize (->d ([p contract?][eq (p p . -> . boolean?)])
()
[result (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 (->d ([d dictionary?]
[k (and symbol? (not-has? d))]
[v (dictionary-value? d)])
()
[result dictionary?]
#:post-cond
(and (has? result k)
(= (count d) (- (count result) 1))
([dictionary-eq? d] (value-for result k) v)))]
;; remove key k from this dictionary
[rem (->d ([d dictionary?]
[k (and/c symbol? (lambda (k) (has? d k)))])
()
[result (and/c dictionary? not-has?)]
#:post-cond
(= (count d) (+ (count result) 1)))])
;; end of interface

34
collects/scribblings/guide/contracts-examples/5-test.ss Normal file
View File

@ -0,0 +1,34 @@
(module 5-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))))
)

157
collects/scribblings/guide/contracts-examples/5.ss
View File

@ -2,101 +2,70 @@
;; --- 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>
#lang scheme
(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
)
;; Note: this queue doesn't implement the capacity restriction
;; of McKim and Mitchell's queue but this is really minor and easy to add.
;; --- tests -------------------------------------------------------------------
;; 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 (deq 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 ([q queue?]) () [result (listof (queue-p? q))])]
;; derived queries
[count (->d ([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).
()
[result (and/c natural-number/c (=/c (length (items q))))])]
[is-empty? (->d ([q queue?])
()
[result (and/c boolean? (eq/c (null? (items q))))])]
[head (->d ([q (and/c queue? (compose not is-empty?))])
()
[result (and/c (queue-p? q) (eq/c (car (items q))))])]
;; creation
[initialize (-> contract?
(contract? contract? . -> . boolean?)
(and/c queue? (compose null? items)))]
;; commands
[put (->d ([oldq queue?][i (queue-p? oldq)])
()
[result (and/c queue?
(lambda (q)
(define old-items (items oldq))
(equal? (items q) (append old-items (list i)))))])]
[deq (->d ([oldq (and/c queue? (compose not is-empty?))])
()
[result
(and/c queue?
(lambda (q)
(equal? (cdr (items oldq)) (items q))))])])
;; end of interface
(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)

27
collects/scribblings/guide/contracts-general-function.scrbl
View File

@ -4,12 +4,11 @@
@require["guide-utils.ss"]
@require["contracts-utils.ss"]
@(require (for-label scheme/contract)
(for-label srfi/13/string)
(for-label scheme/gui))
@title{Contracts on Functions in General}
@question[#:tag "flat-named-contracts"]{Why do the error messages contain "..."?}
@ctc-section[#:tag "flat-named-contracts"]{Contract error messages that contain ``...''}
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
@ -65,7 +64,7 @@ sudden quite readable:
@inset-flow{@schemeerror{bank-client broke the contract (-> amount
any) it had with myaccount on deposit; expected <amount>, given: -10"}}
@question[#:tag "optional"]{What about optional arguments?}
@ctc-section[#:tag "optional"]{Optional arguments}
Take a look at this excerpt from a string-processing module, inspired by the
@link["http://schemecookbook.org"]{Scheme cookbook}:
@ -101,9 +100,7 @@ functionality. The interesting point here is the formulation
of the contract for the @scheme[string-pad-center].
Like the contract combinator for
@scheme[->*], i.e., rest arguments, @scheme[opt->] demands several
groups of contracts:
The contract combinator @scheme[->*], demands several groups of contracts:
@itemize{
@item{The first one is a parenthesized group of contracts for all required
arguments. In this example, we see two: @scheme[string?] and
@ -128,7 +125,7 @@ the other function contract combinators, like we did in
the @scheme[substring1] function above.
@question[#:tag "rest-args"]{What about rest arguments?}
@ctc-section[#:tag "rest-args"]{Rest arguments}
We all know that @scheme[+] in Beginner Scheme is a function
that consumes at least two numbers but, in principle,
@ -173,7 +170,7 @@ Finally, you may have noticed that the contract for the function range
for those is that functions can return multiple values not just one, and
this is our next topic in this guide.
@question[#:tag "keywords"]{What about keyword arguments?}
@ctc-section[#:tag "keywords"]{Keyword arguments}
Sometimes, a function accepts many arguments and remembering
their order can be a nightmare. To help with such functions,
@ -237,7 +234,7 @@ five keyword arguments, one for each of the keywords
Also, just like in a function definition, the keywords in
the @scheme[->] may appear in any order.
@question[#:tag "optional-keywords"]{What about optional keyword arguments?}
@ctc-section[#:tag "optional-keywords"]{Optional keyword arguments}
Of course, many of the parameters in
@scheme[ask-yes-or-no-question] (from the previous question)
@ -274,7 +271,7 @@ sections. In this case, we have mandatory keywords
putting the mandatory keywords in the first section and the
optional ones in the second section.
@question[#:tag "arrow-d"]{Can a contract specify that the result depends on the arguments?}
@ctc-section[#:tag "arrow-d"]{When a function's result depends on its arguments}
Here is an excerpt from an imaginary (pardon the pun) numerics module:
@ -306,7 +303,7 @@ and @scheme[>=/c], and it pays off to look them up in the contract
section of the reference manual. They simplify contracts tremendously
and make them more accessible to potential clients.
@question[#:tag "arrow-d-args"]{Can a contract specify that arguments depend on each other?}
@ctc-section[#:tag "arrow-d-args"]{When contract arguments depend on each other}
Eventually bank customers want their money back. Hence, a module that
implements a bank account must include a method for withdrawing money. Of
@ -321,7 +318,7 @@ Suppose the account module provides the following two functions:
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
@questionlink["flat-named-contracts"]{@scheme[deposit]}:
@ctc-link["flat-named-contracts"]{@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,
@ -411,7 +408,7 @@ 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[#:tag "case-lambda"]{What about case-lambda?}
@ctc-section[#:tag "case-lambda"]{Contracts for @scheme[case-lambda]}
Dybvig, in Chapter 5 of the
@link["http://www.scheme.com/csug/"]{Chez Scheme User's Guide},
@ -475,7 +472,7 @@ In the case of @scheme[substring1], we also know that the indices
numeric constraints on them.
}
@question[#:tag "multiple"]{What about multiple values?}
@ctc-section[#:tag "multiple"]{Multiple result values}
The function @scheme[split] consumes a list of @scheme[char]s
and delivers the string that occurs before the first occurrence of
@ -555,7 +552,7 @@ This contract is expensive to check of course. Here is a slightly
]
Click on @scheme[string-len/c] to see what it does.
@question[#:tag "no-domain"]{What about procedures of any specific arity?}
@ctc-section[#:tag "no-domain"]{Procedures of some fixed, but statically unknown arity}
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

32
collects/scribblings/guide/contracts-gotchas.scrbl
View File

@ -7,7 +7,7 @@
@title{Gotchas}
@question{What about @scheme[set!] on variables provided via @scheme[provide/contract]?}
@ctc-section{Using @scheme[set!] to assign to 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
@ -51,3 +51,33 @@ scheme
]
This is a bug we hope to address in a future release.
@;{
@question{Contracts and @scheme[eq?]}
As a general rule, adding a contract to a program should
either leave the behavior of the program unchanged, or
should signal a contract violation. And this is almost true
for PLT Scheme contracts, with one exception: @scheme[eq?].
The @scheme[eq?] procedure is designed to be fast and does
not provide much in the way of guarantees, except that if it
returns true, it means that the two values behave
identically in all respects. Internally, this is implemented
as pointer equality at a low-level so it exposes information
about how PLT Scheme is implemented (and how contracts are
implemented).
Contracts interact poorly with @scheme[eq?] because function
contract checking is implemented internally as wrapper
functions. For example, consider this module:
@schememod[
scheme
(define (make-adder ))
(provide make-adder)
(provide/contract [make-adder (-> number? (-> number? number?))])
]
}

6
collects/scribblings/guide/contracts-intro.scrbl
View File

@ -45,7 +45,7 @@ scheme/base
(define amount ...)
]
@question[#:tag "amount0"]{What happens if @scheme[a] sets @scheme[amount] to 0?}
@ctc-section[#:tag "amount0"]{A first contract violation}
Suppose the creator of @scheme[a] had written
@schememod[
@ -60,7 +60,7 @@ 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]?}
@ctc-section[#:tag "qamount"]{A more subtle contract violation}
Suppose the creator of @scheme[a] had written
@schememod[
@ -181,7 +181,7 @@ the module boundary for a second time.
</question>
}
@question[#:tag "obligations"]{How can a ``server'' module impose obligations on its client?}
@ctc-section[#:tag "obligations"]{Imposing obligations on a module's clients}
On occasion, a module may want to enter a contract with
another module only if the other module abides by certain

16
collects/scribblings/guide/contracts-simple-function.scrbl
View File

@ -18,7 +18,7 @@ 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?}
@ctc-section[#:tag "argcontract"]{Restricting 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
@ -60,7 +60,7 @@ 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?}
@ctc-section[#:tag "arrow"]{Arrows}
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
@ -95,7 +95,7 @@ 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?}
@ctc-section[#:tag "dots"]{Infix contract notation}
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
@ -119,7 +119,7 @@ is really just a short-hand for
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?}
@ctc-section[#:tag "own"]{Rolling your own contracts for function arguments}
The @scheme[deposit] function adds the given number to the value of
@scheme[amount]. While the function's contract prevents clients from
@ -176,10 +176,10 @@ scheme
Lesson: learn about the built-in contracts in @schememodname[scheme/contract].
@question[#:tag "and-or"]{Are @scheme[and/c] and @scheme[or/c] contract combinators? What of @scheme[listof]?}
@ctc-section[#:tag "and-or"]{The @scheme[and/c], @scheme[or/c], and @scheme[listof] contract combinators}
The short answer is yes. Both @scheme[and/c] and @scheme[or/c]
ombine contracts and they do what you expect them to do.
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
@ -208,7 +208,7 @@ value satisfies @scheme[number?] and @scheme[integer?] and
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?}
@ctc-section[#:tag "range"]{Restricting the range of a function}
Consider a utility module for creating strings from banking records:

10
collects/scribblings/guide/contracts-structure.scrbl
View File

@ -17,7 +17,7 @@ its fields contain values of a certain kind. This section
explains how to protect structs with contracts for both
uses.
@question[#:tag "single-struct"]{Can a module promise something about a specific struct?}
@ctc-section[#:tag "single-struct"]{Promising something about a specific struct}
Yes. If your module defines a variable to be a structure, then on export you
can specify the structures shape:
@ -35,12 +35,12 @@ 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., @tt{(0,0)}, of the grid.
@question[#:tag "single-vector"]{Can a module promise something about a specific vector?}
@ctc-section[#:tag "single-vector"]{Promising something about a specific vector}
Yes, again. See the help desk for information on @scheme[vector/c] and
similar contract combinators for (flat) compound data.
@question[#:tag "define-struct"]{Can a contract enforce that all structs are well-formed?}
@ctc-section[#:tag "define-struct"]{Ensuring that all structs are well-formed}
The book @link["http://www.htdp.org/"]{@italic{How to Design
Programs}} teaches that @scheme[posn]s should contain only
@ -111,7 +111,7 @@ reated a @scheme[posn] from symbols, i.e., the programmer who added
keep this example in mind.
@(exercise) Use your knowledge from the
@questionlink["single-struct"] section on exporting specific
@ctc-link["single-struct"] section on exporting specific
structs and change the contract for @scheme[p-sick] so that
the error is caught when @scheme[sick] is exported.
@ -128,7 +128,7 @@ A single change suffices:
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[#:tag "lazy-contracts"]{What about contracts that check properties of data structures?}
@ctc-section[#:tag "lazy-contracts"]{Checking properties of data structures}
Contracts written using @scheme[struct/c] immediately
check the fields of the data structure, but sometimes this

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

@ -2,8 +2,8 @@
(require scribble/basic
scribble/manual)
(provide ctc-section question
ctc-link questionlink
(provide ctc-section
ctc-link
exercise
solution)
@ -13,12 +13,8 @@
(list (and tag (str->tag tag)))
rest))
(define question ctc-section)
(define (ctc-link tag . rest) (apply seclink (str->tag tag) rest))
(define questionlink ctc-link)
(define (str->tag tag) (format "contracts-~a" tag))
(define exercise-number 0)
@ -27,4 +23,5 @@
(bold (format "Exercise ~a" exercise-number)))
(define (solution)
(bold (format "Solution to exercise ~a" exercise-number)))
(bold (format "Solution to exercise ~a" exercise-number)))

7
collects/scribblings/guide/contracts.scrbl
View File

@ -34,8 +34,7 @@ update string-pad-center to show examples via REPL notation:
@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["contracts-class.scrbl"]}
@include-section["contracts-examples.scrbl"]
@include-section["contracts-gotchas.scrbl"]