Split verification of quantifier expressions into #2 for checked and #1 for assumed.

Fixed cases where token was not being updated for refinement.

1 files changed, 23 insertions, 23 deletions

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 19375ac2..1610d8b8 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -15,7 +15,7 @@ module A {
     method N()

       modifies this;

       ensures P();

-    {

+    {  // error: in module B, the postcondition P() has been strengthened and no longer holds

       x := -28;

     }

   }

@@ -36,7 +36,7 @@ module Loose {
   class MyNumber {

     var N: int;

     ghost var Repr: set<object>;

-    predicate Valid

+    predicate Valid()

       reads this, Repr;

     {

       this in Repr && null !in Repr &&

@@ -44,20 +44,20 @@ module Loose {
     }

     constructor Init()

       modifies this;

-      ensures Valid && fresh(Repr - {this});

+      ensures Valid() && fresh(Repr - {this});

     {

       N, Repr := 0, {this};

     }

     method Inc()

-      requires Valid;

+      requires Valid();

       modifies Repr;

       ensures old(N) < N;

-      ensures Valid && fresh(Repr - old(Repr));

+      ensures Valid() && fresh(Repr - old(Repr));

     {

       N := N + 2;

     }

     method Get() returns (n: int)

-      requires Valid;

+      requires Valid();

       ensures n == N;

     {

       n := N;

@@ -67,7 +67,7 @@ module Loose {
 

 module Tight refines Loose {

   class MyNumber {

-    predicate Valid

+    predicate Valid()

     {

       N % 2 == 0

     }

@@ -107,20 +107,20 @@ module AwareClient {
 module Tricky_Base {

   class Tree {

     var x: int;

-    predicate Constrained

+    predicate Constrained()

       reads this;

     {

       x < 10

     }

-    predicate Valid

+    predicate Valid()

       reads this;

     {

       x < 100

     }

     method Init()

       modifies this;

-      ensures Valid;

-    {

+      ensures Valid();

+    {  // error: in module Tricky_Full, the strengthened postcondition Valid() no longer holds

       x := 20;

     }

   }

@@ -128,7 +128,7 @@ module Tricky_Base {
 

 module Tricky_Full refines Tricky_Base {

   class Tree {

-    predicate Valid

+    predicate Valid()

     {

       Constrained  // this causes an error to be generated for the inherited Init

     }

@@ -140,43 +140,43 @@ module Tricky_Full refines Tricky_Base {
 module Q0 {

   class C {

     var x: int;

-    predicate P

+    predicate P()

       reads this;

     {

       true

     }

     method M()

       modifies this;

-      ensures forall c: C :: c != null ==> c.P;

-    {

+      ensures forall c: C :: c != null ==> c.P();

+    {  // error: in module Q1, the postcondition no longer holds

     }

-    predicate Q

+    predicate Q()

       reads this;

     {

       x < 100

     }

     method N()

       modifies this;

-      ensures forall c :: c == this ==> c.Q;

-    {

-      x := 102;  // error: fails to establish postcondition (but this error should not be repeated in Q1 below)

+      ensures forall c :: c == this ==> c.Q();

+    {  // error: fails to establish postcondition (but this error should not be repeated in Q1 below)

+      x := 102;

     }

-    predicate R reads this;  // a body-less predicate

+    predicate R() reads this;  // a body-less predicate

   }

 }

 

 module Q1 refines Q0 {

   class C {

-    predicate P

+    predicate P()

     {

       x == 18

     }

-    predicate R  // no body yet

+    predicate R()  // no body yet

   }

 }

 

 module Q2 refines Q1 {

   class C {

-    predicate R { x % 3 == 2 }  // finally, give it a body

+    predicate R() { x % 3 == 2 }  // finally, give it a body

   }

 }