Standard syntax for preconditions, postconditions, and invariants

[Alan Falloon]

I propose that haskell' include a standard syntax for invariants that 
the programmer wants to express. Here is a rough idea (just to get the 
point across):

\begin{code}

head :: [a] -> a
head xs @ require { not (null xs) }
head (x:xs) = x

reverse :: [a] -> [a]
reverse @ ensure { reverse (reverse xs) == xs }
reverse [] = []
reverse (x:xs) = reverse xs ++ x

data RedBlackTree a = RBLeaf a |  RBNode  Bool  (RedBlackTree a) a 
(RedBlackTree a)
invariant RedBlackTree a where
  RBNode False _ l _ r ==> redDepth l == redDepth r

\end{code}

The intent is not to have standardized checks on the invariants, its 
just to supply a common way to specify invariants to that the various 
strategies for checking them can all work from the same data. For 
example, one tool might use the invariants to generate QuickCheck 
properties, a compiler might provide a mode that does run-time checking 
of the invariants, and another tool might try to prove the invariants 
statically like in ESC [1]. Eventually, we might end up with 
sophisticated hybrid approaches that combine static proof with 
generating test cases for the unprovable bits. At the very least Haddock 
could include the invariants as part of the documentation.

[1] http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps