Add asserts for all even implementations to test-even.ww

team-worthwhile · Mar 10, 2012 · a502560 · a502560
1 parent c62553d
commit a502560
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/implementierung/src/worthwhile.interpreter.tests/src/test/resources/test-even.ww b/implementierung/src/worthwhile.interpreter.tests/src/test/resources/test-even.ww
@@ -49,4 +49,5 @@ if even2(i + 1) {
 
 _assert ¬even2(i)
 
-_assert forall Integer lp : isEven(2 * lp)
+_assert forall Integer lp1 : isEven(2 * lp1) && even(2 * lp1) && even2(2 * lp1)
+_assert forall Integer lp2 : !(isEven(2 * lp2 - 1) || even(2 * lp2 - 1) || even2(2 * lp2 - 1))
diff --git a/implementierung/src/worthwhile.prover.tests/src/test/resources/test-even.ww b/implementierung/src/worthwhile.prover.tests/src/test/resources/test-even.ww
@@ -49,4 +49,5 @@ if even2(i + 1) {
 
 _assert ¬even2(i)
 
-_assert forall Integer lp : isEven(2 * lp)
+_assert forall Integer lp1 : isEven(2 * lp1) && even(2 * lp1) && even2(2 * lp1)
+_assert forall Integer lp2 : !(isEven(2 * lp2 - 1) || even(2 * lp2 - 1) || even2(2 * lp2 - 1))