<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html;charset=ISO-8859-1">
<title></title>
</head>
<body text="#000000" bgcolor="#ffffff">
Robert Will wrote:<br>
<blockquote type="cite"
cite="midPine.SGI.4.51.0402171038430.900042@tissot.rz.tu-ilmenau.de">4.
A notation for preconditions. For simple functions a Precondition<br>
<pre wrap=""> can be calculated automatically from the Patterns:
</pre>
<blockquote type="cite">
<pre wrap=""> head (x:xs) = x
</pre>
</blockquote>
<pre wrap=""><!---->
Gives the Precondition @xs /= []@ for @head xs@. This only needs
some simple knowledge about @data@ and @newtype@ declarations. (We
could also choose to leave it out, if it's too much work, for too
few cases where it works. Then programmers would have to state all
preconditions explicitly as shown next.)
Presently I use the following coding style:
</pre>
<blockquote type="cite">
<pre wrap=""> take n xs | not (n >= 9) = error "take.Precondition"
</pre>
</blockquote>
<pre wrap=""><!---->
The precondition can simply be extracted as <<the bracketed
expression behind @not@ in a line containing the words @error@ and
"Precondition">>.
However it has the disadvantage that I can't simply disable
run-time checking of the Precondition (as I could when using
@assert@). Furthermore it is also rather ugly. Does anyone have a
better idea?</pre>
</blockquote>
The most lightweight way to specify preconditions would be via another
function definition with the same parameters and a systematically
chosen name, for example<br>
<br>
take_pre n xs = n>=0<br>
<br>
thus making it easy to generate the QuickCheck property<br>
<br>
prop_take n xs = take_pre n xs ==> take_spec n xs == take n xs<br>
<br>
There are some problems in generating such properties automatically,
though:<br>
<br>
- QuickCheck properties have to be tested at a particular
(mono-)type. It isn't obvious how to specify at which type such a
polymorphic property should be tested.<br>
<br>
- Simple preconditions (such as n>=0) work well in tested
properties. More complex ones (such as ordered xs) need to be replaced
by a custom test data generator for testing to be both efficient and
effective. Again, it's hard to see how to insert these automatically.<br>
<br>
Perhaps it's simpler just to write QuickCheck properties explicitly?<br>
<blockquote type="cite"
cite="midPine.SGI.4.51.0402171038430.900042@tissot.rz.tu-ilmenau.de">6.
Invariants are an important part of Design by Contract according to<br>
<pre wrap=""> [3].
In Functional Programming it has been proven practical to check
(and at the same time: document) data structure invariants in a
smart constructor; the invariant resides only in this place (is
not redundantly mentioned in the code) and is run-time checked on
each creation of a data cell. This works with @assert@ and doesn't
need QuickCheck properties. Also, such internal invariants are not
relevant for the external documentation. (Otherwise we could
documentation- export the definition of the smart constructor,
using -- ||.)
External Invariants are nothing else than algebraic properties of
data structures. They can be documented using normal QuickCheck-
Properties, and these can be documentation- exported via -- ||.
As a consequence, invariants need no special notation. I only
mention them her for methodological reasons.
</pre>
</blockquote>
In our experience it's important to state properties that invariants
are preserved by functions -- for example,<br>
<br>
ordered xs ==> ordered (insert x xs)<br>
<br>
or rather<br>
<br>
forAll orderedList $ \xs -> ordered (insert x xs)<br>
<br>
But I agree, no special notation is needed.<br>
<br>
John<br>
</body>
</html>