Simple Parity Test

proofs/parity.dfy

@@ -0,0 +1,8 @@
+lemma {:induction false} ParityProof(x: nat, y: nat) 
+    requires isEven(x) || isEven(y)
+    ensures isEven(x * y)
+    decreases x + y
+{
+
+}
+

testcases/parity.dfy

@@ -0,0 +1,14 @@
+predicate {:induction false} isEven(n: nat)
+{
+    if n == 0 then true 
+    else if n == 1 then false 
+    else isEven(n - 2)
+}
+
+method {:induction false} ParityTest(x: nat, y: nat) 
+    requires isEven(x) || isEven(y)
+{
+    assert isEven(x * y) by {
+        ParityProof(x, y);
+    }
+}