From 2efa59dea051803bc716d02070aa013397cfccc4 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 6 Nov 2009 23:54:22 +0000
Subject: Added a sequence update expression in Dafny.

---
 Test/VSI-Benchmarks/b3.dfy | 2 +-
 Test/VSI-Benchmarks/b4.dfy | 4 +---
 Test/VSI-Benchmarks/b8.dfy | 4 +---
 3 files changed, 3 insertions(+), 7 deletions(-)

(limited to 'Test/VSI-Benchmarks')

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