Matthias's improvements to the contracts docs, plus a few minor fixes
svn: r8478
This commit is contained in:
parent
b012e7dbe7
commit
9bdbfba888
|
@ -15,10 +15,9 @@
|
|||
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):
|
||||
observers. While we reformulate Mitchell and McKim's terminology and
|
||||
we use a mostly applicative, we
|
||||
retain their terminology of "classes" and "objects":
|
||||
|
||||
@itemize{
|
||||
@item{@bold{Separate queries from commands.}
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
#lang mzscheme
|
||||
#lang scheme
|
||||
(require (planet "test.ss" ("schematics" "schemeunit.plt" 2))
|
||||
(planet "text-ui.ss" ("schematics" "schemeunit.plt" 2)))
|
||||
(require "1.ss" "1b.ss")
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
#lang scheme
|
||||
|
||||
;; a contract utility
|
||||
;; a shorthand for use below
|
||||
(define-syntax ⇒
|
||||
(syntax-rules ()
|
||||
[(⇒ antecedent consequent) (if antecedent consequent #t)]))
|
||||
|
|
|
@ -26,14 +26,14 @@ scheme
|
|||
]
|
||||
|
||||
Several clients used your module. Others used their
|
||||
modules. And all of a sudden one of them sees this error
|
||||
modules in turn. And all of a sudden one of them sees this error
|
||||
message:
|
||||
|
||||
@inset-flow{@schemeerror{bank-client broke the contract (-> ??? any)
|
||||
it had with myaccount on deposit; expected <???>, given: -10}}
|
||||
|
||||
Clearly, @scheme[bank-client] is a module that uses @scheme[myaccount]
|
||||
but what are the @schemeerror{?}s doing there? Wouldn't it be nice if
|
||||
but what is the @schemeerror{???} doing there? Wouldn't it be nice if
|
||||
we had a name for this class of data much like we have string, number,
|
||||
and so on?
|
||||
|
||||
|
@ -62,7 +62,7 @@ With this little change, the error message becomes all of the
|
|||
sudden quite readable:
|
||||
|
||||
@inset-flow{@schemeerror{bank-client broke the contract (-> amount
|
||||
any) it had with myaccount on deposit; expected <amount>, given: -10"}}
|
||||
any) it had with myaccount on deposit; expected <amount>, given: -10}}
|
||||
|
||||
@ctc-section[#:tag "optional"]{Optional arguments}
|
||||
|
||||
|
@ -88,16 +88,18 @@ scheme
|
|||
(build-string rmargin (λ (x) pad))))
|
||||
]
|
||||
|
||||
The module exports @scheme[string-pad-center], a function that creates a
|
||||
string of a given @scheme[width] with the given string in the center. The
|
||||
default fill character is @scheme[#\space]; if the client module requires
|
||||
different character, it may call @scheme[string-pad-center] with a third
|
||||
argument, a @scheme[char], overwriting the default.
|
||||
The module exports @scheme[string-pad-center], a function
|
||||
that creates a string of a given @scheme[width] with the
|
||||
given string in the center. The default fill character is
|
||||
@scheme[#\space]; if the client module wishes to use a
|
||||
different character, it may call @scheme[string-pad-center]
|
||||
with a third argument, a @scheme[char], overwriting the
|
||||
default.
|
||||
|
||||
The function definition uses optional arguments of
|
||||
@scheme[lambda], which is appropriate for this kind of
|
||||
functionality. The interesting point here is the formulation
|
||||
of the contract for the @scheme[string-pad-center].
|
||||
The function definition uses optional arguments, which is
|
||||
appropriate for this kind of functionality. The interesting
|
||||
point here is the formulation of the contract for the
|
||||
@scheme[string-pad-center].
|
||||
|
||||
|
||||
The contract combinator @scheme[->*], demands several groups of contracts:
|
||||
|
@ -111,19 +113,12 @@ arguments: @scheme[char?]. }
|
|||
|
||||
@item{The last one is a single contract: the result of the function.}
|
||||
}
|
||||
Note if a default value does not satisfy a contract, you won't get a contract
|
||||
error for this interface. We do trust you; if you can't trust
|
||||
yourself, you need to communicate across boundaries for everything you write.
|
||||
|
||||
The contract library does not have built-in combinators to
|
||||
specify richer contracts for functions that have optional
|
||||
arguments, like functions that have optional arguments where
|
||||
the arguments depend on each other.
|
||||
|
||||
To specify such contracts combine @scheme[case->] with
|
||||
the other function contract combinators, like we did in
|
||||
the @scheme[substring1] function above.
|
||||
|
||||
Note if a default value does not satisfy a contract, you
|
||||
won't get a contract error for this interface. In contrast
|
||||
to type systems, we do trust you; if you can't trust
|
||||
yourself, you need to communicate across boundaries for
|
||||
everything you write.
|
||||
|
||||
@ctc-section[#:tag "rest-args"]{Rest arguments}
|
||||
|
||||
|
@ -165,11 +160,6 @@ rest argument follows @scheme[#:rest]
|
|||
contract demands a list of values; in this specific
|
||||
examples, these values must be number.
|
||||
|
||||
Finally, you may have noticed that the contract for the function range
|
||||
of @scheme[plus] is also wrapped in a pair of parentheses. The reason
|
||||
for those is that functions can return multiple values not just one, and
|
||||
this is our next topic in this guide.
|
||||
|
||||
@ctc-section[#:tag "keywords"]{Keyword arguments}
|
||||
|
||||
Sometimes, a function accepts many arguments and remembering
|
||||
|
@ -182,25 +172,22 @@ GUI and asks the user a yes-or-no question:
|
|||
scheme/gui
|
||||
|
||||
(define (ask-yes-or-no-question #:question question
|
||||
#:default def
|
||||
#:default answer
|
||||
#:title title
|
||||
#:width w
|
||||
#:height h)
|
||||
(define d (new dialog% [label title] [width w] [height h]))
|
||||
(define answer def)
|
||||
(define msg (new message% [label question] [parent d]))
|
||||
(define (yes) (set! answer #t) (send d show #f))
|
||||
(define (no) (set! answer #f) (send d show #f))
|
||||
(define yes-b (new button%
|
||||
[label "Yes"]
|
||||
[parent d]
|
||||
[label "Yes"] [parent d]
|
||||
[callback (λ (x y) (yes))]
|
||||
[style (if def '(border) '())]))
|
||||
[style (if answer '(border) '())]))
|
||||
(define no-b (new button%
|
||||
[label "No"]
|
||||
[parent d]
|
||||
[label "No"] [parent d]
|
||||
[callback (λ (x y) (no))]
|
||||
[style (if def '() '(border))]))
|
||||
[style (if answer '() '(border))]))
|
||||
(send d show #t)
|
||||
answer)
|
||||
|
||||
|
@ -241,7 +228,7 @@ Of course, many of the parameters in
|
|||
have reasonable defaults, and should be made optional:
|
||||
@schemeblock[
|
||||
(define (ask-yes-or-no-question #:question question
|
||||
#:default def
|
||||
#:default answer
|
||||
#:title [title "Yes or No?"]
|
||||
#:width [w 400]
|
||||
#:height [h 200])
|
||||
|
@ -285,7 +272,7 @@ scheme
|
|||
]
|
||||
|
||||
The contract for the exported function @scheme[sqrt.v1] uses the
|
||||
@scheme[->d] rather than @scheme[->] function contract. The "d"
|
||||
@scheme[->d] rather than @scheme[->] function contract. The ``d''
|
||||
stands for @italic{dependent} contract, meaning the contract for the
|
||||
function range depends on the value of the argument.
|
||||
|
||||
|
@ -312,8 +299,8 @@ money but only as much as they have in the account.
|
|||
|
||||
Suppose the account module provides the following two functions:
|
||||
@schemeblock[
|
||||
(code:comment "balance : account -> amount")
|
||||
(code:comment "withdraw : account amount -> account")
|
||||
balance : (-> account amount)
|
||||
withdraw : (-> account amount account)
|
||||
]
|
||||
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.''
|
||||
|
@ -330,7 +317,7 @@ conditions we just discussed:
|
|||
@schememod[
|
||||
scheme
|
||||
|
||||
(code:comment "the contract definitions")
|
||||
(code:comment "section 1: the contract definitions")
|
||||
(define-struct account (balance))
|
||||
(define amount natural-number/c)
|
||||
|
||||
|
@ -343,7 +330,7 @@ scheme
|
|||
(and (account? a) (op balance0 (balance a))))
|
||||
(flat-named-contract (format msg balance0) ctr))
|
||||
|
||||
(code:comment "the exports")
|
||||
(code:comment "section 2: the exports")
|
||||
(provide/contract
|
||||
[create (amount . -> . account?)]
|
||||
[balance (account? . -> . amount)]
|
||||
|
@ -356,7 +343,7 @@ scheme
|
|||
()
|
||||
[result (mk-account-contract acc amt < msg<)])])
|
||||
|
||||
(code:comment "the function definitions")
|
||||
(code:comment "section 3: the function definitions")
|
||||
(define balance account-balance)
|
||||
|
||||
(define (create amt) (make-account amt))
|
||||
|
@ -533,7 +520,7 @@ Now suppose we also want to ensure that the first result of
|
|||
(values [s (substring-of (list->string fl))]
|
||||
[c (listof char?)]))])
|
||||
]
|
||||
Like @scheme[->*], the new combinator uses a function over the
|
||||
Like @scheme[->*], the @scheme[->d] combinator uses a function over the
|
||||
argument to create the range contracts. Yes, it doesn't just return one
|
||||
contract but as many as the function produces values: one contract per
|
||||
value. In this case, the second contract is the same as before, ensuring
|
||||
|
@ -594,7 +581,7 @@ Here are two uses:
|
|||
|
||||
A contract for @scheme[n-step] must specify two aspects of
|
||||
@scheme[proc]'s behavior: its arity must include the number of elements
|
||||
in @scheme[inits], and it must return either a number of
|
||||
in @scheme[inits], and it must return either a number or
|
||||
@scheme[#f]. The latter is easy, the former is difficult. At first
|
||||
glance, this appears to suggest a contract that assigns a
|
||||
@italic{variable-arity} to @scheme[proc]:
|
||||
|
|
|
@ -11,8 +11,8 @@
|
|||
|
||||
The contract library assumes that variables exported via
|
||||
@scheme[provide/contract] are not assigned to, but does not enforce
|
||||
it. Accordingly, if you try to @scheme[set!] those variables, you may
|
||||
find unexpected behavior. Consider the following example:
|
||||
it. Accordingly, if you try to @scheme[set!] those variables, you
|
||||
may be surprised. Consider the following example:
|
||||
|
||||
@interaction[
|
||||
(module server scheme
|
||||
|
|
|
@ -9,7 +9,8 @@
|
|||
|
||||
Like a contract between two business partners, a software
|
||||
contract is an agreement between two parties. The agreement
|
||||
specifies obligations and guarantees for each party.
|
||||
specifies obligations and guarantees for each ``product''
|
||||
(or value) that is handed from one party to the other.
|
||||
|
||||
A contract thus establishes a boundary between the two parties. Whenever a
|
||||
value crosses this boundary, the contract monitoring system performs contract
|
||||
|
@ -27,10 +28,11 @@ scheme
|
|||
(define amount ...)
|
||||
]
|
||||
|
||||
promises to all clients of @scheme[a] that amount will always be a
|
||||
positive number. The contract system monitors @scheme[a]'s obligation
|
||||
carefully. Every time a client refers to @scheme[amount], the monitor checks
|
||||
that the value of @scheme[amount] is indeed a positive number.
|
||||
promises to all clients of the above module that amount will
|
||||
always be a positive number. The contract system monitors
|
||||
@scheme[a]'s obligation carefully. Every time a client
|
||||
refers to @scheme[amount], the monitor checks that the value
|
||||
of @scheme[amount] is indeed a positive number.
|
||||
|
||||
The contracts library is built into the Scheme language, but
|
||||
if you wish to use @scheme[scheme/base], you can explicitly
|
||||
|
@ -57,10 +59,10 @@ scheme
|
|||
(define amount 0)]
|
||||
|
||||
When module @scheme[a] is required, the monitoring
|
||||
system will signal a violation of the contract and
|
||||
system signals a violation of the contract and
|
||||
blame @scheme[a] for breaking its promises.
|
||||
|
||||
@ctc-section[#:tag "qamount"]{A more subtle contract violation}
|
||||
@ctc-section[#:tag "qamount"]{A subtle contract violation}
|
||||
|
||||
Suppose the creator of @scheme[a] had written
|
||||
@schememod[
|
||||
|
@ -72,11 +74,12 @@ scheme
|
|||
(define amount 'amount)
|
||||
]
|
||||
|
||||
In that case, @scheme[positive?] will report an error, since
|
||||
its domain is only numbers. To make the contract capture our
|
||||
intentions for all Scheme values, we can ensure that the
|
||||
value is both a number and is positive, using an
|
||||
@scheme[and/c] contract:
|
||||
In that case, the monitoring system applies
|
||||
@scheme[positive?] to a symbol, but @scheme[positive?]
|
||||
reports an error, because its domain is only numbers. To
|
||||
make the contract capture our intentions for all Scheme
|
||||
values, we can ensure that the value is both a number and is
|
||||
positive, combining the two contracts with @scheme[and/c]:
|
||||
|
||||
@schemeblock[
|
||||
(provide/contract
|
||||
|
|
|
@ -13,7 +13,7 @@ module that imports the function. If the client module calls
|
|||
the function, it sends a value into the ``server''
|
||||
module. Conversely, if such a function call ends and the
|
||||
function returns a value, the ``server'' module sends a
|
||||
value back to the "client" module.
|
||||
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.
|
||||
|
@ -45,16 +45,17 @@ arguments, a string and a number, and it promises nothing about the return value
|
|||
@item{@scheme[deposit]: The function's contract demands from the client modules
|
||||
that they apply it to numbers. It promises nothing about the return value. }}
|
||||
|
||||
If a "client" module that were to apply @scheme[deposit] to
|
||||
@scheme['silly], it would violate the contract. The contract monitoring
|
||||
system would flag this violation and blame "client" for breaking the contract
|
||||
with @scheme[myaccount].
|
||||
If a ``client'' module were to apply @scheme[deposit] to
|
||||
@scheme['silly], it would violate the contract. The
|
||||
contract monitoring system would catch this violation and
|
||||
blame ``client'' for breaking the contract with the above
|
||||
module.
|
||||
|
||||
@bold{Note:} Instead of @scheme[any] you could also use the
|
||||
more specific contract @scheme[void?], which says that the function will
|
||||
always return the @scheme[(void)] value. This contract, however, would require
|
||||
the contract monitoring system to check the return value every time the function
|
||||
is called, even though the "client" module can't do much with this value
|
||||
is called, even though the ``client'' module can't do much with this value
|
||||
anyway. In contrast, @scheme[any] tells the monitoring system @italic{not}
|
||||
to check the return value. Additionally, it tells a potential client that the
|
||||
``server'' module @italic{makes no promises at all} about the function's return
|
||||
|
@ -79,10 +80,10 @@ reader what the name represents (a function) and, if it is a function (or
|
|||
some other complex value) what the pieces are supposed to be. This is why
|
||||
we use a @scheme[->] to say "hey, expect this to be a function."
|
||||
|
||||
So @scheme[->] says "this is contract for a function." What follows
|
||||
So @scheme[->] says ``this is a contract for a function.'' What follows
|
||||
in a function contracts are contracts (sub-contracts if you wish) that tell
|
||||
the reader what kind of arguments to expect and what kind of a result the
|
||||
function will produce. For example,
|
||||
function produces. For example,
|
||||
@schemeblock[
|
||||
(provide/contract
|
||||
[create (-> string? number? boolean? account?)])
|
||||
|
@ -228,9 +229,7 @@ scheme
|
|||
|
||||
(code:comment "convert an amount into a dollar based string")
|
||||
[format-nat (-> natural-number/c
|
||||
(lambda (result)
|
||||
(and (string? result)
|
||||
(has-decimal? string))))])
|
||||
(and/c string? has-decimal?))])
|
||||
]
|
||||
The contract of the exported function @scheme[format-number] specifies that
|
||||
the function consumes a number and produces a string.
|
||||
|
@ -286,8 +285,8 @@ scheme
|
|||
The contract @scheme[any/c] accepts any value, and
|
||||
@scheme[any] is a keyword that can appear in the range of
|
||||
the function contracts (@scheme[->], @scheme[->*], and
|
||||
@scheme[->d]), so it is natural to wonder what is the
|
||||
difference between these two contracts:
|
||||
@scheme[->d]), so it is natural to wonder what the
|
||||
difference between these two contracts is:
|
||||
@schemeblock[
|
||||
(-> integer? any)
|
||||
(-> integer? any/c)
|
||||
|
@ -306,8 +305,8 @@ example, this function:
|
|||
meets the first contract, but not the second one.}
|
||||
|
||||
@item{Relatedly, this means that a call to a function that
|
||||
has the first contract is not a tail call. So, for example,
|
||||
this program is an infinite loop that takes only a constant
|
||||
has the second contract is not a tail call. So, for example,
|
||||
the following program is an infinite loop that takes only a constant
|
||||
amount of space, but if you replace @scheme[any] with
|
||||
@scheme[any/c], it uses up all of the memory available.
|
||||
|
||||
|
|
|
@ -67,12 +67,12 @@ or promises that the two fields of a @scheme[posn] structure are
|
|||
numbers---when the values flow across the module boundary.
|
||||
|
||||
Thus, if a client calls @scheme[make-posn] on @scheme[10] and
|
||||
@scheme['a], the contract system will signal a contract
|
||||
@scheme['a], the contract system signals a contract
|
||||
violation.
|
||||
|
||||
The creation of @scheme[p-sick] inside of the @scheme[posn] module,
|
||||
however, does not violate the contracts. The function @scheme[make-posn] is
|
||||
internal so @scheme['a] and @scheme['b] don't cross the module
|
||||
used internally so @scheme['a] and @scheme['b] don't cross the module
|
||||
boundary. Similarly, when @scheme[p-sick] crosses the boundary of
|
||||
@scheme[posn], the contract promises a @scheme[posn?] and nothing
|
||||
else. In particular, this check does @italic{not} require that the fields of
|
||||
|
@ -89,10 +89,10 @@ scheme
|
|||
... (posn-x p-sick) ...
|
||||
]
|
||||
|
||||
Using @scheme[posn-x] is the only way @scheme[client] can find out what
|
||||
Using @scheme[posn-x] is the only way the client can find out what
|
||||
a @scheme[posn] contains in the @scheme[x] field. The application of
|
||||
@scheme[posn-x] sends @scheme[p-sick] back into the
|
||||
@scheme[posn]module and the result value -- @scheme['a] here -- back to
|
||||
@scheme[posn] module and the result value -- @scheme['a] here -- back to
|
||||
the client, again across the module boundary. At this very point, the contract
|
||||
system discovers that a promise is broken. Specifically, @scheme[posn-x]
|
||||
doesn't return a number but a symbol and is therefore blamed.
|
||||
|
@ -102,7 +102,7 @@ doesn't always pinpoint the source of the error. The good news is that the
|
|||
error is located in the @scheme[posn] module. The bad news is that the
|
||||
explanation is misleading. Although it is true that @scheme[posn-x]
|
||||
produced a symbol instead of a number, it is the fault of the programmer who
|
||||
reated a @scheme[posn] from symbols, i.e., the programmer who added
|
||||
created a @scheme[posn] from symbols, i.e., the programmer who added
|
||||
|
||||
@schemeblock[
|
||||
(define p-sick (make-posn 'a 'b))
|
||||
|
@ -144,9 +144,8 @@ subtree are smaller than the number in the node, and all of
|
|||
the numbers in the right subtree are larger than the number
|
||||
in the node.
|
||||
|
||||
We can implement implement a search
|
||||
function @scheme[in?] that takes advantage of the
|
||||
structure of the binary search tree.
|
||||
We can implement a search function @scheme[in?] that takes
|
||||
advantage of the structure of the binary search tree.
|
||||
@schememod[
|
||||
scheme
|
||||
|
||||
|
@ -201,7 +200,7 @@ checking the binary search tree contract. In particular, if
|
|||
we only checked the contract on the nodes
|
||||
that @scheme[in?] looks at, we can still guarantee that
|
||||
the tree is at least partially well-formed, but without
|
||||
the performance loss.
|
||||
changing the complexity.
|
||||
|
||||
To do that, we need to
|
||||
use @scheme[define-contract-struct] in place
|
||||
|
@ -211,8 +210,8 @@ predicate, and selectors for a new
|
|||
structure. Unlike @scheme[define-struct], it also
|
||||
defines contract combinators, in this
|
||||
case @scheme[node/c] and @scheme[node/dc]. Also unlike
|
||||
@scheme[define-struct], it does not define mutators, making
|
||||
its structs immutable.
|
||||
@scheme[define-struct], it does not allow mutators, making
|
||||
its structs always immutable.
|
||||
|
||||
The @scheme[node/c] function accepts a contract for each
|
||||
field of the struct and returns a contract on the
|
||||
|
|
|
@ -3,7 +3,11 @@
|
|||
@require[scribble/eval]
|
||||
@require["guide-utils.ss"]
|
||||
|
||||
@title[#:tag "contracts" #:style 'toc]{Contracts}
|
||||
@title[#:tag "Contracts" #:style 'toc]{Contracts}
|
||||
|
||||
This chapter provides a gentle introduction to PLT Scheme's
|
||||
contract system. For the complete details see the
|
||||
@refsecref["Contracts"] section in the reference manual.
|
||||
|
||||
@local-table-of-contents[]
|
||||
|
||||
|
@ -30,6 +34,7 @@ update string-pad-center to show examples via REPL notation:
|
|||
|
||||
}
|
||||
|
||||
|
||||
@include-section["contracts-intro.scrbl"]
|
||||
@include-section["contracts-simple-function.scrbl"]
|
||||
@include-section["contracts-general-function.scrbl"]
|
||||
|
|
|
@ -1,7 +1,12 @@
|
|||
#lang scribble/doc
|
||||
@require["mz.ss"]
|
||||
|
||||
@title[#:tag "mzlib:contract" #:style 'toc]{Contracts}
|
||||
@title[#:tag "Contracts" #:style 'toc]{Contracts}
|
||||
|
||||
This chapter is long on detail and short on the motivation
|
||||
and pragmatics of using contracts. See
|
||||
@guidesecref["Contracts"] in the Guide for more of the
|
||||
latter and less of the former.
|
||||
|
||||
A @defterm{contract} controls the flow of values to ensure that the
|
||||
expectations of one party are met by another party. The
|
||||
|
|
Loading…
Reference in New Issue
Block a user