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).

1 files changed, 17 insertions, 0 deletions

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

+}