added the example section

svn: r8266
This commit is contained in:
Robby Findler 2008-01-08 23:30:49 +00:00
parent 6352736822
commit 364d7ff274
14 changed files with 225 additions and 402 deletions

View File

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

View File

@ -40,46 +40,58 @@ Mitchell and McKim's principles for design by contract DbC are derived
@item{@bold{For each command, write a post-condition contract that specifies the
changes to the observable properties in terms of the basic queries.}}
@item{@bold{For each query and command, decide on suitable pre-condition contract.}}}
@item{@bold{For each query and command, decide on suitable
pre-condition contract.}}}
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.
Each of the following sections corresponds to a chapter in
Mitchell and McKim's book (but not all chapters show up
here). We recommend that you read the contracts first (near
the end of the first modules), then the implementation (in
the first modules), and then the test module (at the end of
each section).
Mitchell and McKim use Eiffel as the underlying programming language and
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).
structure-oriented imperative Scheme, and PLT Scheme's class system.
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).
@; @external-file[1]
@section{A Customer Manager Component for Managing Customer Relationships}
@begin[
#reader scribble/comment-reader
[schememod
scheme
;; data definitions
(define id? symbol?)
(define id-equal? eq?)
(define-struct basic-customer (id name address) #:mutable)
This first module contains some struct definitions in a
separate module in order to better track bugs.
;; interface
(provide/contract
[id? (-> any/c boolean?)]
[id-equal? (-> id? id? boolean?)]
[struct basic-customer ((id id?) (name string?) (address string?))])
;; end of interface
]]
@external-file[1]
This module contains the program that uses the above.
@external-file[1b]
The tests:
@external-file[1-test]
@section{A Parameteric (Simple) Stack}
@external-file[2]
The tests:
@external-file[2-test]
@section{A Dictionary}
@external-file[3]
The tests:
@external-file[3-test]
@section{A Queue}
@external-file[5]
The tests:
@external-file[5-test]

View File

@ -1,123 +1,19 @@
;; chapter 1: A Customer Manager Component for Managing Customer Relationships
#lang mzscheme
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2)))
(require "1.ss" "1b.ss")
;; --- common data definitions ------------------------------------------------
(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"))
(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
)
(test/text-ui
(test-suite
"manager"
(test-equal? "id lookup" "matthias" (name 'mf))
(test-equal? "count" 4 count)
(test-true "active?" (active? 'mf))
(test-false "active? 2" (active? 'kk))
(test-true "set name" (void? (set-name 'mf "matt")))))
;; --- 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)

View File

@ -1,9 +1,4 @@
;; chapter 1: A Customer Manager Component for Managing Customer Relationships
;; --- common data definitions ------------------------------------------------
; #lang scheme
#lang scheme
;; data definitions
(define id? symbol?)
@ -14,7 +9,9 @@
(provide/contract
[id? (-> any/c boolean?)]
[id-equal? (-> id? id? boolean?)]
[struct basic-customer ((id id?) (name string?) (address string?))])
[struct basic-customer ((id id?)
(name string?)
(address string?))])
;; end of interface

View File

@ -1,15 +1,14 @@
;; --- the customer manager ----------------------------------------------------
#lang scheme
(require "1.ss")
(require "1.ss") ;; the module just above
;; 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 (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))
@ -36,7 +35,6 @@
(define c0 0)
;; end of implementation
;; interface
(provide/contract
;; how many customers are in the db?
[count natural-number/c]
@ -53,9 +51,9 @@
[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
;; A pre-post condition contract must use
;; a side-effect to express this contract
;; via post-conditions
#:pre-cond (set! c0 count)
[result any/c] ;; result contract
#:post-cond (> count c0))])
;; end of interface

View File

@ -1,105 +1,23 @@
;; chapter 2: A Parameteric (Simple) Stack
#lang scheme
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2))
"2.ss")
;; --- stack -------------------------------------------------------------------
(define s0 (initialize (flat-contract integer?) =))
(define s2 (push (push s0 2) 1))
(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)
(test/text-ui
(test-suite
"stack"
(test-true
"empty"
(is-empty? (initialize (flat-contract integer?) =)))
(test-true "push" (stack? s2))
(test-true
"push exn"
(with-handlers ([exn:fail:contract? (lambda _ #t)])
(push (initialize (flat-contract integer?)) 'a)
#f))
(test-true "pop" (stack? (pop s2)))
(test-equal? "top" (top s2) 1)
(test-equal? "toppop" (top (pop s2)) 2)))

View File

@ -1,13 +1,8 @@
;; chapter 2: A Parameteric (Simple) Stack
one-of
;; --- stack -------------------------------------------------------------------
#lang scheme
;; 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))
@ -17,50 +12,62 @@ one-of
(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 (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 (->d ([s stack?][i (and/c positive? (<=/c (count s)))])
()
[result (stack-p? s)])]
[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))])]
[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))))]
[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?)])]
[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))))]
[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
[pop
(->d ([s (and/c stack? not-empty?)])
()
[sn stack?] ;; result kind
#:post-cond
(= (- (count s) 1) (count sn)))])

