diff options
Diffstat (limited to 'Test/dafny1/PriorityQueue.dfy')
| -rw-r--r-- | Test/dafny1/PriorityQueue.dfy | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy index 94223cba..3d2a5d78 100644 --- a/Test/dafny1/PriorityQueue.dfy +++ b/Test/dafny1/PriorityQueue.dfy @@ -12,7 +12,7 @@ class PriorityQueue { reads this, Repr;
{
MostlyValid() &&
- (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+ (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])
}
predicate MostlyValid()
@@ -50,8 +50,8 @@ class PriorityQueue { 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 leaf
+ requires (forall j {:nowarn} :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
+ requires (forall j {:nowarn} :: 1 <= j && j <= n ==> j/2 != k); // k is a leaf
modifies a;
ensures Valid();
{
@@ -59,8 +59,8 @@ class PriorityQueue { 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]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
{
if (a[i/2] <= a[i]) {
return;
@@ -85,8 +85,8 @@ class PriorityQueue { 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 (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
+ requires (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
+ requires (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
// Alternatively, the line above can be expressed as:
// requires (forall j :: 1 <= k/2 && j/2 == k && j <= n ==> a[j/2/2] <= a[j]);
modifies a;
@@ -95,8 +95,8 @@ class PriorityQueue { 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 :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
{
var smallestChild;
if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
@@ -127,7 +127,7 @@ class PriorityQueue_Alternative { reads this, Repr;
{
MostlyValid() &&
- (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+ (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])
}
predicate MostlyValid()
@@ -164,7 +164,7 @@ class PriorityQueue_Alternative { method SiftUp()
requires MostlyValid();
- requires (forall j :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
+ requires (forall j {:nowarn} :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
modifies a;
ensures Valid();
{
@@ -172,8 +172,8 @@ class PriorityQueue_Alternative { assert MostlyValid();
while (1 < i)
invariant i <= n && 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]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
{
if (a[i/2] <= a[i]) {
return;
@@ -197,15 +197,15 @@ class PriorityQueue_Alternative { method SiftDown()
requires MostlyValid();
- requires (forall j :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
+ requires (forall j {:nowarn} :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
modifies a;
ensures Valid();
{
var i := 1;
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]);
+ invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+ invariant (forall j {:nowarn} :: 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]) {
|