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
_______________________________________________
Haskell-prime mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-prime
