Added a sequence update expression in Dafny.

7 files changed, 30 insertions, 10 deletions

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 4f44612d..ed121ba0 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -100,7 +100,7 @@ class Benchmark3 {
       call r.Enqueue(m);

       pperm:=  pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] +[pperm[k]];

     }

-    assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //needed to trigger axiom

+    assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //lemma needed to trigger axiom

    }

   

   

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index e3a99884..3fa80b4c 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -52,10 +52,8 @@ class Map<Key,Value> {
     if (j == -1) {

       keys := keys + [key];

       values := values + [val];

-      assert values[|keys|-1] == val;  // lemma

     } else {

-      values := values[..j] + [val] + values[j+1..];

-      assert values[j] == val; //lemma

+      values := values[j := val];

     }

   }

 

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index c3374605..bc26ee85 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -298,10 +298,8 @@ class Map<Key,Value> {
     if (j == -1) {

       keys := keys + [key];

       values := values + [val];

-      assert values[|keys|-1] == val;  // lemma

     } else {

-      values := values[..j] + [val] + values[j+1..];

-      assert values[j] == val; //lemma

+      values := values[j := val];

     }

   }

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 78982f01..e7f7c4d6 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -27,6 +27,7 @@ class MyClass<T, U> {
       var to: MyClass<T,U>;

       call to, u, v := M(true, lotsaObjects)

       call to, u, v := to.M(true, lotsaObjects)

+      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

     }

   }

 }

@@ -38,8 +39,11 @@ Dafny program verifier finished with 0 verified, 0 errors
 Boogie program verifier finished with 8 verified, 0 errors

 

 -------------------- SmallTests.dfy --------------------

+SmallTests.dfy(29,7): Error: RHS expression must be well defined

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 3 verified, 0 errors

+Dafny program verifier finished with 4 verified, 1 error

 

 -------------------- Queue.dfy --------------------

 

diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 01d8b63b..759c6afd 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -77,10 +77,10 @@ class Node<T> {
         (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);

     {

       var nx := current.next;

-      assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]);

+      assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma

 

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

-      assert current.data == current.list[0];

+      assert current.data == current.list[0]; // lemma

       current.next := reverse;

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

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

diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index 9f89543c..5f0bee87 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -24,6 +24,7 @@ class MyClass<T,U> {
       var to: MyClass<T,U>;

       call to, u, v := this.M(true, lotsaObjects);

       call to, u, v := to.M(true, lotsaObjects);

+      assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10];

     }

   }

 }

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a2cfc741..01c9f1ea 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -23,4 +23,23 @@ class Node {
     tmp := new Node;

     assert tmp != this;  // was once a bug in the Dafny checker

   }

+

+  method SequenceUpdateOutOfBounds(s: seq<set<int>>, j: int) returns (t: seq<set<int>>)

+  {

+    t := s[j := {}];  // error: j is possibly out of bounds

+  }

+

+  method Sequence(s: seq<bool>, j: int, b: bool, c: bool) returns (t: seq<bool>)

+    requires 10 <= |s|;

+    requires 8 <= j && j < |s|;

+    ensures |t| == |s|;

+    ensures t[8] == s[8] || t[9] == s[9];

+    ensures t[j] == b;

+  {

+    if (c) {

+      t := s[j := b];

+    } else {

+      t := s[..j] + [b] + s[j+1..];

+    }

+  }

 }