From 14e28e64aaae0c5620c2d2f2a3d13350b472b1e9 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 12 Mar 2010 04:12:37 +0000
Subject: Dafny: * Modifies clause checking is now done with each update,
 instead of at the end of the method.  Not only does this improve error
 messages, but on some examples, it gives a dramatic speed-up (2x) in proving
 time. * bugfix: range expressions of foreach statements were previously
 ignored during Translation

---
 Test/VSI-Benchmarks/b3.dfy | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'Test/VSI-Benchmarks')

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index e3a91ab2..d45db684 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -10,8 +10,6 @@
 // pperm, had to write invariants over p and perm rather than pperm and we couldn't use 
 // "x in p".
 
-//would be nice if we could mark pperm as a ghost variable
-
 class Queue<T> {
   var contents: seq<T>;
   method Init();
@@ -43,7 +41,7 @@ class Comparable {
 class Benchmark3 {
 
 
-  method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)
+  method Sort(q: Queue<int>) returns (r: Queue<int>, ghost perm:seq<int>)
     requires q != null;
     modifies q;
     ensures r != null && fresh(r);
@@ -59,7 +57,7 @@ class Benchmark3 {
   {
     r := new Queue<int>;
     call r.Init();
-    var p:= [];
+    ghost var p:= [];
     
     var n := 0;
 	while (n < |q.contents|)
@@ -72,7 +70,7 @@ class Benchmark3 {
 		n := n + 1;
    }
    perm:= [];
-   var pperm := p + perm; 
+   ghost var pperm := p + perm; 
    
     while (|q.contents| != 0)
       invariant |r.contents| == |old(q.contents)| - |q.contents|;
-- 
cgit v1.2.3