From 62abed579e970785ad43041c63dca38eb9206906 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 3 Nov 2014 13:05:04 -0800
Subject: Updated a test case for new syntax and convensions

---
 Test/dafny1/ListContents.dfy        | 106 ++++++++++++++++++------------------
 Test/dafny1/ListContents.dfy.expect |   2 +-
 2 files changed, 55 insertions(+), 53 deletions(-)

(limited to 'Test/dafny1')

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
-- 
cgit v1.2.3