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