Standard syntax for preconditions, postconditions, and invariants

[Alan Falloon]

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?