On 10/13/05, Dave Whipp <[EMAIL PROTECTED]> wrote:
> I started thinking about the "in general, unverifiable programmatically"
> bit. While obviously true, perhaps we can get closer than just leaving
> them as comments. It should be possible to associate a
> unit-test-generator with the theory, so I can say:
> theory Ring(::R) {
>     ...
>     axiom associative(R ($a, $b, $b)) {
>       is_true( ((a+b)+c) - (a+(b+c)) eqv R(0) );
>     }
>     ...
> }
> And then say "for type T, please generate 1000 random tests of T using
> axioms of Ring".

The points about hand-crafted edge-case tests are good, but that's not
to say that this isn't a good idea.  Putting the properties inline
with the theory is good documentation (plus, as you say, it could be
used to generate pre- and postconditions).

By the way, Haskell already did this. 



Reply via email to