► |  | Guide: PLT Scheme

1 | Welcome to PLT Scheme
2 | Scheme Essentials
3 | Built-In Datatypes
4 | Expressions and Definitions
5 | Programmer-Defined Datatypes
6 | Modules
7 | Contracts
8 | Input and Output
9 | Regular Expressions
10 | Exceptions and Control
11 | Iterations and Comprehensions
12 | Pattern Matching
13 | Classes and Objects
14 | Units (Components)
15 | Reflection and Dynamic Evaluation
16 | Macros
17 | Performance
18 | Running and Creating Executables
19 | Compilation and Configuration
20 | More Libraries
21 | Dialects of Scheme
| Bibliography
| Index

▼ | 7 | Contracts

7.1 | Contracts and Boundaries
7.2 | Simple Contracts on Functions
7.3 | Contracts on Functions in General
7.4 | Contracts on Structures
7.5 | Examples
7.6 | Gotchas

► | 7.5 | Examples

7.5.1 | A Customer Manager Component for Managing Customer Relationships
7.5.2 | A Parameteric (Simple) Stack
7.5.3 | A Dictionary
7.5.4 | A Queue

On this page:

7.5.1`` A Customer Manager Component for Managing Customer Relationships
7.5.2`` A Parameteric (Simple) Stack
7.5.3`` A Dictionary
7.5.4`` A Queue

Version: 4.1.4
top← prev up next →

#### 7.5`` Examples

This section illustrates the current state of PLT Scheme’s contract implementation with a series of examples from Design by Contract, by Example [Mitchell02].

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 and we use a mostly applicative, we retain their terminology of “classes” and “objects”:

- Separate queries from commands.

  A query returns a result but does not change the observable properties of an object. A command changes the visible properties of an object, but does not return a result. In applicative implementation a command typically returns an new object of the same class.

- Separate basic queries from derived queries

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

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

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

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

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

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

##### 7.5.1`` A Customer Manager Component for Managing Customer Relationships

This first module contains some struct definitions in a separate module in order to better track bugs.

#lang scheme
; d a t a d e f i n i t i o n s
(define id? symbol?)
(define id-equal? eq?)
(define-struct basic-customer (id name address) #:mutable)
; i n t e r f a c e
(provide/contract
[id? (-> any/c boolean?)]
[id-equal? (-> id? id? boolean?)]
[struct basic-customer ((id id?)
(name string?)
(address string?))])
; e n d o f i n t e r f a c e

This module contains the program that uses the above.

#lang scheme
(require "1.ss") ; t h e m o d u l e j u s t a b o v e
; i m p l e m e n t a t i o n
; [l i s t o f (l i s t b a s i c-c u s t o m e r? s e c r e t-i n f o)]
(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)
; e n d o f i m p l e m e n t a t i o n
(provide/contract
; h o w m a n y c u s t o m e r s a r e i n t h e d b?
[count natural-number/c]
; i s t h e c u s t o m e r w i t h t h i s i d a c t i v e?
[active? (-> id? boolean?)]
; w h a t i s t h e n a m e o f t h e c u s t o m e r w i t h t h i s i d?
[name (-> (and/c id? active?) string?)]
; c h a n g e t h e n a m e o f t h e c u s t o m e r w i t h t h i s i d
[set-name (->d ([id id?] [nn string?])
()
[result any/c] ; r e s u l t c o n t r a c t
#:post-cond
(string=? (name id) nn))]
[add (->d ([bc (and/c basic-customer? not-active?)])
()
; A p r e-p o s t c o n d i t i o n c o n t r a c t m u s t u s e
; a s i d e-e f f e c t t o e x p r e s s t h i s c o n t r a c t
; v i a p o s t-c o n d i t i o n s
#:pre-cond (set! c0 count)
[result any/c] ; r e s u l t c o n t r a c t
#:post-cond (> count c0))])

The tests:

#lang scheme
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2)))
(require "1.ss" "1b.ss")
(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
(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")))))

##### 7.5.2`` A Parameteric (Simple) Stack

#lang scheme
; a c o n t r a c t u t i l i t y
(define (eq/c x) (lambda (y) (eq? x y)))
(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)))
(provide/contract
; p r e d i c a t e
[stack? (-> any/c boolean?)]
; p r i m i t i v e q u e r i e s
; h o w m a n y i t e m s a r e o n t h e s t a c k?
[count (-> stack? natural-number/c)]
; w h i c h i t e m i s a t t h e g i v e n p o s i t i o n?
[item-at
(->d ([s stack?][i (and/c positive? (<=/c (count s)))])
()
[result (stack-p? s)])]
; d e r i v e d q u e r i e s
; i s t h e s t a c k e m p t y?
[is-empty?
(->d ([s stack?])
()
[result (eq/c (= (count s) 0))])]
; w h i c h i t e m i s a t t h e t o p o f t h e s t a c k
[top
(->d ([s (and/c stack? not-empty?)])
()
[t (stack-p? s)] ; a s t a c k i t e m, t i s i t s n a m e
#:post-cond
([stack-eq s] t (item-at s (count s))))]
; c r e a t i o n
[initialize
(->d ([p contract?][s (p p . -> . boolean?)])
()
; M i t c h e l a n d M c K i m u s e (= (c o u n t s) 0) h e r e t o e x p r e s s
; t h e p o s t-c o n d i t i o n i n t e r m s o f a p r i m i t i v e q u e r y
[result (and/c stack? is-empty?)])]
; c o m m a n d s
; a d d a n i t e m t o t h e t o p o f t h e s t a c k
[push
(->d ([s stack?][x (stack-p? s)])
()
[sn stack?] ; r e s u l t k i n d
#:post-cond
(and (= (+ (count s) 1) (count sn))
([stack-eq s] x (top sn))))]
; r e m o v e t h e i t e m a t t h e t o p o f t h e s t a c k
[pop
(->d ([s (and/c stack? not-empty?)])
()
[sn stack?] ; r e s u l t k i n d
#:post-cond
(= (- (count s) 1) (count sn)))])

The tests:

#lang scheme
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2))
"2.ss")
(define s0 (initialize (flat-contract integer?) =))
(define s2 (push (push s0 2) 1))
(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)))

