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)

10 files changed, 44 insertions, 44 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e0874a66..d9d3a572 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -53,7 +53,7 @@ datatype List<T> {
 

 datatype WildData {

   Something;

-  JustAboutAnything<G, H>(G, myName: set<H>, int, WildData);

+  JustAboutAnything(bool, myName: set<int>, int, WildData);

   More(List<int>);

 }

 

@@ -620,7 +620,7 @@ Execution trace:
     (0,0): anon5

     Termination.dfy(119,3): anon12_Else

     (0,0): anon7

-Termination.dfy(248,36): Error: cannot prove termination; try supplying a decreases clause

+Termination.dfy(248,35): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

@@ -694,7 +694,7 @@ DTypes.dfy(134,6): Related location: Related location
 DTypes.dfy(93,3): Related location: Related location

 Execution trace:

     (0,0): anon0

-DTypes.dfy(160,13): Error: assertion violation

+DTypes.dfy(160,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
index 35d939d3..2c9b3a35 100644
--- a/Test/dafny0/ControlStructures.dfy
+++ b/Test/dafny0/ControlStructures.dfy
@@ -9,7 +9,7 @@ method M0(d: D)
 }

 

 method M1(d: D)

-  requires d != #D.Blue;

+  requires d != D.Blue;

 {

   match (d) {  // error: missing case: Purple

     case Green =>

@@ -18,7 +18,7 @@ method M1(d: D)
 }

 

 method M2(d: D)

-  requires d != #D.Blue && d != #D.Purple;

+  requires d != D.Blue && d != D.Purple;

 {

   match (d) {

     case Green =>

@@ -27,9 +27,9 @@ method M2(d: D)
 }

 

 method M3(d: D)

-  requires d == #D.Green;

+  requires d == D.Green;

 {

-  if (d != #D.Green) {

+  if (d != D.Green) {

     match (d) {

       // nothing here

     }

@@ -37,9 +37,9 @@ method M3(d: D)
 }

 

 method M4(d: D)

-  requires d == #D.Green || d == #D.Red;

+  requires d == D.Green || d == D.Red;

 {

-  if (d != #D.Green) {

+  if (d != D.Green) {

     match (d) {  // error: missing case Red

       // nothing here

     }

@@ -56,7 +56,7 @@ function F0(d: D): int
 

 function F1(d: D, x: int): int

   requires x < 100;

-  requires d == #D.Red ==> x == 200;  // (an impossibility, given the first precondition, so d != Red)

+  requires d == D.Red ==> x == 200;  // (an impossibility, given the first precondition, so d != Red)

 {

   match (d)

   case Purple => 80

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index 2f59db73..b402c335 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -80,7 +80,7 @@ datatype Data {
 }

 

 function G(d: Data): int

-  requires d != #Data.Lemon;

+  requires d != Data.Lemon;

 {

   match d

   case Lemon => G(d)

@@ -144,19 +144,19 @@ class DatatypeInduction<T> {
   method IntegerInduction_Succeeds(a: array<int>)

     requires a != null;

     requires a.Length == 0 || a[0] == 0;

-    requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);

+    requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;

   {

     // The following assertion can be proved by induction:

-    assert (forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n);

+    assert forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n;

   }

 

   method IntegerInduction_Fails(a: array<int>)

     requires a != null;

     requires a.Length == 0 || a[0] == 0;

-    requires (forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1);

+    requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;

   {

     // ...but the induction heuristics don't recognize the situation as one where

     // applying induction would be profitable:

-    assert (forall n :: 0 <= n && n < a.Length ==> a[n] == n*n);  // error reported

+    assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n;  // error reported

   }

 }

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index 998b20bc..9a16a91a 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -19,14 +19,14 @@ class Node {
 

   method Init()

     modifies this;

-    ensures Repr(#List.Nil);

+    ensures Repr(Nil);

   {

     next := null;

   }

 

   method Add(d: int, L: List<int>) returns (r: Node)

     requires Repr(L);

-    ensures r != null && r.Repr(#List.Cons(d, L));

+    ensures r != null && r.Repr(Cons(d, L));

   {

     r := new Node;

     r.data := d;

@@ -49,14 +49,14 @@ class AnotherNode {
   }

 

   method Create() returns (n: AnotherNode)

-    ensures Repr(n, #List.Nil);

+    ensures Repr(n, Nil);

   {

     n := null;

   }

 

   method Add(n: AnotherNode, d: int, L: List<int>) returns (r: AnotherNode)

     requires Repr(n, L);

-    ensures Repr(r, #List.Cons(d, L));

+    ensures Repr(r, Cons(d, L));

   {

     r := new AnotherNode;

     r.data := d;

@@ -117,7 +117,7 @@ class NestedMatchExpr {
   method TestNesting0()

   {

     var x := 5;

-    var list := #List.Cons(3, #List.Cons(6, #List.Nil));

+    var list := Cons(3, Cons(6, Nil));

     assert Cadr(list, x) == 6;

     match (list) {

       case Nil => assert false;

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 6b7ce9b9..161ac22f 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -47,7 +47,7 @@ function method FenEric<T>(t0: T, t1: T): T;
 datatype Pair<T> { Pr(T, T); }

 

 method K(n: nat, i: int) {

-  match (#Pair.Pr(n, i)) {

+  match (Pair.Pr(n, i)) {

     case Pr(k, l) =>

       assert k == n;  // fine: although the type of k is int, we know it's equal to n

       assert 0 <= k;

diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy
index d8c8d91d..930c4253 100644
--- a/Test/dafny0/Simple.dfy
+++ b/Test/dafny0/Simple.dfy
@@ -46,7 +46,7 @@ datatype List<T> {
 

 datatype WildData {

   Something();

-  JustAboutAnything<G,H>(G, myName: set<H>, int, WildData);

+  JustAboutAnything(bool, myName: set<int>, int, WildData);

   More(List<int>);

 }

 

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index a5f02dc6..3359cff1 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -211,19 +211,19 @@ class AllocatedTests {
     assert allocated(6);

     assert allocated(6);

     assert allocated(null);

-    assert allocated(#Lindgren.HerrNilsson);

+    assert allocated(Lindgren.HerrNilsson);

 

     match (d) {

       case Pippi(n) => assert allocated(n);

       case Longstocking(q, dd) => assert allocated(q); assert allocated(dd);

       case HerrNilsson => assert old(allocated(d));

     }

-    var ls := #Lindgren.Longstocking([], d);

+    var ls := Lindgren.Longstocking([], d);

     assert allocated(ls);

     assert old(allocated(ls));

 

-    assert old(allocated(#Lindgren.Longstocking([r], d)));

-    assert old(allocated(#Lindgren.Longstocking([n], d)));  // error, because n was not allocated initially

+    assert old(allocated(Lindgren.Longstocking([r], d)));

+    assert old(allocated(Lindgren.Longstocking([n], d)));  // error, because n was not allocated initially

   }

 }

 

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 226eadbe..5d411eb3 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -79,7 +79,7 @@ class Termination {
 

   method Q<T>(list: List<T>) {

     var l := list;

-    while (l != #List.Nil)

+    while (l != List.Nil)

       decreases l;

     {

       call x, l := Traverse(l);

@@ -87,8 +87,8 @@ class Termination {
   }

 

   method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);

-    requires a != #List.Nil;

-    ensures a == #List.Cons(val, b);

+    requires a != List.Nil;

+    ensures a == List.Cons(val, b);

 }

 

 datatype List<T> {

@@ -245,7 +245,7 @@ function Zipper0<T>(a: List<T>, b: List<T>): List<T>
 {

   match a

   case Nil => b

-  case Cons(x, c) => #List.Cons(x, Zipper0(b, c))  // error: cannot prove termination

+  case Cons(x, c) => List.Cons(x, Zipper0(b, c))  // error: cannot prove termination

 }

 

 function Zipper1<T>(a: List<T>, b: List<T>, k: bool): List<T>

@@ -253,7 +253,7 @@ function Zipper1<T>(a: List<T>, b: List<T>, k: bool): List<T>
 {

   match a

   case Nil => b

-  case Cons(x, c) => #List.Cons(x, Zipper1(b, c, !k))

+  case Cons(x, c) => List.Cons(x, Zipper1(b, c, !k))

 }

 

 function Zipper2<T>(a: List<T>, b: List<T>): List<T>

@@ -262,7 +262,7 @@ function Zipper2<T>(a: List<T>, b: List<T>): List<T>
 {

   match a

   case Nil => b

-  case Cons(x, c) => #List.Cons(x, Zipper2(b, c))

+  case Cons(x, c) => List.Cons(x, Zipper2(b, c))

 }

 

 // -------------------------- test translation of while (*) -----------------

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 6fe86493..a932eccf 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -7,14 +7,14 @@ datatype Unit { It; }
 datatype Color { Yellow; Blue; }

 

 function F(a: Wrapper<Unit>): bool

-  ensures a == #Wrapper.Wrap(#Unit.It);

+  ensures a == Wrapper.Wrap(Unit.It);

 {

   match a

   case Wrap(u) => G(u)

 }

 

 function G(u: Unit): bool

-  ensures u == #Unit.It;

+  ensures u == Unit.It;

 {

   match u

   case It => true

@@ -23,19 +23,19 @@ function G(u: Unit): bool
 method BadLemma(c0: Color, c1: Color)

   ensures c0 == c1;

 {

-  var w0 := #Wrapper.Wrap(c0);

-  var w1 := #Wrapper.Wrap(c1);

+  var w0 := Wrapper.Wrap(c0);

+  var w1 := Wrapper.Wrap(c1);

 

   // Manually, add the following assertions in Boogie.  (These would

   // be ill-typed in Dafny.)

-  //     assert _default.F($Heap, this, w0#6);

-  //     assert _default.F($Heap, this, w1#7);

+  //     assert _default.F($Heap, this, w#06);

+  //     assert _default.F($Heap, this, w#17);

 

   assert w0 == w1;  // this would be bad news (it should be reported as an error)

 }

 

 method Main() {

-  call BadLemma(#Color.Yellow, #Color.Blue);

+  call BadLemma(Color.Yellow, Color.Blue);

   assert false;  // this shows how things can really go wrong if BadLemma verified successfully

 }

 

@@ -82,9 +82,9 @@ method M(list: List, S: set<MyClass>) returns (ret: int)
   // note, the definedness problem in the next line sits inside an unreachable branch

   assert (forall t: MyClass :: t != null ==> (if t.H() == 5 then true else 10 / 0 == 3));

 

-  assert TakesADatatype(#List.Nil) == 12;

-  assert TakesADatatype(#List.Cons(null, #List.Nil)) == 12;

-  assert AlsoTakesADatatype(#GenData.Pair(false, true)) == 17;

+  assert TakesADatatype(List.Nil) == 12;

+  assert TakesADatatype(List.Cons(null, List.Nil)) == 12;

+  assert AlsoTakesADatatype(GenData.Pair(false, true)) == 17;

 }

 

 method N() returns (k: MyClass)

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 792c8fac..7deeb0a1 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -1,9 +1,9 @@
 class C {

   function F(c: C, d: D): bool { true }

   method M(x: int) returns (y: int, c: C)

-    requires F(#D.A, this);  // 2 errors

+    requires F(D.A, this);  // 2 errors

     requires F(4, 5);  // 2 errors

-    requires F(this, #D.A);  // good

+    requires F(this, D.A);  // good

   { }

 

   method Caller()