Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for literals.

Added axiom to better handle DtAlloc/GenericAlloc correspondence (which improves handling of computations).

2 files changed, 24 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 29f7b8cc..5297d132 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2047,8 +2047,14 @@ Execution trace:
 Dafny program verifier finished with 1 verified, 4 errors

 

 -------------------- Computations.dfy --------------------

+Computations.dfy(163,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Computations.dfy(168,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 46 verified, 0 errors

+Dafny program verifier finished with 49 verified, 2 errors

 

 -------------------- ComputationsNeg.dfy --------------------

 ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure

diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
index 641b8207..4b975559 100644
--- a/Test/dafny0/Computations.dfy
+++ b/Test/dafny0/Computations.dfy
@@ -150,3 +150,20 @@ ghost method copt_test()
   ensures copt(Plus(Plus(Plus(Num(0), Num(0)), Num(0)), Num(1)))==Num(1);

 {

 }

+

+// The following is a test that well-typedness antecednets are included in the literal axioms

+static function StaticFact(n: nat): nat

+  ensures 0 < StaticFact(n);

+{

+  if n == 0 then 1 else n * StaticFact(n - 1)

+}

+static method test_StaticFact()

+{

+  assert StaticFact(0) == 1;

+  assert 42 != 42;  // error:  this should fail

+} 

+method test_fact()

+{

+  assert fact(0) == 1;

+  assert 42 != 42;  // error:  this should fail

+}