Improve computations, in particular compositionality. Isolated useless literals around if-then-else as a surprising source of practical hanging.

1 files changed, 22 insertions, 1 deletions

diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy
index 72e249d8..b225a210 100644
--- a/Test/dafny0/ComputationsNeg.dfy
+++ b/Test/dafny0/ComputationsNeg.dfy
@@ -19,4 +19,25 @@ ghost method test_ThProperty()
   ensures ThProperty(10, Succ(Zero), 0);

 {

 //  assert ThProperty(9, Zero, 0);

-}
\ No newline at end of file
+}

+

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

+} 

+function fact(n: nat): nat

+{

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

+}

+method test_fact()

+{

+  assert fact(0) == 1;

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

+}