Standard syntax for preconditions, postconditions, and invariants

Alan Falloon Al.Falloon at synopsys.com
Thu Oct 19 09:54:06 EDT 2006

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 xs @ require { not (null xs) }

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