REBOL [
Title: "Design By Contract"
Date: 29-Oct-2002
Name: DBC
Version: 1.0.4
File: %dbc.r
Author: "Jan Skibinski"
Purpose: "Provides support for DBC and some simple examples"
Email: jan.skibinski@sympatico.ca
Category: [util tutor 3]
Acknowledgments: {
Function 'nargs is due to Carl Sassenrath.
Functions 'map and 'filter are due Ladislav Mecir,
script %highfun.r.
}
]
comment {
Basic little framework for Design By Contract. It is made of
the constructors 'contract and 'contr, the wrapper 'wrap-dbc and
additional three logical functions for testing the assertions:
'require, 'ensure and 'implies.
User functions constructed with the help of 'contract,
rather than 'func or 'function, will be provided with
runtime assertion testing mechanism, as in:
g: contract spec locals pre body post
where spec, locals, pre, body and post are blocks.
Blocks of preconditions and postconditions are formed
from the series of block conditions.
A shorter variety of 'contract is a 'contr function, which
assumes that local words are already defined within the spec:
g: contr spec pre body post
Alternatively, one may prefer using the 'wrap-dbc' function,
which wraps a pre-post contract around any existing regular
function 'f, as in:
g: wrap-dbc pre :f post.
Also provided is a new help utility, function help', which
is an extension of the standard help. It prints not only
the standard info but also blocks of pre- and postconditions
- if they are defined. You can run the help' on any word
- regardless whether the word represents the "contracted"
function or not.
Several simple examples are attached at the bottom of the page.
One of the examples shows how to bypass the "contract" fuction
and to code the assertions directly in the body of a function.
All four approaches: via 'contr, 'contract, 'wrap-dbc and manual
construction seem to be equally easy to use.
Suggested tests: execute examples with good and forbidden
inputs to test the preconditions, recompile postconditions
to something ridiculously incorrect and watch how they
kick in, check how the sources of examples look like
and play with the help and help' functions.
Related: %contract.r by Maarten Koopmans
}
Comment {
Auxiliary functions
}
integral?: func [
"True if a decimal 'x' is an integral."
x [decimal! integer!] /local result [logic!]
][
result: either decimal? x [x = to-decimal to-integer x][true]
result
]
block-of-blocks?: func [
{True if block 'b is either empty or is made of blocks,
presumably assertion blocks. This is to remind the user
that each assertion should be enclosed in a block.}
b [block!] /local result [logic!]
][
result: all map (func [x][block? x]) b
result
]
map: function [
{Maps a function to all elements of a block
Precise signature should be:
map :: (a -> b) -> [a] -> [b]
}
[throw]
f [any-function!] {:: a -> b}
blk [block!] {:: [a]}
][
result [block!] {:: [b]}
][
result: make block! length? blk
foreach elem blk [
insert/only tail result f :elem
]
result
]
filter: func [
{Filter a 'series using a 'selector function.
Precise signature should be
filter :: (a -> logic) -> [a] -> [a]
}
[throw]
selector [any-function!] {:: a -> logic}
series [series!] {:: [a]}
/local result [series!]
][
result: make :series length? :series
foreach element :series [
if selector :element [
insert/only tail result :element
]
]
result
]
nargs: func [
{Number of the function arguments}
f [any-function!]
][
-1 + index? any [find first :f refinement! tail first :f]
]
comment {
Basic functions
}
contr: func [
"Defines a user function with assertions."
fun-spec [block!] "Arguments and their types and local words"
pre [block!] "Preconditions"
fun-body [block!] "Function body"
post [block!] "Postconditions"
/local spec body result [function!]
][
require [
[block-of-blocks? pre]
[block-of-blocks? post]
]
spec: modify-spec copy fun-spec
body: make-body pre fun-body post
result: make function! spec body
:result
]
contract: func [
"Defines a user function with assertions and local words."
fun-spec [block!] "Arguments and their types"
vars [block!] "Local words"
pre [block!] "Preconditions"
fun-body [block!] "Function body"
post [block!] "Postconditions"
/local spec body result [function!]
][
require [
[block-of-blocks? pre]
[block-of-blocks? post]
]
spec: modify-spec head insert insert tail copy fun-spec /local vars
body: make-body pre fun-body post
result: make function! spec body
:result
]
wrap-dbc: func [
"Wrap preconditions and postcondition around an existing function."
pre [block!] "Preconditions"
fun [function!] "Function to be wrapped"
post [block!] "Postconditions"
/local spec body result [function!]
][
require [
[block-of-blocks? pre]
[block-of-blocks? post]
]
spec: modify-spec load mold third :fun
body: make-body pre (copy second :fun) post
result: make function! spec body
:result
]
make-body: func [
"Make contract body from a copy of a function body and assertions"
pre [block!]
fun-body [block!]
post [block!]
][
compose/deep [
require
[(pre)]
result: do
[(fun-body)]
ensure
[(post)]
result
]
]
modify-spec: func [
"Modify function spec to match dbc requirement"
spec [block!]
][
either empty? spec [
spec: [[catch] /local result]
][
either string? spec/1 [
insert/only next spec [catch]
][
insert/only spec [catch]
]
if not find spec 'result [
either find spec /local [
replace spec /local [/local result]
][
append spec [/local result]
]
]
]
spec: head spec
]
contract?: func [
{True if a function has embedded contract.}
fun [function!] "Function"
/local result [logic!]
][
result: either (find (second :fun) 'require) [true][false]
]
require: func [
{Throws an error if any 'precondition' is violated,
otherwise returns 'true'. Used for preconditions validation.}
[throw]
preconditions [block!]
/local result [logic!]
][
foreach p preconditions [
if not (do p) [
throw make error! (join "Violated precondition " (mold p))
]
]
result: true
result
]
ensure: func [
{Throws an error if any 'postcondition' is violated,
otherwise returns 'true'. Used for postconditions validation.}
[throw]
postconditions [block!]
/local result [logic!]
][
foreach p postconditions [
if not (do p) [
throw make error! (join "Violated postcondition " (mold p))
]
]
result: true
result
]
implies: func [
{True if condition c1 is false, or if c1 and c2 are both true.
Used to encode this logic: "if c1 is true then c2 must also be true"}
c1 [logic!]
c2 [logic!]
/local result [logic!]
][
result: (c1 and c2) or not c1
result
]
comment {
Aside from the runtime validation of the contracts the
Design By Contract technique should benefit users
with improved way of producing documentation. As any
user of Eiffel knows, the assertions can and should be
parts of a program specification, or API if you will.
But Eiffel provides a language support for DBC,
while other languages offer only some add hoc and often
ugly solutions. For example many Java implementations
of DBC are based on comment preprocessing, and quite
a few rely on javadoc special comment tags, etc.
So how does the Rebol score on this point? I think
it does quite well, as this little patch of the standard
function "help" demonstrates.
}
help': func [
{Extended help providing standard help plus
assertions if they are available.}
'word [any-type!]
/local assertions names
][
help :word
if not value? word [exit]
if not function? (get word) [exit]
names: [[require PRECONDITIONS] [ensure POSTCONDITIONS]]
foreach pair names [
assertions: find second (get word) (first pair)
if assertions [
print join "^/" [second pair ":"]
foreach p second assertions [print join "^-" mold p]
]
]
exit
]
comment {
Here are few examples of using DBC in Rebol.
Some of them insist on using the strongly typed arithmetic
and do not allow for silent conversions from integers
to decimals.
This does not mean that I do not like working with mixed
type arithmetics. I was just in the "typeful" mood
when working on the examples to illustrate the
Design By Contract concept and implementation.
Method 1: Using the 'contr and 'contract constructors
}
simple: contr [
"Simple example of a useless function with assertions."
x [integer!] /local a result [integer!]
][ ;Require:
[x >= 2]
[x <= 10]
][ ;Body
a: 8
a * x
][ ;Ensure:
[result >= 16]
[result <= 80]
]
factorial: contract [
{Factorial of a number 'x' computed
recursively without a help of an accumulator.
Example of a function with assertions.}
x [number!]
][ ;Local words
fac result [number!]
][ ;Require
[x >= 0]
[implies (integer? x) (x <= 12) ]
[implies (decimal? x) (x <= 170)]
[implies (decimal? x) (integral? x)]
][ ;Body
fac: func [n] [
either n = 0 [1] [n * fac (n - 1)]
]
fac x
][ ;Ensure
[result >= 1]
[result <= max-factorial]
[(type? x) == (type? result)]
]
comment {
Method 2: Using the 'wrap-dbc wrapper
}
accum-factorial: func [
{Factorial of a number 'x' computed recursively
with a help of an accumulator.}
x [number!] /local accum result [number!]
][
accum: func [a n] [
either n = 0 [a][accum (n * a) (n - 1)]
]
either decimal? x [accum 1.0 x][accum 1 x]
]
factorial': wrap-dbc
[
[x >= 0]
[implies (integer? x) (x <= 12) ]
[implies (decimal? x) (x <= 170)]
[implies (decimal? x) (integral? x)]
]
:accum-factorial
[
[result >= 1]
[result <= max-factorial]
[(type? x) == (type? result)]
]
Comment {
Method 3: Inserting assertions manually
}
binomial: func [
{Binomial n k.}
[catch]
n [number!]
k [number!]
/local result [number!] f
][ ;Body
require [
[n >= 0]
[k >= 0]
[k <= n]
[implies (integer? n) (n <= 12) ]
[implies (decimal? n) (n <= 170)]
[(type? n) == (type? k)]
[implies (decimal? n) (integral? n)]
[implies (decimal? k) (integral? k)]
]
f: func [s r] [
either s = r [1][s * f (s - 1) r]
]
result: either (n - k > k) [
(f n (n - k)) / accum-factorial k
][
(f n k) / accum-factorial (n - k)
]
ensure [
[result >= 1]
[result <= max-factorial]
[(type? n) == (type? result)]
]
return result
]
max-factorial: 7.25741561530799E+306
; The maximum computable output value of a factorial x,
; where x = 170.0}
"DBC loaded OK!"