--This section illustrates the current state of PLT Scheme's contract implementation with a series of examples from Mitchell and McKim's text book "Design by Contract, by Example" [Addison and Wesley, 2002]. -
-
Mitchell and McKim's principles for design by contract DbC are derived +Mitchell and McKim's principles for design by contract DbC are derived from the 1970s style algebraic specifications. The overall goal of DbC is to specify the constructors of an algebra in terms of its observers. While we reformulate Mitchell and McKim's terminology, we retain their terminology of "classes" and "objects" even though we reformulate their examples in an applicative style (as well as an imperative one): -
-A query returns a result but does not change the observable - properties of an object. A command changes the visible + 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.
-A derived query returns a result that is computable in - terms of basic queries.
--diff --git a/collects/scribblings/guide/contracts-examples/1-test.ss b/collects/scribblings/guide/contracts-examples/1-test.ss new file mode 100644 index 0000000000..1ecb08ac7d --- /dev/null +++ b/collects/scribblings/guide/contracts-examples/1-test.ss @@ -0,0 +1,123 @@ +;; chapter 1: A Customer Manager Component for Managing Customer Relationships + +;; --- common data definitions ------------------------------------------------ + +(module basic-customer-details mzscheme + (require (lib "contract.ss")) + + ;; data definitions + + (define id? symbol?) + (define id-equal? eq?) + (define-struct basic-customer (id name address)) + + ;; interface + (provide/contract + [id? (-> any/c boolean?)] + [id-equal? (-> id? id? boolean?)] + [struct basic-customer ((id id?) (name string?) (address string?))]) + ;; end of interface + ) + +;; --- the customer manager ---------------------------------------------------- + +(module customer-manager mzscheme + (require (lib "contract.ss") (lib "etc.ss") (lib "list.ss")) + + (require basic-customer-details) + + ;; implementation + ;; [listof (list basic-customer? secret-info)] + (define all '()) + + (define (find c) + (define (has-c-as-key p) (id-equal? (basic-customer-id (car p)) c)) + (define x (filter has-c-as-key all)) + (if (pair? x) (car x) x)) + + (define (active? c) + (define f (find c)) + (pair? (find c))) + + (define not-active? (compose not active? basic-customer-id)) + + (define count 0) + + (define (add c) + (set! all (cons (list c 'secret) all)) + (set! count (+ count 1))) + + (define (name id) + (define bc-with-id (find id)) + (basic-customer-name (car bc-with-id))) + + (define (set-name id name) + (define bc-with-id (find id)) + (set-basic-customer-name! (car bc-with-id) name)) + + (define c0 0) + ;; end of implementation + + ;; interface + (provide/contract + ;; how many customers are in the db? + [count natural-number/c] + ;; is the customer with this id active? + [active? (-> id? boolean?)] + ;; what is the name of the customer with this id? + [name (-> (and/c id? active?) string?)] + ;; change the name of the customer with this id + [set-name (->pp ([id id?] [nn string?]) + #t ;; no additional precondition + any/c ;; result contract + ____ ;; the result's name (irrelevant) + ;; the postcondition + (string=? (name id) nn))] + ;; add a customer + [add (->d (and/c basic-customer? not-active?) + (lambda (bc) + (let ([c0 count]) + (lambda (void) (> count c0)))))] + #; + [add (->pp ([bc (and/c basic-customer? not-active?)]) + ;; A pre-post condition contract must use a side-effect + ;; to express this contract via post-conditions + (set! c0 count) ;; pre + any/c ;; result contract + _____ ;; result name + (> count c0))]) + ;; end of interface + ) + +;; --- tests ------------------------------------------------------------------- + +(module test mzscheme + (require (planet "test.ss" ("schematics" "schemeunit.plt" 1 2)) + (planet "text-ui.ss" ("schematics" "schemeunit.plt" 1 2))) + (require basic-customer-details customer-manager) + + (add (make-basic-customer 'mf "matthias" "brookstone")) + (add (make-basic-customer 'rf "robby" "beverly hills park")) + (add (make-basic-customer 'fl "matthew" "pepper clouds town")) + (add (make-basic-customer 'sk "shriram" "i city")) + + (test/text-ui + (make-test-suite + "manager" + (make-test-case + "id lookup" + (assert equal? "matthias" (name 'mf))) + (make-test-case + "count" + (assert = 4 count)) + (make-test-case + "active?" + (assert-true (active? 'mf))) + (make-test-case + "active? 2" + (assert-false (active? 'kk))) + (make-test-case + "set name" + (assert-true (void? (set-name 'mf "matt"))))))) + +(require test) diff --git a/collects/scribblings/guide/contracts-examples/1.ss b/collects/scribblings/guide/contracts-examples/1.ss index 1ecb08ac7d..edc63d0ded 100644 --- a/collects/scribblings/guide/contracts-examples/1.ss +++ b/collects/scribblings/guide/contracts-examples/1.ss @@ -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?)]) - ;; A pre-post condition contract must use a side-effect - ;; to express this contract via post-conditions - (set! c0 count) ;; pre - any/c ;; result contract - _____ ;; result name - (> count c0))]) - ;; end of interface - ) -;; --- tests ------------------------------------------------------------------- -(module test mzscheme - (require (planet "test.ss" ("schematics" "schemeunit.plt" 1 2)) - (planet "text-ui.ss" ("schematics" "schemeunit.plt" 1 2))) - (require basic-customer-details customer-manager) - - (add (make-basic-customer 'mf "matthias" "brookstone")) - (add (make-basic-customer 'rf "robby" "beverly hills park")) - (add (make-basic-customer 'fl "matthew" "pepper clouds town")) - (add (make-basic-customer 'sk "shriram" "i city")) - - (test/text-ui - (make-test-suite - "manager" - (make-test-case - "id lookup" - (assert equal? "matthias" (name 'mf))) - (make-test-case - "count" - (assert = 4 count)) - (make-test-case - "active?" - (assert-true (active? 'mf))) - (make-test-case - "active? 2" - (assert-false (active? 'kk))) - (make-test-case - "set name" - (assert-true (void? (set-name 'mf "matt"))))))) -(require test) diff --git a/collects/scribblings/guide/contracts-examples/1b.ss b/collects/scribblings/guide/contracts-examples/1b.ss new file mode 100644 index 0000000000..cb3a985091 --- /dev/null +++ b/collects/scribblings/guide/contracts-examples/1b.ss @@ -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 diff --git a/collects/scribblings/guide/contracts-examples/2-test.ss b/collects/scribblings/guide/contracts-examples/2-test.ss new file mode 100644 index 0000000000..b38b627050 --- /dev/null +++ b/collects/scribblings/guide/contracts-examples/2-test.ss @@ -0,0 +1,105 @@ +;; chapter 2: A Parameteric (Simple) Stack + +;; --- stack ------------------------------------------------------------------- + +(module stack mzscheme + (require (lib "contract.ss") (lib "etc.ss")) + + ;; a contract utility + (define (eq/c x) (lambda (y) (eq? x y))) + + ;; implementation + (define-struct stack (list p? eq)) + + (define (initialize p? eq) (make-stack '() p? eq)) + (define (push s x) + (make-stack (cons x (stack-list s)) (stack-p? s) (stack-eq s))) + (define (item-at s i) (list-ref (reverse (stack-list s)) (- i 1))) + (define (count s) (length (stack-list s))) + (define (is-empty? s) (null? (stack-list s))) + (define not-empty? (compose not is-empty?)) + (define (pop s) (make-stack (cdr (stack-list s)) (stack-p? s) (stack-eq s))) + (define (top s) (car (stack-list s))) + ;; end of implementation + + ;; interface + (provide/contract + ;; predicate + [stack? (-> any/c boolean?)] + ;; primitive queries + ;; how many items are on the stack? + [count (-> stack? natural-number/c)] + ;; which item is at the given position? + [item-at (->r ([s stack?][i (and/c positive? (<=/c (count s)))]) + (stack-p? s))] + ;; derived queries + ;; is the stack empty? + [is-empty? (->d stack? (lambda (s) (eq/c (= (count s) 0))))] + ;; which item is at the top of the stack + [top (->pp ([s (and/c stack? not-empty?)]) + #t ;; no precondition + (stack-p? s) ;; a stack item + t ;; the name of the result + ;; the postcondition + ([stack-eq s] t (item-at s (count s))))] + ;; creation + [initialize (->r ([p contract?][s (p p . -> . boolean?)]) + ;; Mitchel and McKim use (= (count s) 0) here to express + ;; the post-condition in terms of a primitive query + (and/c stack? is-empty?))] + ;; commands + ;; add an item to the top of the stack + [push (->pp ([s stack?][x (stack-p? s)]) + #t ;; pre + stack? ;; result kind + sn ;; name of result + ;; post: + (and (= (+ (count s) 1) (count sn)) + ([stack-eq s] x (top sn))))] + ;; remove the item at the top of the stack + [pop (->pp ([s (and/c stack? not-empty?)]) + #t ;; pre + stack? ;; result kind + sn ;; name of result + ;; post: + (= (- (count s) 1) (count sn)))]) + ;; end of interface + ) + +;; --- tests ------------------------------------------------------------------- + +(module test mzscheme + (require (planet "test.ss" ("schematics" "schemeunit.plt" 1 2)) + (planet "text-ui.ss" ("schematics" "schemeunit.plt" 1 2))) + (require (lib "contract.ss")) + (require stack) + + (define s (push (push (initialize (flat-contract integer?) =) 2) 1)) + + (test/text-ui + (make-test-suite + "stack" + (make-test-case + "empty" + (assert-true (is-empty? (initialize (flat-contract integer?) =)))) + (make-test-case + "push" + (assert-true (stack? s))) + (make-test-case + "push exn" + ;; Noel & Ryan: this is how things should work: + #;(assert-exn exn:fail:contract? + (push (initialize (flat-contract integer?)) 'a)) + ;; this is what I have to do: + (assert-true (with-handlers ([exn:fail:contract? (lambda _ #t)]) + (push (initialize (flat-contract integer?)) 'a) + #f))) + (make-test-case + "pop" + (assert-true (stack? (pop s)))) + (make-test-case + "top" + (assert = (top s) 1)))) + ) + +(require test) diff --git a/collects/scribblings/guide/contracts-examples/2.ss b/collects/scribblings/guide/contracts-examples/2.ss index b38b627050..b7c01252ae 100644 --- a/collects/scribblings/guide/contracts-examples/2.ss +++ b/collects/scribblings/guide/contracts-examples/2.ss @@ -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" - ;; Noel & Ryan: this is how things should work: - #;(assert-exn exn:fail:contract? - (push (initialize (flat-contract integer?)) 'a)) - ;; this is what I have to do: - (assert-true (with-handlers ([exn:fail:contract? (lambda _ #t)]) - (push (initialize (flat-contract integer?)) 'a) - #f))) - (make-test-case - "pop" - (assert-true (stack? (pop s)))) - (make-test-case - "top" - (assert = (top s) 1)))) - ) - -(require test) +;; 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 diff --git a/collects/scribblings/guide/contracts-examples/3-test.ss b/collects/scribblings/guide/contracts-examples/3-test.ss new file mode 100644 index 0000000000..8c778f2ad6 --- /dev/null +++ b/collects/scribblings/guide/contracts-examples/3-test.ss @@ -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)))))) + \ No newline at end of file diff --git a/collects/scribblings/guide/contracts-examples/3.ss b/collects/scribblings/guide/contracts-examples/3.ss index 4249a0a80c..4b4767bc28 100644 --- a/collects/scribblings/guide/contracts-examples/3.ss +++ b/collects/scribblings/guide/contracts-examples/3.ss @@ -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 diff --git a/collects/scribblings/guide/contracts-examples/5-test.ss b/collects/scribblings/guide/contracts-examples/5-test.ss new file mode 100644 index 0000000000..754a1e9026 --- /dev/null +++ b/collects/scribblings/guide/contracts-examples/5-test.ss @@ -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)))) + ) diff --git a/collects/scribblings/guide/contracts-examples/5.ss b/collects/scribblings/guide/contracts-examples/5.ss index a80e63d4a9..c6b81bdd9d 100644 --- a/collects/scribblings/guide/contracts-examples/5.ss +++ b/collects/scribblings/guide/contracts-examples/5.ss @@ -2,101 +2,70 @@ ;; --- queue ------------------------------------------------------------------- -;; Note: this queue doesn't implement the capacity restriction -;; of McKim and Mitchell's queue but this is really minor and easy to add. +#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 - ;; Imagine providing this 'query' for the interface of the module - ;; only. Then in Scheme, there is no reason to have count or is-empty? - ;; around (other than providing it to clients). After all items is - ;; exactly as cheap as count. - [items (->d queue? (compose listof queue-p?))] - ;; derived queries - [count (->r ([q queue?]) - ;; We could express this second part of the post - ;; condition even if count were a module "attribute" - ;; in the language of Eiffel; indeed it would use the - ;; exact same syntax (minus the arrow and domain). - (and/c natural-number/c (=/c (length (items q)))))] - [is-empty? (->r ([q queue?]) - (and/c boolean? (eq/c (null? (items q)))))] - [head (->r ([q (and/c queue? (compose not is-empty?))]) - (and/c (queue-p? q) (eq/c (car (items q)))))] - ;; creation - [initialize (-> contract? (contract? contract? . -> . boolean?) - (and/c queue? (compose null? items)))] - ;; commands - [put (->r ([oldq queue?][i (queue-p? oldq)]) - (and/c queue? - (lambda (q) - (define old-items (items oldq)) - (equal? (items q) (append old-items (list i))))))] - [remove (->r ([oldq (and/c queue? (compose not is-empty?))]) - (and/c queue? - (lambda (q) - (equal? (cdr (items oldq)) (items q)))))]) - ;; end of interface - ) +;; 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 + ;; Imagine providing this 'query' for the interface of the module + ;; only. Then in Scheme, there is no reason to have count or is-empty? + ;; around (other than providing it to clients). After all items is + ;; exactly as cheap as count. + [items (->d ([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) diff --git a/collects/scribblings/guide/contracts-general-function.scrbl b/collects/scribblings/guide/contracts-general-function.scrbl index 533bb556b8..d628efee03 100644 --- a/collects/scribblings/guide/contracts-general-function.scrbl +++ b/collects/scribblings/guide/contracts-general-function.scrbl @@ -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; expectedEach 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 so that they are easy to find. Implementations @@ -66,19 +50,16 @@ to be added to it (presumably programmatically). Finally, tests are included in a light shade. We recommend that you read the contracts first, then the implementation, and then the test module. -
-+ Mitchell and McKim use Eiffel as the underlying programming language and employ a conventional imperative programming style. Our long-term goal is to transliterate their examples into applicative Scheme, structure-oriented imperative Scheme, and PLT Scheme's class system (when - contracts for those become available).
+ contracts for those become available). -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). -
-