Standard syntax for preconditions, postconditions, and invariants
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
Hi
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. Thanks Neil
On 10/19/06, Neil Mitchell
Hi
reverse @ ensure { reverse (reverse xs) == xs }
Question, does "reverse [1..]" meet, or not meet this invariant?
This is a good point. You can only do sensible conditions on functions if appropriate termination constraints are met.
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?
This invariant holds at the time you build the RBNode. It's effectively a precondition on the RBNode "function".
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.
I agree that Haskell' will not have this, if only under the "must
already be implemented" requirement for major features. However, it
seems that Haskell' is a good way to get people thinking about future
improvements, and I'd hate to stifle that.
--
Taral
Hello Alan, Thursday, October 19, 2006, 5:54:06 PM, you wrote:
I propose that haskell' include a standard syntax for invariants that the programmer wants to express.
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
seems that it should be a sort of annotation, yes? so we again need to define common annotation syntax and you can add this as one more possible usage to annotations-proposal page -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Bulat Ziganshin wrote:
Thursday, October 19, 2006, 5:54:06 PM, you wrote:
I propose that haskell' include a standard syntax for invariants that the programmer wants to express.
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
seems that it should be a sort of annotation, yes? so we again need to define common annotation syntax and you can add this as one more possible usage to annotations-proposal page
It does seem to fit as an annotation. What I am worried about, however, is that if there is no 'official' way to annotate the invariants, then the tool writers will come up with their own slightly incompatible invariant annotations, which would be a shame. This actually seems to be a common issue with annotations. Some of the other proposals are looking to use annotations to specify language extensions that are in effect, and they will also need an 'official' syntax if they want all the compilers to recognize them in the same way. Writing the invariants using a common annotation syntax is great idea though! In fact its better than what I originally had in mind because some tools that use the invariants may need additional information that isn't contained in the common invariant syntax. For instance, I expect any purely static checking of the invariants will probably need help from the developer at various points in a function to complete the proof. When you talk about the "annotations-proposal page", you are referring to the trac ticket right? http://hackage.haskell.org/trac/haskell-prime/ticket/88 Should I apply for an account on trac and modify the ticket?
participants (4)
-
Alan Falloon -
Bulat Ziganshin -
Neil Mitchell -
Taral