From b4a219dac0944f0a4a398538f4c05edc8ec9a71b Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 13 Mar 2010 03:30:09 +0000
Subject: Dafny:  Added definedness checks for all statements (previously, some
 were missing)

Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
---
 Test/VSI-Benchmarks/b2.dfy |  2 +-
 Test/VSI-Benchmarks/b3.dfy |  6 ++--
 Test/VSI-Benchmarks/b6.dfy | 90 +++++++++++++++++++++++-----------------------
 3 files changed, 49 insertions(+), 49 deletions(-)

(limited to 'Test/VSI-Benchmarks')

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 457bc894..7d964061 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -17,7 +17,7 @@ class Benchmark2 {
     var high := a.Length();
 
     while (low < high)
-      invariant 0 <= low && high <= a.Length();
+      invariant 0 <= low && low <= high && high <= a.Length();
       invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);
       invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));
       decreases high - low;
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index d45db684..37b73cba 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -61,10 +61,10 @@ class Benchmark3 {
     
     var n := 0;
 	while (n < |q.contents|)
-		invariant n <=|q.contents| ;
-		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
+		invariant n <= |q.contents|;
 		invariant n == |p|;
-		decreases |q.contents| -n;
+		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
+		decreases |q.contents| - n;
    {
 		p := p + [n];
 		n := n + 1;
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index d320f9e9..90f484bd 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -6,22 +6,22 @@ class Collection<T> {
   function Valid():bool
   reads this, footprint;
   {
-		this in footprint
+    this in footprint
   }
   
   method GetCount() returns (c:int)
   requires Valid();
   ensures 0<=c;
   {
-		c:=|elements|;
+    c:=|elements|;
   }
   
   method Init()
   modifies this;
   ensures Valid() && fresh(footprint -{this});
   {
-		elements := [];
-		footprint := {this}; 
+    elements := [];
+    footprint := {this}; 
   }
   
   method GetItem(i:int ) returns (x:T)
@@ -29,7 +29,7 @@ class Collection<T> {
   requires 0<=i && i<|elements|;
   ensures elements[i] ==x;
   {
-		x:=elements[i];
+    x:=elements[i];
   }
   
   method Add(x:T )
@@ -38,7 +38,7 @@ class Collection<T> {
   ensures Valid() && fresh(footprint - old(footprint));
   ensures elements == old(elements) + [x];
   {
-		elements:= elements + [x];
+    elements:= elements + [x];
   }
   
   method GetIterator() returns (iter:Iterator<T>)
@@ -63,7 +63,7 @@ class Iterator<T> {
   function Valid():bool
   reads this, footprint;
   {
-		this in footprint && c!= null && -1<= pos && null !in footprint
+    this in footprint && c!= null && -1<= pos && null !in footprint
   }
   
   method Init(coll:Collection<T>)
@@ -72,9 +72,9 @@ class Iterator<T> {
   ensures Valid() && fresh(footprint -{this}) && pos ==-1;
   ensures c == coll;
   {
-		c:= coll;
-		pos:=-1;
-		footprint := {this}; 
+    c:= coll;
+    pos:=-1;
+    footprint := {this}; 
   }
   
   method MoveNext() returns (b:bool)
@@ -83,22 +83,22 @@ class Iterator<T> {
   ensures fresh(footprint - old(footprint)) &&  Valid()  && pos == old(pos) + 1;
   ensures b == HasCurrent() && c == old(c);
   {
-	pos:= pos+1;
-	b:= pos < |c.elements|;
+  pos:= pos+1;
+  b:= pos < |c.elements|;
   }
   
  function HasCurrent():bool //???
- requires Valid();
- reads this, c;
+   requires Valid();
+   reads this, c;
  {
-	0<= pos && pos < |c.elements|
+  0<= pos && pos < |c.elements|
  }
  
  method GetCurrent() returns (x:T)
  requires Valid() && HasCurrent();
  ensures c.elements[pos] == x;
   {
-		x:=c.elements[pos];
+    x:=c.elements[pos];
   }
  
 } 
@@ -106,34 +106,34 @@ class Iterator<T> {
 class Client
 {
 
-	method Main()
-	{
-		var c:= new Collection<int>;
-		call c.Init();
-		call c.Add(33);
-		call c.Add(45);
-		call c.Add(78);
-		
-		var s:= [ ];
-		
-		call iter:=c.GetIterator();
-		call b:= iter.MoveNext();
-		
-		while (b)
-		invariant b == iter.HasCurrent() && fresh(iter.footprint) && iter.Valid();
-		invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints
-		invariant 0<= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;
-		invariant iter.c == c;
-		decreases |c.elements| - iter.pos;
-		{   
-			call x:= iter.GetCurrent();
-			s:= s + [x];
-			call b:= iter.MoveNext();
-		}
-		
-		assert s == c.elements; //verifies that the iterator returns the correct things
-		call c.Add(100);
-	}
-	
+  method Main()
+  {
+    var c:= new Collection<int>;
+    call c.Init();
+    call c.Add(33);
+    call c.Add(45);
+    call c.Add(78);
+    
+    var s:= [ ];
+    
+    call iter := c.GetIterator();
+    call b := iter.MoveNext();
+    
+    while (b)
+      invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);
+      invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints
+      invariant 0 <= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;
+      invariant iter.c == c;
+      decreases |c.elements| - iter.pos;
+    {   
+      call x:= iter.GetCurrent();
+      s:= s + [x];
+      call b:= iter.MoveNext();
+    }
+    
+    assert s == c.elements; //verifies that the iterator returns the correct things
+    call c.Add(100);
+  }
+  
 }
 
-- 
cgit v1.2.3