Dafny: Ensures that function axioms are not being used while their consistency is being checked.

1 files changed, 13 insertions, 0 deletions

diff --git a/Test/dafny0/BadFunction.dfy b/Test/dafny0/BadFunction.dfy
new file mode 100644
index 00000000..3affaa80
--- /dev/null
+++ b/Test/dafny0/BadFunction.dfy
@@ -0,0 +1,13 @@
+// The following function gives rise to an inconsistent axiom, except

+// for its CanUseFunctionDefs antecedent, which saves the day.

+function F(x: int): int

+  decreases x;

+{

+  F(x) + 1  // error: does not decrease termination metric

+}

+

+method M()

+{

+  assert F(5) == 0;  // no error is generated here, because of the inconsistent axiom

+  assert false;  // ditto

+}