Boogie:

* Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners.
* It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs.
Dafny:
* Ditto for its Parser.cs/Scanner.cs.
* Added ability to provide a custom Errors handler for scanner/parser.
* Added Test/dafny1/Cubes.dfy

1 files changed, 23 insertions, 0 deletions

diff --git a/Test/dafny1/Cubes.dfy b/Test/dafny1/Cubes.dfy
new file mode 100644
index 00000000..1ada79fa
--- /dev/null
+++ b/Test/dafny1/Cubes.dfy
@@ -0,0 +1,23 @@
+method Cubes(a: array<int>)

+  requires a != null;

+  modifies a;

+  ensures (forall i :: 0 <= i && i < a.Length ==> a[i] == i*i*i);

+{

+  var n := 0;

+  var c := 0;

+  var k := 1;

+  var m := 6;

+  while (n < a.Length)

+    invariant n <= a.Length;

+    invariant (forall i :: 0 <= i && i < n ==> a[i] == i*i*i);

+    invariant c == n*n*n;

+    invariant k == 3*n*n + 3*n + 1;

+    invariant m == 6*n + 6;

+  {

+    a[n] := c;

+    c := c + k;

+    k := k + m;

+    m := m + 6;

+    n := n + 1;

+  }

+}