From e90be508dcf82fd35d88107186059bb37f534acb Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 6 May 2010 23:35:04 +0000
Subject: Dafny: * Recoded frame axioms to be more goal directed * Added Main
 test driver to Test/VSI-Benchmarks/b2.dfy

---
 Test/VSI-Benchmarks/Answer | 2 +-
 Test/VSI-Benchmarks/b2.dfy | 7 +------
 2 files changed, 2 insertions(+), 7 deletions(-)

(limited to 'Test/VSI-Benchmarks')

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 926a4da3..1efeba04 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -5,7 +5,7 @@ Dafny program verifier finished with 10 verified, 0 errors
 
 -------------------- b2.dfy --------------------
 
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 12 verified, 0 errors
 
 -------------------- b3.dfy --------------------
 
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 0cae993a..86c12854 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -63,16 +63,12 @@ class Array {
   method Set(i: int, x: int)
     requires 0 <= i && i < |contents|;
     modifies this;
-    ensures |contents| == |old(contents)|;
-    ensures contents[..i] == old(contents[..i]);
-    ensures contents[i] == x;
-    ensures contents[i+1..] == old(contents[i+1..]);
+    ensures contents == old(contents)[i := x];
   {
     contents := contents[i := x];
   }
 }
 
-/******
 method Main() {
   var a := new Array;
   call a.Init(5);
@@ -103,4 +99,3 @@ method TestSearch(a: Array, key: int)
   call r := b.BinarySearch(a, key);
   print "Looking for key=", key, ", result=", r, "\n";
 }
-******/
-- 
cgit v1.2.3