* Added decreases clauses to functions

* If no decreases clause is given, the decreases clause defaults to the set of objects denoted by the reads clause, which was the previous Dafny behavior

* Made Dafny check loops for termination by default.  Previously, this was done only if the loop had a decreases clause.  To indicate that a loop is to be checked only for partial correctness, Dafny now allows "decreases *".

* Allow "reads *" to say that the function may read anything at all (sound, but not very useful)

* Adjusted frame axioms of functions to speak of allocated objects more liberally; and also added antecedents about the heaps being well-formed and the parameters being allocated

* Added some previously omitted well-definedness checks.

* Fixed some bugs in the resolver that caused some type errors not to be reported

* Added some messages to go with some (previously rather opaquely reported) errors

* Fixed some test cases that previously had ordered conjuncts incorrectly to prove termination and reads checks (such checks were previously omitted)

* Beefed up Test/dafny0/SchorrWaite.dfy to use datatypes to specify that no garbage gets marked.  The full-functional total-correctness verification of this Schorr-Waite method now takes about 3.2 seconds.

1 files changed, 18 insertions, 0 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
new file mode 100644
index 00000000..4cb02858
--- /dev/null
+++ b/Test/dafny0/TypeTests.dfy
@@ -0,0 +1,18 @@
+class C {

+  function F(c: C, d: D): bool { true }

+  method M(x: int) returns (y: int, c: C)

+    requires F(#D.A, this);  // 2 errors

+    requires F(4, 5);  // 2 errors

+    requires F(this, #D.A);  // good

+  { }

+

+  method Caller()

+  {

+    call m,n := M(true);  // error on in-parameter

+    call n,m := M(m);  // 2 errors on out-parameters

+  }

+}

+

+datatype D {

+  A;

+}