summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-06-14 13:34:20 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-06-14 13:34:20 -0700
commit904420332a82fb0750fff2a34f70fe4e8868543c (patch)
treedfd67a167bf679ef8f95c1c287f2f31dcc19bf90
parentde2e6cad0c25388aca044d42ad3cbd1a873f7637 (diff)
Dafny: cleaned up test scripts a little
-rw-r--r--Test/VSComp2010/runtest.bat2
-rw-r--r--Test/VSI-Benchmarks/runtest.bat2
-rw-r--r--Test/dafny0/runtest.bat1
-rw-r--r--Test/dafny1/Answer4
-rw-r--r--Test/dafny1/runtest.bat8
-rw-r--r--Test/dafny2/Answer4
-rw-r--r--Test/dafny2/TuringFactorial.dfy26
-rw-r--r--Test/dafny2/runtest.bat3
-rw-r--r--Test/textbook/Answer4
-rw-r--r--Test/textbook/BQueue.bpl (renamed from Test/dafny1/BQueue.bpl)0
-rw-r--r--Test/textbook/runtest.bat2
-rw-r--r--Test/vacid0/runtest.bat2
-rw-r--r--Test/vstte2012/runtest.bat1
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