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

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

   }

 }