Standard syntax for preconditions, postconditions,
Al.Falloon at synopsys.com
Fri Oct 20 08:14:17 EDT 2006
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
> 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?
More information about the Haskell-prime