Dafny: cleaned up test scripts a little

13 files changed, 36 insertions, 23 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/runtest.bat b/Test/dafny0/runtest.bat
index 0da7fe3e..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.

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 93524dfa..9c37549e 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -35,6 +35,10 @@ Dafny program verifier finished with 5 verified, 0 errors
 

 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

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 794b7908..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,7 +13,7 @@ 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 TreeFill.dfy

+    Intervals.dfy TreeFill.dfy TuringFactorial.dfy

     StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy

   ) do (

   echo.

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/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