Added inductive predicates

4 files changed, 184 insertions, 2 deletions

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index 99b263a5..850fa4c1 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -129,7 +129,7 @@ module CoPredicateResolutionErrors {
   }

 

   ghost method Lemma(n: int)

-    ensures Even(Doubles(n));

+    ensures Even(Doubles(n))

   {

   }

 

@@ -184,3 +184,93 @@ module UnfruitfulCoLemmaConclusions {
   {

   }

 }

+

+// --------------- Inductive Predicates --------------------------

+

+module InductivePredicateResolutionErrors {

+

+  datatype List<T> = Nil | Cons(head: T, tail: List)

+  codatatype IList<T> = INil | ICons(head: T, tail: IList)

+

+  inductive predicate Pos(s: List<int>)

+  {

+    s.Cons? && 0 < s.head && Pos(s.tail) && Even(s)

+  }

+

+  inductive predicate Even(s: List<int>)

+  {

+    s.Cons? && s.head % 2 == 0 && Even(s.tail)

+    && (s.head == 17 ==> Pos(s))

+    && (Pos(s) ==> s.head == 17)  // error: cannot make recursive inductive-predicate call in negative position

+    && !Even(s)  // error: cannot make recursive inductive-predicate call in negative position

+    && (Even(s) <==> Even(s))  // error (x2): recursive inductive-predicate calls allowed only in positive positions

+  }

+

+  inductive predicate LetSuchThat(s: List<int>)

+  {

+    if s != Nil then true else

+      var h :| h == s.head;

+      h < 0 && LetSuchThat(s.tail)  // this is fine for an inductive predicate

+  }

+  copredicate CoLetSuchThat(s: IList<int>)

+  {

+    if s != INil then true else

+      var h :| h == s.head;

+      h < 0 && CoLetSuchThat(s.tail)  // error: recursive call to copredicate in body of let-such-that

+  }

+

+  inductive predicate CP(i: int)

+  {

+    CP(i) &&

+    !CP(i) &&  // error: not in a positive position

+    (exists j :: CP(j)) &&

+    (forall k :: 0 <= k < i*i ==> CP(k)) &&

+    (forall k :: 0 <= k ==> CP(k)) &&  // error: unbounded range

+    (forall k :: k < i*i ==> CP(k)) &&  // error: unbounded range

+    (forall l :: CP(l))  // error: unbounded range

+  }

+

+  inductive predicate CQ(i: int, j: int)

+  {

+    forall i :: i == 6 ==> if j % 2 == 0 then CQ(i, i) else CQ(j, j)

+  }

+

+  inductive predicate CR(i: int, j: int)

+  {

+    i == if CR(i, j) then 6 else j  // error: not allowed to call CR recursively here

+  }

+

+  inductive predicate CS(i: int, j: int)

+  {

+    forall i ::

+      i <= (if CS(i, j) then 6 else j) &&  // error: not allowed to call CS recursively here

+      (if CS(i, j) then 6 else j) <= i     // error: not allowed to call CS recursively here

+  }

+

+  inductive predicate Another(s: List<int>)

+  {

+    !Even(s)  // here, negation is fine

+  }

+

+  inductive predicate IndStmtExpr_Good(s: List<int>)

+  {

+    s.head > 0 && (MyLemma(s.head); IndStmtExpr_Good(s.tail))

+  }

+

+  lemma MyLemma(x: int)

+  {

+  }

+

+  inductive predicate IndStmtExpr_Bad(s: List<int>)

+  {

+    s.Cons? && s.head > 0 &&

+    (MyRecursiveLemma(s.head);  // error: cannot call method recursively from inductive predicate

+     IndStmtExpr_Bad(s.tail))

+  }

+

+  lemma MyRecursiveLemma(x: int)

+  {

+    var p := IndStmtExpr_Bad(Cons(x, Nil));

+  }

+}

+

diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect
index 26fec211..0ab15059 100644
--- a/Test/dafny0/Coinductive.dfy.expect
+++ b/Test/dafny0/Coinductive.dfy.expect
@@ -14,4 +14,17 @@ Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in
 Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

 Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

 Coinductive.dfy(148,21): Error: a recursive call from a copredicate can go only to other copredicates

-16 resolution/type errors detected in Coinductive.dfy

+Coinductive.dfy(204,8): Error: an inductive predicate can be called recursively only in positive positions

+Coinductive.dfy(205,8): Error: an inductive predicate can be called recursively only in positive positions

+Coinductive.dfy(206,8): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(206,21): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(219,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+Coinductive.dfy(225,5): Error: an inductive predicate can be called recursively only in positive positions

+Coinductive.dfy(228,28): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(229,29): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(230,17): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(240,12): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(246,15): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(247,10): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(267,21): Error: a recursive call from an inductive predicate can go only to other inductive predicates

+29 resolution/type errors detected in Coinductive.dfy

diff --git a/Test/dafny0/InductivePredicates.dfy b/Test/dafny0/InductivePredicates.dfy
new file mode 100644
index 00000000..9250fade
--- /dev/null
+++ b/Test/dafny0/InductivePredicates.dfy
@@ -0,0 +1,74 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+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) ||

+  (x.N? && 2 <= x.n && Even(N(x.n - 2)))

+}

+

+lemma M(x: natinf)

+  requires Even(x)

+  ensures x.N? && x.n % 2 == 0

+{

+  var k: nat :| Even#[k](x);

+  M'(k, x);

+}

+

+// yay!  my first proof involving an inductive predicate :)

+lemma M'(k: nat, x: natinf)

+  requires Even#[k](x)

+  ensures x.N? && x.n % 2 == 0

+{

+  if 0 < k {

+    if {

+      case x.N? && x.n == 0 =>

+        // trivial

+      case x.N? && 2 <= x.n && Even#[k-1](N(x.n - 2)) =>

+        M'(k-1, N(x.n - 2));

+    }

+  }

+}

+

+lemma InfNotEven()

+  ensures !Even(Inf)

+{

+}

+

+lemma Test()

+{

+  assert !Even(N(1));  // Dafny can prove this

+  assert !Even(N(5));

+  assert !Even(N(17));  // error: this holds, but Dafny can't prove it directly (but see lemma below)

+}

+

+lemma SeventeenIsNotEven()

+  ensures !Even(N(17))

+{

+  assert Even(N(17))

+      == Even(N(15))

+      == Even(N(13))

+      == Even(N(11))

+      == Even(N(9))

+      == Even(N(7))

+      == Even(N(5))

+      == Even(N(3))

+      == Even(N(1))

+      == false;

+}

+

+lemma OneMore(x: natinf) returns (y: natinf)

+  requires Even(x)

+  ensures Even(y)

+{

+  y := N(x.n + 2);

+}

diff --git a/Test/dafny0/InductivePredicates.dfy.expect b/Test/dafny0/InductivePredicates.dfy.expect
new file mode 100644
index 00000000..c0feb7dd
--- /dev/null
+++ b/Test/dafny0/InductivePredicates.dfy.expect
@@ -0,0 +1,5 @@
+InductivePredicates.dfy(51,11): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 13 verified, 1 error