Merge

3 files changed, 10 insertions, 74 deletions

diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer
deleted file mode 100644
index 14986a59..00000000
--- a/Test/dafny4/Answer
+++ /dev/null
@@ -1,43 +0,0 @@
-

--------------------- CoqArt-InsertionSort.dfy --------------------

-

-Dafny program verifier finished with 36 verified, 0 errors

-

--------------------- GHC-MergeSort.dfy --------------------

-

-Dafny program verifier finished with 83 verified, 0 errors

-

--------------------- Fstar-QuickSort.dfy --------------------

-

-Dafny program verifier finished with 6 verified, 0 errors

-

--------------------- Primes.dfy --------------------

-

-Dafny program verifier finished with 24 verified, 0 errors

-

--------------------- KozenSilva.dfy --------------------

-

-Dafny program verifier finished with 47 verified, 0 errors

-

--------------------- SoftwareFoundations-Basics.dfy --------------------

-SoftwareFoundations-Basics.dfy(41,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 82 verified, 1 error

-

--------------------- NumberRepresentations.dfy --------------------

-

-Dafny program verifier finished with 33 verified, 0 errors

-

--------------------- Circ.dfy --------------------

-

-Dafny program verifier finished with 16 verified, 0 errors

-

--------------------- ACL2-extractor.dfy --------------------

-

-Dafny program verifier finished with 33 verified, 0 errors

-

--------------------- ClassRefinement.dfy --------------------

-

-Dafny program verifier finished with 18 verified, 0 errors

diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
index d7c142ee..5b7f3a0f 100644
--- a/Test/dafny4/NumberRepresentations.dfy
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -8,6 +8,7 @@
 

 function eval(digits: seq<int>, base: int): int

   requires 2 <= base;

+  decreases digits;  // see comment in test_eval()

 {

   if |digits| == 0 then 0 else digits[0] + base * eval(digits[1..], base)

 }

@@ -16,36 +17,21 @@ lemma test_eval()
 {

   assert forall base :: 2 <= base ==> eval([], base) == 0;

   assert forall base :: 2 <= base ==> eval([0], base) == 0;

-  forall base | 2 <= base {

-    calc {

-      eval([0, 0], base);

-      0;

-    }

-  }

 

-  calc {

-    eval([3, 2], 10);

-    3 + 10 * eval([2], 10);

-    23;

-  }

+  // To prove this automatically, it is necessary that the Lit axiom is sensitive only to the

+  // 'digits' argument being a literal.  Hence, the explicit 'decreases digits' clause on the

+  // 'eval' function.

+  assert forall base :: 2 <= base ==> eval([0, 0], base) == 0;

+

+  assert eval([3, 2], 10) == 23;

+

   var oct, dec := 8, 10;

-  calc {

-    eval([1, 3], oct);

-    1 + oct * eval([3], oct);

-    5 + dec * eval([2], dec);

-    eval([5, 2], dec);

-  }

+  assert eval([1, 3], oct) == eval([5, 2], dec);

 

   assert eval([29], 420) == 29;

   assert eval([29], 8) == 29;

 

-  calc {

-    eval([-2, 1, -3], 5);

-    -2 + 5 * eval([1, -3], 5);

-    -2 + 5 * 1 + 25 * eval([-3], 5);

-    -2 + 5 * 1 + 25 * (-3);

-    -72;

-  }

+  assert eval([-2, 1, -3], 5) == -72;

 }

 

 // To achieve a unique (except for leading zeros) representation of each number, we

diff --git a/Test/dafny4/runtest.bat b/Test/dafny4/runtest.bat
deleted file mode 100644
index cec5d271..00000000
--- a/Test/dafny4/runtest.bat
+++ /dev/null
@@ -1,7 +0,0 @@
-@echo off

-setlocal

-

-set BINARIES=..\..\Binaries

-set DAFNY_EXE=%BINARIES%\Dafny.exe

-

-%DAFNY_EXE% /compile:0 /verifySeparately /dprint:out.dfy.tmp %* CoqArt-InsertionSort.dfy GHC-MergeSort.dfy Fstar-QuickSort.dfy Primes.dfy KozenSilva.dfy SoftwareFoundations-Basics.dfy NumberRepresentations.dfy Circ.dfy ACL2-extractor.dfy ClassRefinement.dfy