Dafny:

* started rewriting parsing of qualified identifiers in expressions
* annoyingly, had to introduce AST nodes for concrete syntax
* previous syntax for invoking datatype constructors: #List.Cons(h, t)
  new syntax:  List.Cons(h, t)
  or, if only one datatype has a constructor named Cons:  Cons(h, t)
* Removed type parameters for datatype constructors from the grammar
* Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)

1 files changed, 4 insertions, 1 deletions

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index ebaeab84..9f7e272e 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -88,7 +88,7 @@ class Map<Key,Value> {
     }

   }

 

-  method Remove(key: Key)

+  method Remove(key: Key)// returns (ghost h: int)

     requires Valid();

     modifies Repr;

     ensures Valid() && fresh(Repr - old(Repr));

@@ -111,6 +111,9 @@ class Map<Key,Value> {
     if (p != null) {

       Keys := Keys[..n] + Keys[n+1..];

       Values := Values[..n] + Values[n+1..];

+      assert Keys[n..] == old(Keys)[n+1..];

+      assert Values[n..] == old(Values)[n+1..];

+

       nodes := nodes[..n] + nodes[n+1..];

       if (prev == null) {

         head := head.next;