diff options
| author |  leino <unknown> | 2015-05-07 09:42:21 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-07 09:42:21 -0700 |
| commit | 9e999ccbf8581acf181ff00a529de96e12c690d5 (patch) | |
| tree | 0b9bd5d56a2f7a41dc520274d8d110bee997f5b1 | |
| parent | cafbf508ea7aa6f337140293105060393ccb11f5 (diff) | |
Additional test case for inductive predicates
| -rw-r--r-- | Test/dafny0/InductivePredicates.dfy | 83 | ||||
| -rw-r--r-- | Test/dafny0/InductivePredicates.dfy.expect | 6 |
2 files changed, 79 insertions, 10 deletions
diff --git a/Test/dafny0/InductivePredicates.dfy b/Test/dafny0/InductivePredicates.dfy index 5f1184f1..424118e7 100644 --- a/Test/dafny0/InductivePredicates.dfy +++ b/Test/dafny0/InductivePredicates.dfy @@ -3,13 +3,6 @@ datatype natinf = N(n: nat) | Inf
-function S(x: natinf): natinf
-{
- match x
- case N(n) => N(n+1)
- case Inf => Inf
-}
-
inductive predicate Even(x: natinf)
{
(x.N? && x.n == 0) ||
@@ -104,3 +97,79 @@ lemma OneMore(x: natinf) returns (y: natinf) {
y := N(x.n + 2);
}
+
+// ----------------------- Here's another version of Even, using the S function
+
+module Alt {
+ datatype natinf = N(n: nat) | Inf
+
+ function S(x: natinf): natinf
+ {
+ match x
+ case N(n) => N(n+1)
+ case Inf => Inf
+ }
+
+ inductive predicate Even(x: natinf)
+ {
+ (x.N? && x.n == 0) ||
+ exists y :: x == S(S(y)) && Even(y)
+ }
+
+ inductive lemma MyLemma_NotSoNice(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+ {
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case exists y :: x == S(S(y)) && Even#[_k-1](y) =>
+ var y :| x == S(S(y)) && Even#[_k-1](y);
+ MyLemma_NotSoNice(y);
+ assert x.n == y.n + 2;
+ }
+ }
+
+ inductive lemma MyLemma_NiceButNotFast(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+ {
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case exists y :: x == S(S(y)) && Even(y) =>
+ var y :| x == S(S(y)) && Even(y);
+ MyLemma_NiceButNotFast(y);
+ assert x.n == y.n + 2;
+ }
+ }
+
+ lemma InfNotEven()
+ ensures !Even(Inf)
+ {
+ if Even(Inf) {
+ InfNotEven_Aux();
+ }
+ }
+
+ inductive lemma InfNotEven_Aux()
+ requires Even(Inf)
+ ensures false
+ {
+ var x := Inf;
+ if {
+ case x.N? && x.n == 0 =>
+ assert false; // this case is absurd
+ case exists y :: x == S(S(y)) && Even(y) =>
+ var y :| x == S(S(y)) && Even(y);
+ assert y == Inf;
+ InfNotEven_Aux();
+ }
+ }
+
+ lemma NextEven(x: natinf)
+ requires Even(x)
+ ensures Even(S(S(x)))
+ {
+ }
+}
diff --git a/Test/dafny0/InductivePredicates.dfy.expect b/Test/dafny0/InductivePredicates.dfy.expect index a57b7d70..b09b7903 100644 --- a/Test/dafny0/InductivePredicates.dfy.expect +++ b/Test/dafny0/InductivePredicates.dfy.expect @@ -1,9 +1,9 @@ -InductivePredicates.dfy(71,10): Error: assertion violation
+InductivePredicates.dfy(64,10): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-InductivePredicates.dfy(83,11): Error: assertion violation
+InductivePredicates.dfy(76,11): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 18 verified, 2 errors
+Dafny program verifier finished with 29 verified, 2 errors
|