##### 7.5.3`` A Dictionary

#lang scheme
; a s h o r t h a n d f o r u s e b e l o w
(define-syntax ⇒
(syntax-rules ()
[(⇒ antecedent consequent) (if antecedent consequent #t)]))
; i m p l e m e n t a t i o n
(define-struct dictionary (l value? eq?))
; t h e k e y s s h o u l d p r o b a b l y b e a n o t h e r p a r a m e t e r (e x e r c i s e)
(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))))
; e n d o f i m p l e m e n t a t i o n
; i n t e r f a c e
(provide/contract
; p r e d i c a t e s
[dictionary? (-> any/c boolean?)]
; b a s i c q u e r i e s
; h o w m a n y i t e m s a r e i n t h e d i c t i o n a r y?
[count (-> dictionary? natural-number/c)]
; d o e s t h e d i c t i o n a r y d e f i n e k e y k?
[has? (->d ([d dictionary?][k symbol?])
()
[result boolean?]
#:post-cond
((zero? (count d)) . ⇒ . (not result)))]
; w h a t i s t h e v a l u e o f k e y k i n t h i s d i c t i o n a r y?
[value-for (->d ([d dictionary?]
[k (and/c symbol? (lambda (k) (has? d k)))])
()
[result (dictionary-value? d)])]
; i n i t i a l i z a t i o n
; p o s t c o n d i t i o n: f o r a l l k i n s y m b o l, (h a s? d k) i s f a l s e.
[initialize (->d ([p contract?][eq (p p . -> . boolean?)])
()
[result (and/c dictionary? (compose zero? count))])]
; c o m m a n d s
; M i t c h e l l a n d M c K i m s a y t h a t p u t s h o u l d n't c o n s u m e V o i d (n u l l p t r)
; f o r v. W e a l l o w t h e c l i e n t t o s p e c i f y a c o n t r a c t f o r a l l v a l u e s
; v i a i n i t i a l i z e. W e c o u l d d o t h e s a m e v i a a k e y? p a r a m e t e r
; (e x e r c i s e). a d d k e y k w i t h v a l u e v t o t h i s d i c t i o n a r y
[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)))]
; r e m o v e k e y k f r o m t h i s d i c t i o n a r y
[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)))])
; e n d o f i n t e r f a c e

The tests:

#lang scheme
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2))
"3.ss")
(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))))

##### 7.5.4`` A Queue

#lang scheme
; N o t e: t h i s q u e u e d o e s n't i m p l e m e n t t h e c a p a c i t y r e s t r i c t i o n
; o f M c K i m a n d M i t c h e l l's q u e u e b u t t h i s i s e a s y t o a d d.
; a c o n t r a c t u t i l i t y
(define (all-but-last l) (reverse (cdr (reverse l))))
(define (eq/c x) (lambda (y) (eq? x y)))
; i m p l e m e n t a t i o n
(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 (rem s)
(make-queue (cdr (queue-list s))
(queue-p? s)
(queue-eq s)))
(define (head s) (car (queue-list s)))
; i n t e r f a c e
(provide/contract
; p r e d i c a t e
[queue? (-> any/c boolean?)]
; p r i m i t i v e q u e r i e s
; I m a g i n e p r o v i d i n g t h i s 'q u e r y' f o r t h e i n t e r f a c e o f t h e m o d u l e
; o n l y. T h e n i n S c h e m e, t h e r e i s n o r e a s o n t o h a v e c o u n t o r i s-e m p t y?
; a r o u n d (o t h e r t h a n p r o v i d i n g i t t o c l i e n t s). A f t e r a l l i t e m s i s
; e x a c t l y a s c h e a p a s c o u n t.
[items (->d ([q queue?]) () [result (listof (queue-p? q))])]
; d e r i v e d q u e r i e s
[count (->d ([q queue?])
; W e c o u l d e x p r e s s t h i s s e c o n d p a r t o f t h e p o s t
; c o n d i t i o n e v e n i f c o u n t w e r e a m o d u l e "a t t r i b u t e"
; i n t h e l a n g u a g e o f E i f f e l; i n d e e d i t w o u l d u s e t h e
; e x a c t s a m e s y n t a x (m i n u s t h e a r r o w a n d d o m a i n).
()
[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))))])]
; c r e a t i o n
[initialize (-> contract?
(contract? contract? . -> . boolean?)
(and/c queue? (compose null? items)))]
; c o m m a n d s
[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)))))])]
[rem (->d ([oldq (and/c queue? (compose not is-empty?))])
()
[result
(and/c queue?
(lambda (q)
(equal? (cdr (items oldq)) (items q))))])])
; e n d o f i n t e r f a c e

The tests:

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

top← prev up next →