Establish all desirable system properties (functional, timing, resource, …)
Insert at suitable places in the source code of the system assertion points
Use AnaTempura to check that the generated behaviour satisfies the desired properties
Assertion points → behaviour.
Example: Computation of factorial.
main() { long y, fac=1; assertion("fac", fac); text_out("Enter the seed:"); scanf("%d",&y); assertion("y", y); while (y>1) { fac=fac*y; assertion("fac", fac); y=y-1; assertion("y", y); } }
Will generate the following sequence of changes (seed is 4):
!PROG: assert fac:1:! !PROG: assert y:4:! !PROG: assert fac:4:! !PROG: assert y:3:! !PROG: assert fac:12:! !PROG: assert y:2:! !PROG: assert fac:24:! !PROG: assert y:1:!
The corresponding behaviour (interval):
The property we want to check: (Invariant of the while loop)
define fac_rel(Y,seed) = { if Y=seed then Y else Y * fac_rel(Y+1,seed) }.
The check:
define test() = { exists Fac,Y,seed : { { seed = 1+random mod 9 and prog_send(seed) }; check(1,Fac,Y); if seed>1 then { while Y>1 do check(fac_rel(Y,seed),Fac,Y) } else { empty } } }.
Where
define check(Z,X,Y) = { { skip and get_var("fac",X) and stable(X) and if X=Z then { format("!:: Pass Prog %7d Prop %7d \n", X, Z) } else { format("!:: Fac: Prog %d Prop %d \n", X, Z) } }; { skip and get_var("y",Y) and stable(X) and stable(Y)}; { skip and stable(Y) } }.
Sample test run (seed is 10):
Tempura 1> run test(). !:: Pass Prog 1 Prop 1 !:: Pass Prog 10 Prop 10 !:: Pass Prog 90 Prop 90 !:: Pass Prog 720 Prop 720 !:: Pass Prog 5040 Prop 5040 !:: Pass Prog 30240 Prop 30240 !:: Pass Prog 151200 Prop 151200 !:: Pass Prog 604800 Prop 604800 !:: Pass Prog 1814400 Prop 1814400 !:: Pass Prog 3628800 Prop 3628800 Done! Computation length: 30. Total Passes: 31. Total reductions: 4164(4164 successful). Maximum reduction depth: 31.