summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2009-11-24 06:05:35 +0000
committerGravatar rustanleino <unknown>2009-11-24 06:05:35 +0000
commit6a14224aabbdf2145bf522b526313719e9373202 (patch)
treeaefe2f00fe1fa0bcfaa615cb70683709e74fe20a /Test/VSI-Benchmarks
parent9ed23deb0a3db4b61cf07fc6b551e10bc5436837 (diff)
* 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.
Diffstat (limited to 'Test/VSI-Benchmarks')
-rw-r--r--Test/VSI-Benchmarks/Answer4
-rw-r--r--Test/VSI-Benchmarks/b5.dfy4
-rw-r--r--Test/VSI-Benchmarks/b8.dfy4
3 files changed, 6 insertions, 6 deletions
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<T> {
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)