Dafny:

* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks

1 files changed, 0 insertions, 2 deletions

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index d8ee2013..34e0cfef 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -104,7 +104,6 @@ class Glossary {
         invariant q !in wr.footprint;

         invariant qcon == q.contents;

         invariant (forall k :: k in q.contents ==> k in glossary.keys);

-        decreases |definition| -i;

       {

         var w := definition[i];

         call present, d := glossary.Find(w);

@@ -342,7 +341,6 @@ class Map<Key,Value> {
     while (j < |keys|)

       invariant j <= |keys|;

       invariant key !in keys[..j];

-      decreases |keys| -j;

     {

       if (keys[j] == key) {

         idx := j;