diff options
| author |  chmaria <unknown> | 2012-06-18 15:00:48 +0200 |
|---|---|---|
| committer | chmaria <unknown> | 2012-06-18 15:00:48 +0200 |
| commit | 6e0e8b16609329816c07c7ef451479861ed89abe (patch) | |
| tree | c6e60423355816f52b0633f2bcca5cdda5732733 /Test | |
| parent | c0f50ec423987b670181d13a416c1bffd279556a (diff) | |
| parent | 0788f5ea2bb20f079ffa5294d52fe76b78c74fa9 (diff) | |
Merged with default.
Diffstat (limited to 'Test')
30 files changed, 553 insertions, 100 deletions
diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat index 9535d677..63f5df23 100644 --- a/Test/VSComp2010/runtest.bat +++ b/Test/VSComp2010/runtest.bat @@ -3,8 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy
Problem3-FindZero.dfy Problem4-Queens.dfy
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index 611f9251..f5b9d1b9 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -3,8 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (
echo.
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c451cc62..5f80df86 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -91,8 +91,10 @@ TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
-34 resolution/type errors detected in TypeTests.dfy
+36 resolution/type errors detected in TypeTests.dfy
-------------------- NatTypes.dfy --------------------
NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
@@ -280,7 +282,7 @@ Execution trace: (0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-SmallTests.dfy(584,18): Error: target object may be null
+SmallTests.dfy(584,25): Error: target object may be null
Execution trace:
(0,0): anon0
SmallTests.dfy(597,10): Error: assertion violation
@@ -712,13 +714,13 @@ Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
-Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M
-Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M
-Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M
-Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M
-Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)
-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)
Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
@@ -730,13 +732,20 @@ Modules0.dfy(250,15): Error: unresolved identifier: X Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X
Modules0.dfy(294,16): Error: member R does not exist in class B
Modules0.dfy(294,6): Error: expected method call, found expression
+Modules0.dfy(317,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
+Modules0.dfy(321,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
+Modules0.dfy(322,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)
+Modules0.dfy(323,11): Error: Undeclared module name: Wazzup (did you forget a module import?)
+Modules0.dfy(324,17): Error: Undeclared class name Edon in module Q_Imp
+Modules0.dfy(326,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
+Modules0.dfy(327,30): Error: member Create does not exist in class Klassy
Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts
Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts
Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts
Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts
Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context
Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context
-30 resolution/type errors detected in Modules0.dfy
+37 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(74,16): Error: assertion violation
@@ -758,7 +767,7 @@ Modules1.dfy(58,3): Error: failure to decrease termination measure Execution trace:
(0,0): anon0
-Dafny program verifier finished with 19 verified, 5 errors
+Dafny program verifier finished with 22 verified, 5 errors
-------------------- BadFunction.dfy --------------------
BadFunction.dfy(6,3): Error: failure to decrease termination measure
@@ -801,14 +810,7 @@ Basics.dfy(100,16): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon10_Then
-Basics.dfy(113,12): Error: left-hand sides 0 and 1 may refer to the same location
-Execution trace:
- (0,0): anon0
- (0,0): anon3
- (0,0): anon11_Else
- (0,0): anon6
- (0,0): anon12_Then
-Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(119,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value
Execution trace:
(0,0): anon0
(0,0): anon10_Then
@@ -817,7 +819,7 @@ Execution trace: (0,0): anon6
(0,0): anon12_Then
(0,0): anon9
-Basics.dfy(133,10): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(133,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
Execution trace:
(0,0): anon0
Basics.dfy(145,19): Error: assertion violation
@@ -848,8 +850,11 @@ Execution trace: (0,0): anon13_Then
(0,0): anon8
(0,0): anon14_Then
+Basics.dfy(226,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 19 verified, 11 errors
+Dafny program verifier finished with 32 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
@@ -1567,6 +1572,11 @@ Execution trace: Dafny program verifier finished with 30 verified, 2 errors
+-------------------- LiberalEquality.dfy --------------------
+LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)
+LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<int> and array<bool>)
+2 resolution/type errors detected in LiberalEquality.dfy
+
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
Execution trace:
@@ -1708,7 +1718,7 @@ Execution trace: (0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-SmallTests.dfy(584,18): Error: target object may be null
+SmallTests.dfy(584,25): Error: target object may be null
Execution trace:
(0,0): anon0
SmallTests.dfy(597,10): Error: assertion violation
@@ -1856,7 +1866,7 @@ Execution trace: (0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-out.tmp.dfy(530,18): Error: target object may be null
+out.tmp.dfy(530,25): Error: target object may be null
Execution trace:
(0,0): anon0
out.tmp.dfy(543,10): Error: assertion violation
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 6aa1e34d..7fca7199 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -110,7 +110,7 @@ method TestMulti(m: Multi, p: Multi) assert p.x == 300;
if (*) {
p.x, m.y := 10, 10;
- p.x, m.x := 8, 8; // error: duplicate assignment (since m and p may be the same)
+ p.x, m.x := 8, 8;
}
var a, b := new int[20], new int[30];
@@ -184,4 +184,59 @@ method EuclideanTest(a: int, b: int) assert 0 <= r < abs(b);
assert a == b * q + r;
assert (a/b) * b + a % b == a;
-}
\ No newline at end of file +}
+
+method havocInMultiassignment()
+{
+ var i: nat, j: nat;
+ i, j := *, 3;
+ assert 0 <= i;
+}
+
+method m()
+{
+ var i: int, j: int;
+ i, j := 3, 6;
+ i, i := 3, 3;
+}
+
+method swap(a: array<int>, i: nat, j: nat)
+ requires a != null && 0 <= i < a.Length && 0 <= j < a.Length;
+ modifies a;
+{
+ a[i], a[j] := a[j], a[i];
+}
+
+class CC {
+ var x : int;
+ var y : int;
+}
+
+method notQuiteSwap(c: CC, d: CC)
+ requires c != null && d != null;
+ modifies c,d;
+{
+ c.x, d.x := c.x, c.x;
+}
+
+method notQuiteSwap2(c: CC, d: CC)
+ requires c != null && d != null;
+ modifies c,d;
+{
+ c.x, d.x := d.x, c.y; // BAD: c and d could be the same.
+}
+
+method OKNowIt'sSwapAgain(c: CC, d: CC)
+ requires c != null && d != null;
+ modifies c,d;
+{
+ c.x, d.x := d.x, c.x;
+}
+
+method notQuiteSwap3(c: CC, d: CC)
+ requires c != null && d != null && c != d;
+ modifies c,d;
+{
+ c.x, d.x := 4, c.y;
+ c.x, c.y := 3, c.y;
+}
diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy new file mode 100644 index 00000000..3dc52c80 --- /dev/null +++ b/Test/dafny0/LiberalEquality.dfy @@ -0,0 +1,55 @@ +
+class Array<T>
+{
+ var Length: nat;
+}
+
+class Test<T> {
+ var a: Array<int>;
+ var b: Array<T>;
+ predicate valid()
+ reads this, a, b;
+ {
+ a != null && b != null && a != b && a.Length == b.Length
+ }
+}
+
+method m1<T, U>(t: T, u: U)
+ requires t != u;
+{
+
+}
+
+method m2<T>(t: array<T>, a: array<int>)
+ requires t != null && a != null && t != a && t.Length == a.Length;
+{
+
+}
+
+
+class Weird<T, U, V>
+{
+
+}
+
+
+method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)
+ requires a == b; // Bad: second parameter can't be both bool and int.
+{
+
+}
+
+
+method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)
+ requires a == b;
+{
+
+}
+
+
+// Just to make sure nothing went wrong.
+method m5(a: array<int>, b: array<bool>)
+ requires a == b; // Bad: never equal
+{
+
+}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index b171a9c9..cc66c3c1 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -301,3 +301,31 @@ module Local imports NonLocalA, NonLocalB { method Q() { }
}
}
+
+// ------ qualified type names ----------------------------------
+
+module Q_Imp {
+ class Node { }
+ datatype List<T> = Nil | Cons(T, List);
+ class Klassy {
+ method Init()
+ }
+}
+
+module Q_M imports Q_Imp {
+ method MyMethod(root: Q_Imp.Node, S: set<Node>)
+ requires root in S; // error: the element type of S does not agree with the type of root
+ {
+ var i := new Q_Imp.Node;
+ var j := new Node;
+ assert i != j; // error: i and j have different types
+ var k: LongLostModule.Node; // error: undeclared module
+ var l: Wazzup.WazzupA; // error: undeclared module (it has not been imported)
+ var m: Q_Imp.Edon; // error: undeclared class in module Q_Imp
+ var n: Q_Imp.List;
+ var o := new Q_Imp.List; // error: not a class declared in module Q_Imp
+ var p := new Q_Imp.Klassy.Create(); // error: Create is not a method
+ var q := new Q_Imp.Klassy.Init();
+ }
+ class Node { }
+}
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index 5e2d0fff..e8a88749 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -89,3 +89,23 @@ module B_Visibility imports A_Visibility { }
}
}
+
+// ------ qualified type names ----------------------------------
+
+module Q_Imp {
+ class Node { }
+ class Klassy {
+ method Init()
+ }
+}
+
+module Q_M imports Q_Imp {
+ method MyMethod(root: Q_Imp.Node, S: set<Q_Imp.Node>)
+ requires root in S;
+ {
+ var i := new Q_Imp.Node;
+ var j := new Node;
+ assert i != j; // fine
+ var q := new Q_Imp.Klassy.Init();
+ }
+}
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index ab711d02..f260edb5 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -103,6 +103,6 @@ method M1() { method M2() {
var a := new int[100];
parallel (x | 0 <= x < 100) {
- a[x] :| a[x] > 0; // error: not allowed to update heap location in a parallel statement with a(n implicit) assume
+ a[x] :| assume a[x] > 0; // error: not allowed to update heap location in a parallel statement with an assume
}
}
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy index f8569b3a..146129b5 100644 --- a/Test/dafny0/Predicates.dfy +++ b/Test/dafny0/Predicates.dfy @@ -79,7 +79,7 @@ module Tight refines Loose { }
module UnawareClient imports Loose {
- method Main() {
+ method Main0() {
var n := new MyNumber.Init();
assert n.N == 0; // error: this is not known
n.Inc();
@@ -90,7 +90,7 @@ module UnawareClient imports Loose { }
module AwareClient imports Tight {
- method Main() {
+ method Main1() {
var n := new MyNumber.Init();
assert n.N == 0;
n.Inc();
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 4d219cd3..e8b618d7 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -542,21 +542,21 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int) ensures x == a && y == b;
{
if (*) {
- x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;
+ x, y :| assume a <= x < a + 1 && b + a <= y + a && y <= b;
} else {
- var xx, yy :| a <= xx < a + 1 && b + a <= yy + a && yy <= b;
+ var xx, yy :| assume a <= xx < a + 1 && b + a <= yy + a && yy <= b;
x, y := xx, yy;
}
}
method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)
{
- var k :| 0 <= k < a - b; // this acts like an 'assume 0 < a - b;'
+ var k :| assume 0 <= k < a - b; // this acts like an 'assume 0 < a - b;'
assert b < a;
- k :| k == old(2*k); // note, the 'old' has no effect on local variables like k
+ k :| assume k == old(2*k); // note, the 'old' has no effect on local variables like k
assert k == 0;
var S := {2, 4, 7};
- var T :| T <= S;
+ var T :| assume T <= S;
assert 3 !in T;
assert T == {}; // error: T may be larger
}
@@ -568,38 +568,38 @@ method AssignSuchThat2(i: int, j: int, ghost S: set<Node>) var a := new int[25];
var t;
if (0 <= i < j < 25) {
- a[i], t, a[j], n.next, n :| true;
+ a[i], t, a[j], n.next, n :| assume true;
}
if (n != null && n.next != null) {
assume n in S && n.next in S;
- n.next.next, n.next :| n != null && n.next != null && n.next.next == n.next; // error: n.next may equal n (thus aliasing n.next.next and n.next)
+ n.next.next, n.next :| assume n != null && n.next != null && n.next.next == n.next; // error: n.next may equal n (thus aliasing n.next.next and n.next)
} else if (0 <= i < 25 && 0 <= j < 25) {
- t, a[i], a[j] :| t < a[i] < a[j]; // error: i may equal j (thus aliasing a[i] and a[j])
+ t, a[i], a[j] :| assume t < a[i] < a[j]; // error: i may equal j (thus aliasing a[i] and a[j])
}
}
method AssignSuchThat3()
{
var n := new Node;
- n, n.next :| n.next == n; // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)
+ n, n.next :| assume n.next == n; // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)
}
method AssignSuchThat4()
{
var n := new Node;
- n, n.next :| n != null && n.next == n; // that's the ticket
+ n, n.next :| assume n != null && n.next == n; // that's the ticket
}
method AssignSuchThat5()
{
var n := new Node;
- n :| fresh(n); // fine
+ n :| assume fresh(n); // fine
assert false; // error
}
method AssignSuchThat6()
{
var n: Node;
- n :| n != null && fresh(n); // there is no non-null fresh object, so this amounts to 'assume false;'
+ n :| assume n != null && fresh(n); // there is no non-null fresh object, so this amounts to 'assume false;'
assert false; // no problemo
}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 29274381..8434f06c 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -92,3 +92,28 @@ method K(s: set<nat>) { // error: not allowed to instantiate 'set' with 'nat' var b := new nat[100,200]; // error: not allowed the type array2<nat>
}
+// --------------------- more ghost tests, for assign-such-that statements
+
+method M()
+{
+ ghost var b: bool;
+ ghost var k: int, l: int;
+ var m: int;
+
+ // These three statements are allowed by the resolver, but the compiler will complain
+ // if it ever gets them.
+ k :| k < 10;
+ k, m :| 0 <= k < m;
+ m :| m < 10;
+
+ // Because of the ghost guard, these 'if' statements are ghost contexts, so only
+ // assignments to ghosts are allowed.
+ if (b) {
+ k :| k < 10; // should be allowed
+ k, l :| 0 <= k < l; // ditto
+ }
+ if (b) {
+ m :| m < 10; // error: not allowed in ghost context
+ k, m :| 0 <= k < m; // error: not allowed in ghost context
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index e4c134f6..ac7c8aed 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -3,7 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
for %%f in (Simple.dfy) do (
echo.
@@ -22,7 +21,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
- Predicates.dfy Skeletons.dfy Maps.dfy) do (
+ Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 9ed6d75a..7c7719ee 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -1,8 +1,4 @@ --------------------- BQueue.bpl --------------------
-
-Boogie program verifier finished with 8 verified, 0 errors
-
-------------------- Queue.dfy --------------------
Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 1f5d78df..d098d753 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -3,14 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
-
-for %%f in (BQueue.bpl) do (
- echo.
- echo -------------------- %%f --------------------
- %BPLEXE% %* %%f
-)
for %%f in (Queue.dfy PriorityQueue.dfy
ExtensibleArray.dfy ExtensibleArrayAuto.dfy
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 381b9cb1..9c37549e 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -31,6 +31,22 @@ Dafny program verifier finished with 23 verified, 0 errors Dafny program verifier finished with 5 verified, 0 errors
+-------------------- TreeFill.dfy --------------------
+
+Dafny program verifier finished with 3 verified, 0 errors
+
+-------------------- TuringFactorial.dfy --------------------
+
+Dafny program verifier finished with 3 verified, 0 errors
+
-------------------- StoreAndRetrieve.dfy --------------------
Dafny program verifier finished with 22 verified, 0 errors
+
+-------------------- MajorityVote.dfy --------------------
+
+Dafny program verifier finished with 11 verified, 0 errors
+
+-------------------- SegmentSum.dfy --------------------
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy new file mode 100644 index 00000000..a7512486 --- /dev/null +++ b/Test/dafny2/MajorityVote.dfy @@ -0,0 +1,171 @@ +// Rustan Leino, June 2012.
+// This file verifies an algorithm, due to Boyer and Moore, that finds the majority choice
+// among a sequence of votes, see http://www.cs.utexas.edu/~moore/best-ideas/mjrty/.
+// Actually, this algorithm is a slight variation on theirs, but the general idea for why
+// it is correct is the same. In the Boyer and Moore algorithm, the loop counter is advanced
+// by exactly 1 each iteration, which means that there may or may not be a "current leader".
+// In my program below, I had instead written the loop invariant to say there is always a
+// "current leader", which requires the loop index sometimes to skip a value.
+//
+// This file has two versions of the algorithm. In the first version, the given sequence
+// of votes is assumed to have a (strict) majority choice, meaning that strictly more than
+// 50% of the votes are for one candidate. It is convenient to have a name for the majority
+// choice, in order to talk about it in specifications. The easiest way to do this in
+// Dafny is probably to introduce a ghost parameter with the given properties. That's what
+// the algorithm does, see parameter K. The postcondition is thus to output the value of
+// K, which is done in the non-ghost out-parameter k.
+// The proof of the algorithm requires two lemmas. These lemmas are proved automatically
+// by Dafny's induction tactic.
+//
+// In the second version of the program, the main method does not assume there is a majority
+// choice. Rather, it eseentially uses the first algorithm and then checks if what it
+// returns really is a majority choice. To do this, the specification of the first algorithm
+// needs to be changed slightly to accommodate the possibility that there is no majority
+// choice. That change in specification is also reflected in the loop invariant. Moreover,
+// the algorithm itself now needs to extra 'if' statements to see if the entire sequence
+// has been searched through. (This extra 'if' is essentially already handled by Boyer and
+// Moore's algorithm, because it increments the loop index by 1 each iteration and therefore
+// already has a special case for the case of running out of sequence elements without a
+// current leader.)
+// The calling harness, DetermineElection, somewhat existentially comes up with the majority
+// choice, if there is such a choice, and then passes in that choice as the ghost parameter K
+// to the main algorithm. Neat, huh?
+
+// Advanced remark:
+// There is a subtle situation in the verification of DetermineElection. Suppose the type
+// parameter Candidate denotes some type whose instances depend on which object are
+// allocated. For example, if Candidate is some class type, then more candidates can come
+// into being by object allocations (using "new"). What does the quantification of
+// candidates "c" in the postcondition of DetermineElection now mean--all candidates that
+// existed in the pre-state or (the possibly larger set of) all candidates that exist in the
+// post-state? (It means the latter.) And if there does not exist a candidate in majority
+// in the pre-state, could there be a (newly created) candidate in majority in the post-state?
+// This will require some proof. The simplest argument seems to be that even if more candidates
+// are created during the course of DetermineElection, such candidates cannot possibly
+// be in majority in the sequence "a", since "a" can only contain candidates that were already
+// created in the pre-state. This property is easily specified by adding a postcondition
+// to the Count function. Alternatively, one could have added the antecedent "c in a" or
+// "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.
+
+function method Count<T>(a: seq<T>, s: int, t: int, x: T): int
+ requires 0 <= s <= t <= |a|;
+ ensures Count(a, s, t, x) == 0 || x in a;
+{
+ if s == t then 0 else
+ Count(a, s, t-1, x) + if a[t-1] == x then 1 else 0
+}
+
+// Here is the first version of the algorithm, the one that assumes there is a majority choice.
+
+method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)
+ requires 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
+ ensures k == K; // find K
+{
+ k := a[0];
+ var n, c, s := 1, 1, 0;
+ while (n < |a|)
+ invariant 0 <= s <= n <= |a|;
+ invariant 2 * Count(a, s, |a|, K) > |a| - s; // K has majority among a[s..]
+ invariant 2 * Count(a, s, n, k) > n - s; // k has majority among a[s..n]
+ invariant c == Count(a, s, n, k);
+ {
+ if (a[n] == k) {
+ n, c := n + 1, c + 1;
+ } else if (2 * c > n + 1 - s) {
+ n := n + 1;
+ } else {
+ n := n + 1;
+ // We have 2*Count(a, s, n, k) == n-s, and thus the following lemma
+ // lets us conclude 2*Count(a, s, n, K) <= n-s.
+ Lemma_Unique(a, s, n, K, k);
+ // We also have 2*Count(a, s, |a|, K) > |a|-s, and the following lemma
+ // tells us Count(a, s, |a|, K) == Count(a, s, n, K) + Count(a, n, |a|, K),
+ // and thus we can conclude 2*Count(a, n, |a|, K) > |a|-n.
+ Lemma_Split(a, s, n, |a|, K);
+ k, n, c, s := a[n], n + 1, 1, n;
+ }
+ }
+ Lemma_Unique(a, s, |a|, K, k); // both k and K have a majority, so K == k
+}
+
+// ------------------------------------------------------------------------------
+
+// Here is the second version of the program, the one that also computes whether or not
+// there is a majority choice.
+
+method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)
+ ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;
+ ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;
+{
+ ghost var b := exists c :: 2 * Count(a, 0, |a|, c) > |a|;
+ ghost var w :| b ==> 2 * Count(a, 0, |a|, w) > |a|;
+ cand := SearchForWinner(a, b, w);
+ return 2 * Count(a, 0, |a|, cand) > |a|, cand;
+}
+
+// The difference between SearchForWinner for FindWinner above are the occurrences of the
+// antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"
+// statement.
+
+method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)
+ requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
+ ensures hasWinner ==> k == K; // find K
+{
+ if (|a| == 0) { return; }
+ k := a[0];
+ var n, c, s := 1, 1, 0;
+ while (n < |a|)
+ invariant 0 <= s <= n <= |a|;
+ invariant hasWinner ==> 2 * Count(a, s, |a|, K) > |a| - s; // K has majority among a[s..]
+ invariant 2 * Count(a, s, n, k) > n - s; // k has majority among a[s..n]
+ invariant c == Count(a, s, n, k);
+ {
+ if (a[n] == k) {
+ n, c := n + 1, c + 1;
+ } else if (2 * c > n + 1 - s) {
+ n := n + 1;
+ } else {
+ n := n + 1;
+ // We have 2*Count(a, s, n, k) == n-s, and thus the following lemma
+ // lets us conclude 2*Count(a, s, n, K) <= n-s.
+ Lemma_Unique(a, s, n, K, k);
+ // We also have 2*Count(a, s, |a|, K) > |a|-s, and the following lemma
+ // tells us Count(a, s, |a|, K) == Count(a, s, n, K) + Count(a, n, |a|, K),
+ // and thus we can conclude 2*Count(a, n, |a|, K) > |a|-n.
+ Lemma_Split(a, s, n, |a|, K);
+ if (|a| == n) { return; }
+ k, n, c, s := a[n], n + 1, 1, n;
+ }
+ }
+ Lemma_Unique(a, s, |a|, K, k); // both k and K have a majority, so K == k
+}
+
+// ------------------------------------------------------------------------------
+
+// Here are two lemmas about Count that are used in the methods above.
+
+ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)
+ requires 0 <= s <= t <= u <= |a|;
+ ensures Count(a, s, t, x) + Count(a, t, u, x) == Count(a, s, u, x);
+{
+ /* The postcondition of this method is proved automatically via Dafny's
+ induction tactic. But if a manual proof had to be provided, it would
+ look like this:
+ if (s != t) {
+ Lemma_Split(a, s, t-1, u, x);
+ }
+ */
+}
+
+ghost method Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)
+ requires 0 <= s <= t <= |a|;
+ ensures x != y ==> Count(a, s, t, x) + Count(a, s, t, y) <= t - s;
+{
+ /* The postcondition of this method is proved automatically via Dafny's
+ induction tactic. But if a manual proof had to be provided, it would
+ look like this:
+ if (s != t) {
+ Lemma_Unique(a, s, t-1, x, y);
+ }
+ */
+}
diff --git a/Test/dafny2/SegmentSum.dfy b/Test/dafny2/SegmentSum.dfy new file mode 100644 index 00000000..dc67162b --- /dev/null +++ b/Test/dafny2/SegmentSum.dfy @@ -0,0 +1,29 @@ +function Sum(a: seq<int>, s: int, t: int): int
+ requires 0 <= s <= t <= |a|;
+{
+ if s == t then 0 else Sum(a, s, t-1) + a[t-1]
+}
+
+method MaxSegSum(a: seq<int>) returns (k: int, m: int)
+ ensures 0 <= k <= m <= |a|;
+ ensures forall p,q :: 0 <= p <= q <= |a| ==> Sum(a, p, q) <= Sum(a, k, m);
+{
+ k, m := 0, 0;
+ var s := 0; // invariant s == Sum(a, k, m)
+ var n := 0;
+ var c, t := 0, 0; // invariant t == Sum(a, c, n)
+ while (n < |a|)
+ invariant n <= |a|;
+ invariant 0 <= c <= n && t == Sum(a, c, n);
+ invariant forall b :: 0 <= b <= n ==> Sum(a, b, n) <= Sum(a, c, n);
+ invariant 0 <= k <= m <= n && s == Sum(a, k, m);
+ invariant forall p,q :: 0 <= p <= q <= n ==> Sum(a, p, q) <= Sum(a, k, m);
+ {
+ t, n := t + a[n], n + 1;
+ if (t < 0) {
+ c, t := n, 0;
+ } else if (s < t) {
+ k, m, s := c, n, t;
+ }
+ }
+}
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy index ea26a234..15c82d65 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -1,4 +1,4 @@ -module A imports Library {
+ghost module A imports Library {
class {:autocontracts} StoreAndRetrieve<Thing> {
ghost var Contents: set<Thing>;
predicate Valid
diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy new file mode 100644 index 00000000..f7e2cc89 --- /dev/null +++ b/Test/dafny2/TreeFill.dfy @@ -0,0 +1,27 @@ +datatype Tree<T> = Null | Node(Tree, T, Tree);
+
+function Contains<T>(t: Tree, v: T): bool
+{
+ match t
+ case Null => false
+ case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)
+}
+
+method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)
+ requires a != null && 0 <= start <= a.Length;
+ modifies a;
+ ensures start <= end <= a.Length;
+ ensures forall i :: 0 <= i < start ==> a[i] == old(a[i]);
+ ensures forall i :: start <= i < end ==> Contains(t, a[i]);
+{
+ match (t) {
+ case Null =>
+ end := start;
+ case Node(left, x, right) =>
+ end := Fill(left, a, start);
+ if (end < a.Length) {
+ a[end] := x;
+ end := Fill(right, a, end + 1);
+ }
+ }
+}
diff --git a/Test/dafny2/TuringFactorial.dfy b/Test/dafny2/TuringFactorial.dfy new file mode 100644 index 00000000..585c998e --- /dev/null +++ b/Test/dafny2/TuringFactorial.dfy @@ -0,0 +1,26 @@ +function Factorial(n: nat): nat
+{
+ if n == 0 then 1 else n * Factorial(n-1)
+}
+
+method ComputeFactorial(n: int) returns (u: int)
+ requires 1 <= n;
+ ensures u == Factorial(n);
+{
+ var r := 1;
+ u := 1;
+ while (r < n)
+ invariant r <= n;
+ invariant u == Factorial(r);
+ {
+ var v, s := u, 1;
+ while (s < r + 1)
+ invariant s <= r + 1;
+ invariant v == Factorial(r) && u == s * Factorial(r);
+ {
+ u := u + v;
+ s := s + 1;
+ }
+ r := r + 1;
+ }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index a4796939..b68ba251 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -3,7 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
REM soon again: SnapshotableTrees.dfy
for %%f in (
@@ -14,8 +13,8 @@ for %%f in ( COST-verif-comp-2011-2-MaxTree-datatype.dfy
COST-verif-comp-2011-3-TwoDuplicates.dfy
COST-verif-comp-2011-4-FloydCycleDetect.dfy
- Intervals.dfy
- StoreAndRetrieve.dfy
+ Intervals.dfy TreeFill.dfy TuringFactorial.dfy
+ StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy
) do (
echo.
echo -------------------- %%f --------------------
diff --git a/Test/dafnyRuntimeChecking/Answer b/Test/dafnyRuntimeChecking/Answer index 6bda12af..0cc946ab 100644 --- a/Test/dafnyRuntimeChecking/Answer +++ b/Test/dafnyRuntimeChecking/Answer @@ -7,10 +7,11 @@ Rewrote assembly into AssumeStmt0.exe using System.Diagnostics.Contracts;
using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
@@ -589,13 +590,13 @@ namespace Dafny { }
}
-public class @_default {
+public class @__default {
public void @Main()
{
Contract.Assume((new BigInteger(2)) < (new BigInteger(10)));
}
public static void Main(string[] args) {
- @_default b = new @_default();
+ @__default b = new @__default();
b.Main();
}
}
@@ -608,10 +609,11 @@ Rewrote assembly into AssumeStmt1.exe using System.Diagnostics.Contracts;
using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
@@ -1190,13 +1192,13 @@ namespace Dafny { }
}
-public class @_default {
+public class @__default {
public void @Main()
{
Contract.Assume((new BigInteger(10)) < (new BigInteger(2)));
}
public static void Main(string[] args) {
- @_default b = new @_default();
+ @__default b = new @__default();
b.Main();
}
}
@@ -1209,10 +1211,11 @@ Rewrote assembly into AssertStmt0.exe using System.Diagnostics.Contracts;
using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
@@ -1791,13 +1794,13 @@ namespace Dafny { }
}
-public class @_default {
+public class @__default {
public void @Main()
{
Contract.Assert((new BigInteger(2)) < (new BigInteger(10)));
}
public static void Main(string[] args) {
- @_default b = new @_default();
+ @__default b = new @__default();
b.Main();
}
}
@@ -1810,10 +1813,11 @@ Rewrote assembly into AssertStmt1.exe using System.Diagnostics.Contracts;
using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
@@ -2392,13 +2396,13 @@ namespace Dafny { }
}
-public class @_default {
+public class @__default {
public void @Main()
{
Contract.Assert((new BigInteger(10)) < (new BigInteger(2)));
}
public static void Main(string[] args) {
- @_default b = new @_default();
+ @__default b = new @__default();
b.Main();
}
}
@@ -2411,10 +2415,11 @@ Rewrote assembly into Precondition0.exe using System.Diagnostics.Contracts;
using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
@@ -2993,13 +2998,13 @@ namespace Dafny { }
}
-public class @_default {
+public class @__default {
public void @Main()
{
Contract.Requires(true);
}
public static void Main(string[] args) {
- @_default b = new @_default();
+ @__default b = new @__default();
b.Main();
}
}
@@ -3012,10 +3017,11 @@ Rewrote assembly into Precondition1.exe using System.Diagnostics.Contracts;
using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
@@ -3594,7 +3600,7 @@ namespace Dafny { }
}
-public class @_default {
+public class @__default {
public void @foo(BigInteger @x, BigInteger @y)
{
Contract.Requires((new BigInteger(0)) <= (@x));
@@ -3605,7 +3611,7 @@ public class @_default { (this).@foo(new BigInteger(2), (new BigInteger(0)) - (new BigInteger(7)));
}
public static void Main(string[] args) {
- @_default b = new @_default();
+ @__default b = new @__default();
b.Main();
}
}
@@ -3618,10 +3624,11 @@ Rewrote assembly into Postcondition0.exe using System.Diagnostics.Contracts;
using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
@@ -4200,13 +4207,13 @@ namespace Dafny { }
}
-public class @_default {
+public class @__default {
public void @Main()
{
Contract.Ensures(true);
}
public static void Main(string[] args) {
- @_default b = new @_default();
+ @__default b = new @__default();
b.Main();
}
}
@@ -4219,10 +4226,11 @@ Rewrote assembly into Postcondition1.exe using System.Diagnostics.Contracts;
using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
@@ -4801,7 +4809,7 @@ namespace Dafny { }
}
-public class @_default {
+public class @__default {
public BigInteger @x = new BigInteger(0);
public BigInteger @y = new BigInteger(0);
public void @Main()
@@ -4812,7 +4820,7 @@ public class @_default { (this).@y = (new BigInteger(0)) - (new BigInteger(7));
}
public static void Main(string[] args) {
- @_default b = new @_default();
+ @__default b = new @__default();
b.Main();
}
}
diff --git a/Test/dafnytests.txt b/Test/dafnytests.txt index 74f055ab..ca40465e 100644 --- a/Test/dafnytests.txt +++ b/Test/dafnytests.txt @@ -2,7 +2,7 @@ dafny0 Use Dafny functionality tests dafny1 Use Various Dafny examples
dafny2 Use More Dafny examples
dafnyRuntimeChecking Use Dafny runtime checking tests
-dafnyCompiler Use Dafny compiler tests
+dafnyCompiler Postpone Dafny compiler tests
VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
diff --git a/Test/test15/Answer b/Test/test15/Answer index 56c247c2..04a94759 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -144,7 +144,7 @@ type -> { T@U!val!0 -> T@T!val!4
T@U!val!1 -> T@T!val!2
T@U!val!2 -> T@T!val!3
- T@U!val!3 -> T@T!val!0
+ -2 -> T@T!val!0
else -> T@T!val!4
}
Ctor -> {
@@ -162,12 +162,12 @@ Ctor -> { 6 5 -> true
else -> true
}
-MapType0Select -> {
- T@U!val!0 T@U!val!1 T@U!val!2 -> T@U!val!3
- else -> T@U!val!3
+[3] -> {
+ T@U!val!0 T@U!val!1 T@U!val!2 -> -2
+ else -> -2
}
U_2_int -> {
- T@U!val!3 -> -2
+ -2 -> -2
else -> -2
}
MapType0TypeInv1 -> {
@@ -187,8 +187,8 @@ MapType0TypeInv0 -> { else -> T@T!val!2
}
int_2_U -> {
- -2 -> T@U!val!3
- else -> T@U!val!3
+ -2 -> -2
+ else -> -2
}
*** STATE <initial>
Heap -> T@U!val!0
diff --git a/Test/textbook/Answer b/Test/textbook/Answer index dace3eb3..42e41c5a 100644 --- a/Test/textbook/Answer +++ b/Test/textbook/Answer @@ -22,3 +22,7 @@ Boogie program verifier finished with 1 verified, 0 errors ------------------------------ TuringFactorial.bpl ---------------------
Boogie program verifier finished with 1 verified, 0 errors
+
+------------------------------ BQueue.bpl ---------------------
+
+Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Test/dafny1/BQueue.bpl b/Test/textbook/BQueue.bpl index 77f1efb3..77f1efb3 100644 --- a/Test/dafny1/BQueue.bpl +++ b/Test/textbook/BQueue.bpl diff --git a/Test/textbook/runtest.bat b/Test/textbook/runtest.bat index b747312d..f43e54d9 100644 --- a/Test/textbook/runtest.bat +++ b/Test/textbook/runtest.bat @@ -7,7 +7,7 @@ REM ====================== REM ====================== Examples written in Boogie
REM ======================
for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl McCarthy-91.bpl
- TuringFactorial.bpl) do (
+ TuringFactorial.bpl BQueue.bpl) do (
echo.
echo ------------------------------ %%f ---------------------
%BPLEXE% %* %%f
diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy index e56a8317..3e5a95ef 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -11,10 +11,10 @@ class LazyInitArray<T> { reads this, a, b, c;
{
a != null && b != null && c != null &&
- a.Length == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'
+ a.Length == |Contents| &&
b.Length == |Contents| &&
c.Length == |Contents| &&
- b != c &&
+ b != c && a != b && a != c &&
0 <= n && n <= c.Length &&
(forall i :: 0 <= i && i < |Contents| ==>
Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&
@@ -41,7 +41,7 @@ class LazyInitArray<T> { ensures |Contents| == N && Zero == zero;
ensures (forall x :: x in Contents ==> x == zero);
{
- a := new T[N+1];
+ a := new T[N];
b := new int[N];
c := new int[N];
n := 0;
diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat index efe7b3d5..cd047d39 100644 --- a/Test/vacid0/runtest.bat +++ b/Test/vacid0/runtest.bat @@ -3,8 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set BPLEXE=%BOOGIEDIR%\Boogie.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (
echo.
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat index 770f41dc..7f7c9b9f 100644 --- a/Test/vstte2012/runtest.bat +++ b/Test/vstte2012/runtest.bat @@ -3,7 +3,6 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
for %%f in (
Two-Way-Sort.dfy
|