Updated a test case for new syntax and convensions

2 files changed, 55 insertions, 53 deletions

diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy
index b79d3308..3efe2fd0 100644
--- a/Test/dafny1/ListContents.dfy
+++ b/Test/dafny1/ListContents.dfy
@@ -2,90 +2,92 @@
 // RUN: %diff "%s.expect" "%t"

 

 class Node<T> {

-  var list: seq<T>;

-  var footprint: set<Node<T>>;

+  ghost var List: seq<T>;

+  ghost var Repr: set<Node<T>>;

 

   var data: T;

   var next: Node<T>;

 

-  function Valid(): bool

-    reads this, footprint;

+  predicate Valid()

+    reads this, Repr

   {

-    this in this.footprint && null !in this.footprint &&

-    (next == null ==> list == [data]) &&

+    this in Repr && null !in Repr &&

+    (next == null ==> List == [data]) &&

     (next != null ==>

-        next in footprint && next.footprint <= footprint &&

-        this !in next.footprint &&

-        list == [data] + next.list &&

+        next in Repr && next.Repr <= Repr &&

+        this !in next.Repr &&

+        List == [data] + next.List &&

         next.Valid())

   }

 

-  method Init(d: T)

-    modifies this;

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

-    ensures list == [d];

+  constructor (d: T)

+    modifies this

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

+    ensures List == [d]

   {

-    data := d;

-    next := null;

-    list := [d];

-    footprint := {this};

+    data, next := d, null;

+    List, Repr := [d], {this};

   }

 

-  method SkipHead() returns (r: Node<T>)

-    requires Valid();

-    ensures r == null ==> |list| == 1;

-    ensures r != null ==> r.Valid() && r.footprint <= footprint;

-    ensures r != null ==> r.list == list[1..];

+  constructor InitAsPredecessor(d: T, succ: Node<T>)

+    requires succ != null && succ.Valid() && this !in succ.Repr;

+    modifies this;

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

+    ensures List == [d] + succ.List;

   {

-    r := next;

+    data, next := d, succ;

+    List := [d] + succ.List;

+    Repr := {this} + succ.Repr;

   }

 

   method Prepend(d: T) returns (r: Node<T>)

-    requires Valid();

-    ensures r != null && r.Valid() && fresh(r.footprint - old(footprint));

-    ensures r.list == [d] + list;

+    requires Valid()

+    ensures r != null && r.Valid() && fresh(r.Repr - old(Repr))

+    ensures r.List == [d] + List

   {

-    r := new Node<T>;

-    r.data := d;

-    r.next := this;

-    r.footprint := {r} + this.footprint;

-    r.list := [r.data] + this.list;

+    r := new Node.InitAsPredecessor(d, this);

   }

   

+  method SkipHead() returns (r: Node<T>)

+    requires Valid()

+    ensures r == null ==> |List| == 1

+    ensures r != null ==> r.Valid() && r.List == List[1..] && r.Repr <= Repr

+  {

+    r := next;

+  }

+

   method ReverseInPlace() returns (reverse: Node<T>)

-    requires Valid();

-    modifies footprint;

-    ensures reverse != null && reverse.Valid();

-    ensures fresh(reverse.footprint - old(footprint));

-    ensures |reverse.list| == |old(list)|;

-    ensures (forall i :: 0 <= i && i < |old(list)| ==> old(list)[i] == reverse.list[|old(list)|-1-i]);

+    requires Valid()

+    modifies Repr

+    ensures reverse != null && reverse.Valid() && reverse.Repr <= old(Repr)

+    ensures |reverse.List| == |old(List)|

+    ensures forall i :: 0 <= i < |reverse.List| ==> reverse.List[i] == old(List)[|old(List)|-1-i]

   {

     var current := next;

     reverse := this;

     reverse.next := null;

-    reverse.footprint := {reverse};

-    reverse.list := [data];

+    reverse.Repr := {reverse};

+    reverse.List := [data];

     

-    while (current != null)

-      invariant reverse != null && reverse.Valid();

-      invariant reverse.footprint <= old(footprint);

-      invariant current == null ==> |old(list)| == |reverse.list|;

+    while current != null

+      invariant reverse != null && reverse.Valid() && reverse.Repr <= old(Repr)

+      invariant current == null ==> |old(List)| == |reverse.List|

       invariant current != null ==>

         current.Valid() &&

-        current in old(footprint) && current.footprint <= old(footprint) &&

-        current.footprint !! reverse.footprint &&

-        |old(list)| == |reverse.list| + |current.list|;

-      invariant current != null ==> current.list == old(list)[|reverse.list|..];

-      invariant

-        (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);

-      decreases if current != null then |current.list| else -1;

+        current in old(Repr) && current.Repr <= old(Repr) &&

+        current.Repr !! reverse.Repr

+      invariant current != null ==>

+        |old(List)| == |reverse.List| + |current.List| &&

+        current.List == old(List)[|reverse.List|..]

+      invariant forall i :: 0 <= i < |reverse.List| ==> reverse.List[i] == old(List)[|reverse.List|-1-i]

+      decreases if current != null then |current.List| else -1

     {

       var nx := current.next;

 

       // ..., reverse, current, nx, ...

       current.next := reverse;

-      current.footprint := {current} + reverse.footprint;

-      current.list := [current.data] + reverse.list;

+      current.Repr := {current} + reverse.Repr;

+      current.List := [current.data] + reverse.List;

 

       reverse := current;

       current := nx;

diff --git a/Test/dafny1/ListContents.dfy.expect b/Test/dafny1/ListContents.dfy.expect
index 249e77e5..f3a9c95f 100644
--- a/Test/dafny1/ListContents.dfy.expect
+++ b/Test/dafny1/ListContents.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 9 verified, 0 errors

+Dafny program verifier finished with 11 verified, 0 errors