diff options
| author |  chmaria <unknown> | 2012-06-18 15:00:48 +0200 |
|---|---|---|
| committer | chmaria <unknown> | 2012-06-18 15:00:48 +0200 |
| commit | 1d8777cd2e431dc0d504727bda2081c7522e0e51 (patch) | |
| tree | 05608c0508ddf8072bee43c3bc4153d3c317f4d0 /Test/vacid0 | |
| parent | 0eb394f362b391b123825ec47c68eac0b8adac8f (diff) | |
| parent | 28d1c7ea6a32350df3379ab5991fd7407cc1b9b7 (diff) | |
Merged with default.
Diffstat (limited to 'Test/vacid0')
| -rw-r--r-- | Test/vacid0/LazyInitArray.dfy | 6 | ||||
| -rw-r--r-- | Test/vacid0/runtest.bat | 2 |
2 files changed, 3 insertions, 5 deletions
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.
|