From 666463d9fa29f14ea8aaec4d5bc8bd602e0033ba Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 24 Nov 2009 06:05:35 +0000 Subject: * 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. --- Test/VSI-Benchmarks/Answer | 4 ++-- Test/VSI-Benchmarks/b5.dfy | 4 ++-- Test/VSI-Benchmarks/b8.dfy | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'Test/VSI-Benchmarks') diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index a9fd2367..954ca3b0 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -9,7 +9,7 @@ Dafny program verifier finished with 3 verified, 0 errors -------------------- b3.dfy -------------------- -Dafny program verifier finished with 4 verified, 0 errors +Dafny program verifier finished with 5 verified, 0 errors -------------------- b4.dfy -------------------- @@ -29,4 +29,4 @@ Dafny program verifier finished with 11 verified, 0 errors -------------------- b8.dfy -------------------- -Dafny program verifier finished with 21 verified, 0 errors +Dafny program verifier finished with 22 verified, 0 errors diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index 8026e60f..34ff5f57 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -17,8 +17,8 @@ class Queue { tail.next == null && (forall n :: n in spine ==> - n != null && n.Valid() && - n.footprint <= footprint && + n != null && n.footprint <= footprint && this !in n.footprint && + n.Valid() && (n.next == null ==> n == tail)) && (forall n :: n in spine ==> diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index bc26ee85..a0cb6e74 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -59,7 +59,7 @@ class Glossary { invariant (forall d :: d in glossary.values ==> null !in d); invariant q !in rs.footprint; invariant q.contents == glossary.keys; - // we leave out the decreases clause - unbounded stream + decreases *; // we leave out the decreases clause - unbounded stream { call term,definition := readDefinition(rs); if (term == null) { @@ -135,7 +135,7 @@ class Glossary { while (true) invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint)); invariant null !in definition; - // we leave out the decreases clause - unbounded stream + decreases *; // we leave out the decreases clause - unbounded stream { call w := rs.GetWord(); if (w == null) -- cgit v1.2.3