Standard syntax for preconditions, postconditions, and invariants

Neil Mitchell ndmitchell at
Thu Oct 19 10:29:40 EDT 2006


> reverse @ ensure { reverse (reverse xs) == xs }

Question, does "reverse [1..]" meet, or not meet this invariant? What
is the type signature for reverse? What about "reverse [(+),(-)]" ? Is
anything going to be said about the semantics of the invariants? Or
are we just reserving a little piece of syntax that no one else is
going to trample on?

> invariant RedBlackTree a where
>   RBNode False _ l _ r ==> redDepth l == redDepth r

Where does this invariant hold? At all points in time? After a call
has executed? Only between module boundaries?

I'd be wary about taking too much time to specify the syntax of this
kind of thing, and skipping the issue of semantics entirely :)

Also, you might want to look at the programatica project, which I
think has had invariants in their code for years. I'm not sure if the
syntax is the same or not.

That said, I think that embedding invariants/pre/postconditions in the
code is very useful, I just don't think that Haskell' is a good target
for this - there is a big design space that no one has yet explored.



More information about the Haskell-prime mailing list