Download HOL-TestGen: User Guide

gen test data "max_test"
The Isabelle command thm allows for interactive inspections of the result:
thm max_test.test_data
which is:
prog -2 -1 = -1
prog 10 -8 = 10
in this case.
Analogously, we can also inspect the test hypotheses and the test theorem:
thm max_test.test_hyps
which yields:
THYP ((∃ x xa. xa ≤ x −→ prog xa x = x) −→ (∀ x xa. xa ≤ x −→ prog xa x = x))
THYP
((∃ x xa. ¬ xa ≤ x −→ prog xa x = xa) −→
(∀ x xa. ¬ xa ≤ x −→ prog xa x = xa))
and
thm max_test.test_thm
resulting in:
[[?X2X24 ≤ ?X1X22 =⇒ prog ?X2X24 ?X1X22 = ?X1X22;
THYP
((∃ x xa. xa ≤ x −→ prog xa x = x) −→ (∀ x xa. xa ≤ x −→ prog xa x = x));
¬ ?X2X14 ≤ ?X1X12 =⇒ prog ?X2X14 ?X1X12 = ?X2X14;
THYP
((∃ x xa. ¬ xa ≤ x −→ prog xa x = xa) −→
(∀ x xa. ¬ xa ≤ x −→ prog xa x = xa))]]
=⇒ (prog a b = max a b)
We turn now to the automatic generation of a test harness. This is performed by the top-level
command:
gen test script "document/max_script.sml" "max_test" "prog" "myMax.max"
which generates:
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
*
Test - Driver
*
g e n e r a t e d by HOL - TestGen 1.5.0 - pre ( alpha : 8882)
* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
structure TestDriver : sig end = struct
val
fun
fun
fun
return = ref ( ~4:( int ));
eval x2 x1 = let val ret = myMax . max
retval () = SOME (! return );
toString a = Int . toString a ;
val testres = [];
38
x2
x1
in (( return := ret ); ret ) end