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, 10 insertions, 10 deletions

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)