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