[Haskell] Haddock, QuickCheck, and Functional Design by Contract

[John Hughes]

Robert Will wrote:

> 4. A notation for preconditions. For simple functions a Precondition
>
>   can be calculated automatically from the Patterns:
>
>  
>
>> head (x:xs) = x
>>    
>>
>
>   Gives the Precondition @xs /= []@ for @head xs at .  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:
>
>  
>
>> take n xs | not (n >= 9) = error "take.Precondition"
>>    
>>
>
>   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?
>
The most lightweight way to specify preconditions would be via another 
function definition with the same parameters and a systematically chosen 
name, for example

    take_pre n xs = n>=0

thus making it easy to generate the QuickCheck property

    prop_take n xs = take_pre n xs ==> take_spec n xs == take n xs

There are some problems in generating such properties automatically, though:

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

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

Perhaps it's simpler just to write QuickCheck properties explicitly?

> 6. Invariants are an important part of Design by Contract according to
>
>   [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.
>
>  
>
In our experience it's important to state properties that invariants are 
preserved by functions -- for example,

    ordered xs ==> ordered (insert x xs)

or rather

   forAll orderedList $ \xs -> ordered (insert x xs)

But I agree, no special notation is needed.

John
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org//pipermail/haskell/attachments/20040217/7676bba8/attachment.htm