equal
deleted
inserted
replaced
24 "s ==> exec c1 s t ==> exec (IF c1 c2) s t" | |
24 "s ==> exec c1 s t ==> exec (IF c1 c2) s t" | |
25 "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t" |
25 "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t" |
26 |
26 |
27 lemma |
27 lemma |
28 "exec c s s' ==> exec (Seq c c) s s'" |
28 "exec c s s' ==> exec (Seq c c) s s'" |
29 quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, timeout = 600.0, expect = counterexample] |
29 quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample] |
30 oops |
30 oops |
31 |
31 |
32 |
32 |
33 end |
33 end |