View File

@ -1,22 +1,14 @@
(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))
#lang scheme
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2))
"3.ss")
(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))))))
(define d0 (initialize (flat-contract integer?) =))
(define d (put (put (put d0 'a 2) 'b 2) 'c 1))
(test/text-ui
(test-suite
"dictionaries"
(test-equal? "value for" 2 (value-for d 'b))
(test-false "has?" (has? (rem d 'b) 'b))
(test-equal? "count" 3 (count d))))

View File

@ -1,7 +1,3 @@
;; chapter 3: A Dictionary
;; --- dictionary --------------------------------------------------------------
#lang scheme
;; a contract utility
@ -57,10 +53,10 @@
()
[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
;; 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)])

View File

@ -1,34 +1,21 @@
(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))))
)
#lang scheme
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2))
"5.ss")
(define s (put (put (initialize (flat-contract integer?) =) 2) 1))
(test/text-ui
(test-suite
"queue"
(test-true
"empty"
(is-empty? (initialize (flat-contract integer?) =)))
(test-true "put" (queue? s))
(test-equal? "count" 2 (count s))
(test-true "put exn"
(with-handlers ([exn:fail:contract? (lambda _ #t)])
(put (initialize (flat-contract integer?)) 'a)
#f))
(test-true "remove" (queue? (rem s)))
(test-equal? "head" 2 (head s))))

View File

@ -1,11 +1,7 @@
;; chapter 5: A Queue
;; --- queue -------------------------------------------------------------------
#lang scheme
;; Note: this queue doesn't implement the capacity restriction
;; of McKim and Mitchell's queue but this is really minor and easy to add.
;; of McKim and Mitchell's queue but this is easy to add.
;; a contract utility
(define (all-but-last l) (reverse (cdr (reverse l))))
@ -17,23 +13,30 @@
(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)))
(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 (rem 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
;; 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>
;; exactly as cheap as count.
[items (->d ([q queue?]) () [result (listof (queue-p? q))])]
;; derived queries
[count (->d ([q queue?])
;; We could express this second part of the post
@ -41,26 +44,34 @@
;; 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))))])]
[result (and/c natural-number/c
(=/c (length (items q))))])]
[is-empty? (->d ([q queue?])
()
[result (and/c boolean? (eq/c (null? (items q))))])]
[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))))])]
[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)))))])]
[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?))])
[rem (->d ([oldq (and/c queue? (compose not is-empty?))])
()
[result
(and/c queue?

View File

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

View File

@ -2,6 +2,7 @@
(require scribble/basic
(for-syntax scheme/port)
scheme/include
(except-in scribble/manual link))
(provide ctc-section
@ -28,6 +29,7 @@
(define (solution)
(bold (format "Solution to exercise ~a" exercise-number)))
#;
(define-syntax (external-file stx)
(syntax-case stx ()
[(_ filename)
@ -43,4 +45,27 @@
(open-input-string suffix))))])
#'s)))]))
;(external-file 1)
(require (for-syntax (only-in scribble/comment-reader [read-syntax comment-reader])))
(define-for-syntax (comment-schememod-reader path port)
(let ([pb (peek-byte port)])
(if (eof-object? pb)
pb
(let ([m (regexp-match #rx"^#lang " port)])
(unless m
(raise-syntax-error 'comment-scheme-reader "expected a #lang to begin file ~s" path))
(let ([np (let-values ([(line col pos) (port-next-location port)])
(relocate-input-port port line 0 pos))])
(port-count-lines! np)
(let loop ([objects '()])
(let ([next (comment-reader path np)])
(cond
[(eof-object? next)
#`(schememod #,@(reverse objects))]
[else
(loop (cons next objects))]))))))))
(define-syntax (external-file stx)
(syntax-case stx ()
[(_ filename)
#`(include/reader #,(format "contracts-examples/~a.ss" (syntax-e #'filename))
comment-schememod-reader)]))

View File

@ -34,7 +34,5 @@ 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-examples.scrbl"]
@include-section["contracts-gotchas.scrbl"]