From bcd9c547b4245b014b1296b9924b4c7b4f4bf02e Mon Sep 17 00:00:00 2001 From: rustanleino Date: Wed, 2 Feb 2011 23:23:14 +0000 Subject: Dafny: added ensures clauses to functions --- Test/dafny0/Answer | 44 +++++++++----- Test/dafny0/DTypes.dfy | 13 +++++ Test/dafny0/Definedness.dfy | 42 ++++++++++++++ Test/dafny1/Answer | 2 +- Test/dafny1/PriorityQueue.dfy | 122 +++++++++++++++++++++++++++++++++++++-- Test/dafny1/TerminationDemos.dfy | 13 +++++ 6 files changed, 216 insertions(+), 20 deletions(-) (limited to 'Test') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 4b4bf920..34b9a0be 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -87,17 +87,17 @@ Execution trace: (0,0): anon0 SmallTests.dfy(61,36): Error: possible division by zero Execution trace: - (0,0): anon10_Then + (0,0): anon12_Then SmallTests.dfy(62,51): Error: possible division by zero Execution trace: - (0,0): anon10_Else + (0,0): anon12_Else (0,0): anon3 - (0,0): anon11_Else + (0,0): anon13_Else SmallTests.dfy(63,22): Error: target object may be null Execution trace: - (0,0): anon10_Then + (0,0): anon12_Then (0,0): anon3 - (0,0): anon11_Then + (0,0): anon13_Then (0,0): anon6 SmallTests.dfy(82,20): Error: decreases expression must be well defined at top of each loop iteration Execution trace: @@ -129,7 +129,7 @@ Dafny program verifier finished with 28 verified, 9 errors -------------------- Definedness.dfy -------------------- Definedness.dfy(8,7): Error: possible division by zero Execution trace: - (0,0): anon0 + (0,0): anon3_Else Definedness.dfy(15,16): Error: possible division by zero Execution trace: (0,0): anon0 @@ -263,8 +263,22 @@ Execution trace: Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry. Execution trace: (0,0): anon0 +Definedness.dfy(231,30): Error: possible violation of function postcondition +Execution trace: + (0,0): anon0 + (0,0): anon5_Else +Definedness.dfy(238,22): Error: target object may be null +Execution trace: + (0,0): anon5_Then + (0,0): anon2 + (0,0): anon6_Then +Definedness.dfy(254,24): Error: possible violation of function postcondition +Execution trace: + (0,0): anon7_Then + (0,0): anon2 + (0,0): anon8_Else -Dafny program verifier finished with 21 verified, 29 errors +Dafny program verifier finished with 23 verified, 32 errors -------------------- Array.dfy -------------------- Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause @@ -293,14 +307,14 @@ Execution trace: (0,0): anon0 Array.dfy(107,6): Error: insufficient reads clause to read array element Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon5_Then + (0,0): anon7_Else + (0,0): anon8_Then + (0,0): anon9_Then Array.dfy(115,6): Error: insufficient reads clause to read array element Execution trace: - (0,0): anon0 - (0,0): anon4_Then - (0,0): anon5_Then + (0,0): anon7_Else + (0,0): anon8_Then + (0,0): anon9_Then Array.dfy(131,10): Error: assignment may update an array element not in the enclosing method's modifies clause Execution trace: (0,0): anon0 @@ -348,7 +362,7 @@ Dafny program verifier finished with 16 verified, 2 errors -------------------- BadFunction.dfy -------------------- BadFunction.dfy(6,3): Error: failure to decrease termination measure Execution trace: - (0,0): anon0 + (0,0): anon3_Else Dafny program verifier finished with 2 verified, 1 error @@ -437,7 +451,7 @@ DTypes.dfy(54,18): Error: assertion violation Execution trace: (0,0): anon0 -Dafny program verifier finished with 13 verified, 3 errors +Dafny program verifier finished with 14 verified, 3 errors -------------------- TypeParameters.dfy -------------------- TypeParameters.dfy(41,22): Error: assertion violation diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index c6f0737c..d925587b 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -74,3 +74,16 @@ class Node { } class CP { } + +datatype Data { + Lemon; + Kiwi(int); +} + +function G(d: Data): int + requires d != #Data.Lemon; +{ + match d + case Lemon => G(d) + case Kiwi(x) => 7 +} diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index d557de21..1cb74b1d 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -213,3 +213,45 @@ class StatementTwoShoes { } } } + +// ----------------- function postconditions ---------------------- + +class Mountain { var x: int; } + +function Postie0(c: Mountain): Mountain + requires c != null; + ensures Postie0(c) != null && Postie0(c).x <= Postie0(c).x; + ensures Postie0(c).x == Postie0(c).x; +{ + c +} + +function Postie1(c: Mountain): Mountain + requires c != null; + ensures Postie1(c) != null && Postie1(c).x == 5; // error: postcondition violation (but no well-formedness problem) +{ + c +} + +function Postie2(c: Mountain): Mountain + requires c != null && c.x == 5; + ensures Postie2(c).x == 5; // well-formedness error (null dereference) +{ + c +} + +function Postie3(c: Mountain): Mountain // all is cool + requires c != null && c.x == 5; + ensures Postie3(c) != null && Postie3(c).x < 10; + ensures Postie3(c).x == 5; +{ + c +} + +function Postie4(c: Mountain): Mountain + requires c != null && c.x <= 5; + ensures Postie4(c) != null && Postie4(c).x < 10; + ensures Postie4(c).x == 5; // error: postcondition might not hold +{ + c +} diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index b8f9591f..5b51b3e4 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -9,7 +9,7 @@ Dafny program verifier finished with 22 verified, 0 errors -------------------- PriorityQueue.dfy -------------------- -Dafny program verifier finished with 12 verified, 0 errors +Dafny program verifier finished with 24 verified, 0 errors -------------------- BinaryTree.dfy -------------------- diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy index 76e4b1d6..4a9ba220 100644 --- a/Test/dafny1/PriorityQueue.dfy +++ b/Test/dafny1/PriorityQueue.dfy @@ -49,7 +49,7 @@ class PriorityQueue { requires 1 <= k && k <= n; requires MostlyValid(); requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]); - requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != k ==> a[j/2/2] <= a[j]); + requires (forall j :: 1 <= j && j <= n ==> j/2 != k); // k is a child modifies a; ensures Valid(); { @@ -58,7 +58,7 @@ class PriorityQueue { while (1 < i) invariant i <= k && MostlyValid(); invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]); - invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != i ==> a[j/2/2] <= a[j]); + invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]); { if (a[i/2] <= a[i]) { return; @@ -84,7 +84,7 @@ class PriorityQueue { requires 1 <= k; requires MostlyValid(); requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]); - requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]); + requires k == 1; modifies a; ensures Valid(); { @@ -92,7 +92,121 @@ class PriorityQueue { while (2*i <= n) // while i is not a leaf invariant 1 <= i && MostlyValid(); invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]); - invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]); + invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]); + { + var smallestChild; + if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) { + smallestChild := 2*i + 1; + } else { + smallestChild := 2*i; + } + if (a[i] <= a[smallestChild]) { + return; + } + var tmp := a[i]; a[i] := a[smallestChild]; a[smallestChild] := tmp; + i := smallestChild; + assert 1 <= i/2/2 ==> a[i/2/2] <= a[i]; + } + } +} + +// ---------- Alternative specifications ---------- + +class PriorityQueue_Alternative { + var N: int; // capacity + var n: int; // current size + ghost var Repr: set; // set of objects that make up the representation of a PriorityQueue + + var a: array; // private implementation of PriorityQueu + + function Valid(): bool + reads this, Repr; + { + MostlyValid() && + (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j]) + } + + function MostlyValid(): bool + reads this, Repr; + { + this in Repr && a in Repr && + a != null && a.Length == N+1 && + 0 <= n && n <= N + } + + method Init(capacity: int) + requires 0 <= capacity; + modifies this; + ensures Valid() && fresh(Repr - {this}); + ensures N == capacity; + { + N := capacity; + var arr := new int[N+1]; + a := arr; + n := 0; + Repr := {this}; + Repr := Repr + {a}; + } + + method Insert(x: int) + requires Valid() && n < N; + modifies this, a; + ensures Valid() && fresh(Repr - old(Repr)); + ensures n == old(n) + 1 && N == old(N); + { + n := n + 1; + a[n] := x; + call SiftUp(n); + } + + method SiftUp(k: int) + requires 1 <= k && k <= n; + requires MostlyValid(); + requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]); + requires (forall j :: 1 <= j && j <= n ==> j/2 != k); // k is a child + modifies a; + ensures Valid(); + { + var i := k; + assert MostlyValid(); + while (1 < i) + invariant i <= k && MostlyValid(); + invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]); + invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]); + { + if (a[i/2] <= a[i]) { + return; + } + var tmp := a[i]; a[i] := a[i/2]; a[i/2] := tmp; + i := i / 2; + } + } + + method RemoveMin() returns (x: int) + requires Valid() && 1 <= n; + modifies this, a; + ensures Valid() && fresh(Repr - old(Repr)); + ensures n == old(n) - 1; + { + x := a[1]; + a[1] := a[n]; + n := n - 1; + call SiftDown(1); + } + + method SiftDown(k: int) + requires 1 <= k; + requires MostlyValid(); + requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]); + requires k == 1; // k is the root + modifies a; + ensures Valid(); + { + var i := k; + while (2*i <= n) // while i is not a leaf + invariant 1 <= i && MostlyValid(); + invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]); + invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]); { var smallestChild; if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) { diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index fb530258..76925e8e 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -30,6 +30,19 @@ class Ackermann { else F(m - 1, F(m, n - 1)) } +/* + function G(m: int, n: int): int + requires 0 <= m && 0 <= n; + ensures 0 <= G(m, n); + { + if m == 0 then + n + 1 + else if n == 0 then + G(m - 1, 1) + else + G(m - 1, G(m, n - 1)) + } +*/ } // ----------------------------------- -- cgit v1.2.3