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.
http://www.haskell.org/ghc/docs/latest/html/libraries/QuickCheck/Test.QuickCheck.html
:-)
Luke
