From 9dbf2a6ce1e130f634c27da7bc300001e28aedaf 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/dafny0/Answer | 6 +++--- Test/dafny0/ControlStructures.dfy | 14 +++++++------- Test/dafny0/DTypes.dfy | 10 +++++----- Test/dafny0/Datatypes.dfy | 10 +++++----- Test/dafny0/NatTypes.dfy | 2 +- Test/dafny0/Simple.dfy | 2 +- Test/dafny0/SmallTests.dfy | 8 ++++---- Test/dafny0/Termination.dfy | 12 ++++++------ Test/dafny0/TypeAntecedents.dfy | 20 ++++++++++---------- Test/dafny0/TypeTests.dfy | 4 ++-- 10 files changed, 44 insertions(+), 44 deletions(-) (limited to 'Test/dafny0') 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 { datatype WildData { Something; - JustAboutAnything(G, myName: set, int, WildData); + JustAboutAnything(bool, myName: set, int, WildData); More(List); } @@ -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 { method IntegerInduction_Succeeds(a: array) 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) 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) 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) 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(t0: T, t1: T): T; datatype Pair { 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 { datatype WildData { Something(); - JustAboutAnything(G, myName: set, int, WildData); + JustAboutAnything(bool, myName: set, int, WildData); More(List); } 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(list: List) { 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(a: List) returns (val: T, b: List); - requires a != #List.Nil; - ensures a == #List.Cons(val, b); + requires a != List.Nil; + ensures a == List.Cons(val, b); } datatype List { @@ -245,7 +245,7 @@ function Zipper0(a: List, b: List): List { 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(a: List, b: List, k: bool): List @@ -253,7 +253,7 @@ function Zipper1(a: List, b: List, k: bool): List { 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(a: List, b: List): List @@ -262,7 +262,7 @@ function Zipper2(a: List, b: List): List { 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): 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) 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() -- cgit v1.2.3