Changes between Initial Version and Version 3 of Ticket #38


Ignore:
Timestamp:
Oct 9, 2007, 6:31:14 AM (17 years ago)
Author:
alex heneveld
Comment:

accepting. will draft proposal using cruisecontrol and junit.

at this point i'm thinking there are three types of tests we want:

via a suite-builder for pointing a unit test case at a collection of proofs, e.g. we write a test case which tests a theory file parses completely, then build a suite which runs that test case against all theories in a predefined "parseable proof files" collection (and another test case for theory files which execute completely, etc...)

extending a fixture to write a test script asserting behaviour in a single proof, e.g. to load A.thy, send "next" 3 times, assert we've just proven Foo, send undo, assert the lemma "Foo" is now undone.

normal units (pojo and ui-plugin), typically simpler than the above two; e.g. asserting that preferences load, that we can connect to the prover, that a theory file opens with the right prover, etc.

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #38

    • Property Owner changed from David Aspinall to alex heneveld