Remember - unit tests aren't meant to prove the algorithm works; they're meant to determine the adherence of the implementation to the algorithm. So, even if you use all the cases in the proof of the algorithm as tests of the implementation, you still haven't proven the validity of the code like you can prove the validity of the algorithm

I guess the way I am looking at it is that I am not so much looking to directly prove the validity of the algorithm as much as I am trying to test how well the functions retain the integrity of the datastructure and through that indirectly test the validity of the algorithms. This is why I thought that using random data might work out well. Here is an example from the binary tree proofs which may help explain my point of view better (assume 't' is the binary tree).

postorder(mirror(t)) = reverse(preorder(t))

This basically states that the postorder of a mirror of the tree should be equal to the reverse of the preorder of that same tree. This (indirectly) tests the validity of the mirror, postorder and preorder algorithms (the reverse is perl's and assumed to work) by testing that they all work together in the correct way. Running this test on hundreds of randomly constructed trees IMO should say something about the underlying algorithms. Am I wrong in assuming that? Of course if the algorithms are wrong, then with a test like this, they would all have to be wrong in the same way.

-stvn

In reply to Re^2: Theorem proving and Unit testing by stvn
in thread Theorem proving and Unit testing by stvn

Title:
Use:  <p> text here (a paragraph) </p>
and:  <code> code here </code>
to format your post, it's "PerlMonks-approved HTML":


  • Posts are HTML formatted. Put <p> </p> tags around your paragraphs. Put <code> </code> tags around your code and data!
  • Titles consisting of a single word are discouraged, and in most cases are disallowed outright.
  • Read Where should I post X? if you're not absolutely sure you're posting in the right place.
  • Please read these before you post! —
  • Posts may use any of the Perl Monks Approved HTML tags:
    a, abbr, b, big, blockquote, br, caption, center, col, colgroup, dd, del, details, div, dl, dt, em, font, h1, h2, h3, h4, h5, h6, hr, i, ins, li, ol, p, pre, readmore, small, span, spoiler, strike, strong, sub, summary, sup, table, tbody, td, tfoot, th, thead, tr, tt, u, ul, wbr
  • You may need to use entities for some characters, as follows. (Exception: Within code tags, you can put the characters literally.)
            For:     Use:
    & &amp;
    < &lt;
    > &gt;
    [ &#91;
    ] &#93;
  • Link using PerlMonks shortcuts! What shortcuts can I use for linking?
  • See Writeup Formatting Tips and other pages linked from there for more info.