Standard syntax for preconditions, postconditions, and invariants

[John Hughes]

>
>> 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
>

I think it's too early for this. As others have pointed out, it's not even 
clear
what the semantics of these things should be. What's more, the way you
write such properties depends partly on what you intend to do with them.
QuickCheck properties aren't just logical properties, they're restricted
to make them testable, and carry extra information to control test case
generation. Other tools, like partly automated provers, may need other
additional information, such as induction variables. We spent a lot of time
looking for a unified property notation in the Cover project, and we didn't
find one we were really happy with. The P-logic that Programmatica uses,
and the preconditions that Dana Xu used in her Haskell workshop paper,
are quite different from each other. We need more research on the tools that
would use these annotations, before we try to fix their syntax.

John