From 3fb46aec7ee22e996323803b4828ee3b0e512053 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sat, 21 May 2011 18:15:17 -0700 Subject: 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) --- Test/VSI-Benchmarks/b4.dfy | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Test/VSI-Benchmarks') 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 { } } - 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 { 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; -- cgit v1.2.3