summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/Answer44
-rw-r--r--Test/dafny0/DTypes.dfy13
-rw-r--r--Test/dafny0/Definedness.dfy42
-rw-r--r--Test/dafny1/Answer2
-rw-r--r--Test/dafny1/PriorityQueue.dfy122
-rw-r--r--Test/dafny1/TerminationDemos.dfy13
6 files changed, 216 insertions, 20 deletions
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<T,U> {
}
+
+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<object>; // set of objects that make up the representation of a PriorityQueue
+
+ var a: array<int>; // 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))
+ }
+*/
}
// -----------------------------------
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 21:45:57 +0000