summaryrefslogtreecommitdiff
path: root/Test/dafny1
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny1')
-rw-r--r--Test/dafny1/BDD.dfy1
-rw-r--r--Test/dafny1/ExtensibleArrayAuto.dfy36
-rw-r--r--Test/dafny1/FindZero.dfy10
-rw-r--r--Test/dafny1/Induction.dfy32
-rw-r--r--Test/dafny1/MoreInduction.dfy18
-rw-r--r--Test/dafny1/MoreInduction.dfy.expect16
-rw-r--r--Test/dafny1/PriorityQueue.dfy32
-rw-r--r--Test/dafny1/Rippling.dfy114
-rw-r--r--Test/dafny1/SchorrWaite-stages.dfy2
-rw-r--r--Test/dafny1/SchorrWaite.dfy8
-rw-r--r--Test/dafny1/Substitution.dfy2
-rw-r--r--Test/dafny1/UltraFilter.dfy2
12 files changed, 137 insertions, 136 deletions
diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy
index 252164db..59dc3092 100644
--- a/Test/dafny1/BDD.dfy
+++ b/Test/dafny1/BDD.dfy
@@ -55,6 +55,7 @@ module SimpleBDD
node := if s[n-i] then node.t else node.f;
i := i - 1;
}
+ assert s[n-i..] == [];
b := node.b;
}
}
diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
index b2e5ecc4..01afdafd 100644
--- a/Test/dafny1/ExtensibleArrayAuto.dfy
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -2,12 +2,12 @@
// RUN: %diff "%s.expect" "%t"
class {:autocontracts} ExtensibleArray<T> {
- ghost var Contents: seq<T>;
+ ghost var Contents: seq<T>
- var elements: array<T>;
- var more: ExtensibleArray<array<T>>;
- var length: int;
- var M: int; // shorthand for: if more == null then 0 else 256 * |more.Contents|
+ var elements: array<T>
+ var more: ExtensibleArray<array<T>>
+ var length: int
+ var M: int // shorthand for: if more == null then 0 else 256 * |more.Contents|
predicate Valid()
{
@@ -35,7 +35,7 @@ class {:autocontracts} ExtensibleArray<T> {
}
constructor Init()
- ensures Contents == [];
+ ensures Contents == []
{
elements := new T[256];
more := null;
@@ -46,11 +46,11 @@ class {:autocontracts} ExtensibleArray<T> {
}
method Get(i: int) returns (t: T)
- requires 0 <= i < |Contents|;
- ensures t == Contents[i];
- decreases Repr;
+ requires 0 <= i < |Contents|
+ ensures t == Contents[i]
+ decreases Repr
{
- if (M <= i) {
+ if M <= i {
t := elements[i - M];
} else {
var arr := more.Get(i / 256);
@@ -59,10 +59,10 @@ class {:autocontracts} ExtensibleArray<T> {
}
method Set(i: int, t: T)
- requires 0 <= i < |Contents|;
- ensures Contents == old(Contents)[i := t];
+ requires 0 <= i < |Contents|
+ ensures Contents == old(Contents)[i := t]
{
- if (M <= i) {
+ if M <= i {
elements[i - M] := t;
} else {
var arr := more.Get(i / 256);
@@ -72,14 +72,14 @@ class {:autocontracts} ExtensibleArray<T> {
}
method Append(t: T)
- ensures Contents == old(Contents) + [t];
- decreases |Contents|;
+ ensures Contents == old(Contents) + [t]
+ decreases |Contents|
{
- if (length == 0 || length % 256 != 0) {
+ if length == 0 || length % 256 != 0 {
// there is room in "elements"
elements[length - M] := t;
} else {
- if (more == null) {
+ if more == null {
more := new ExtensibleArray<array<T>>.Init();
Repr := Repr + {more} + more.Repr;
}
@@ -99,7 +99,7 @@ class {:autocontracts} ExtensibleArray<T> {
method Main() {
var a := new ExtensibleArray<int>.Init();
var n := 0;
- while (n < 256*256+600)
+ while n < 256*256+600
invariant a.Valid() && fresh(a.Repr);
invariant |a.Contents| == n;
{
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index f0eb6a60..374555b0 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -3,7 +3,7 @@
method FindZero(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
@@ -18,9 +18,9 @@ method FindZero(a: array<int>) returns (r: int)
r := -1;
}
-ghost method Lemma(a: array<int>, k: int, m: int)
+lemma Lemma(a: array<int>, k: int, m: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
requires 0 <= k;
requires k < a.Length ==> m <= a[k];
ensures forall i :: k <= i < k+m && i < a.Length ==> a[i] != 0;
@@ -36,7 +36,7 @@ ghost method Lemma(a: array<int>, k: int, m: int)
method FindZero_GhostLoop(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
@@ -63,7 +63,7 @@ method FindZero_GhostLoop(a: array<int>) returns (r: int)
method FindZero_Assert(a: array<int>) returns (r: int)
requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
- requires forall i :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
+ requires forall i {:nowarn} :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
ensures 0 <= r ==> r < a.Length && a[r] == 0;
ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
{
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 28171896..e2cd4ade 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -22,7 +22,7 @@ class IntegerInduction {
// Here is one proof. It uses a lemma, which is proved separately.
- ghost method Theorem0(n: int)
+ lemma Theorem0(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
@@ -32,7 +32,7 @@ class IntegerInduction {
}
}
- ghost method Lemma(n: int)
+ lemma Lemma(n: int)
requires 0 <= n;
ensures 2 * Gauss(n) == n*(n+1);
{
@@ -42,7 +42,7 @@ class IntegerInduction {
// Here is another proof. It states the lemma as part of the theorem, and
// thus proves the two together.
- ghost method Theorem1(n: int)
+ lemma Theorem1(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
ensures 2 * Gauss(n) == n*(n+1);
@@ -52,24 +52,24 @@ class IntegerInduction {
}
}
- ghost method DoItAllInOneGo()
- ensures (forall n :: 0 <= n ==>
+ lemma DoItAllInOneGo()
+ ensures (forall n {:split false} :: 0 <= n ==> // WISH reenable quantifier splitting here. This will only work once we generate induction hypotheses at the Dafny level.
SumOfCubes(n) == Gauss(n) * Gauss(n) &&
2 * Gauss(n) == n*(n+1));
{
}
- // The following two ghost methods are the same as the previous two, but
+ // The following two lemmas are the same as the previous two, but
// here no body is given--and the proof still goes through (thanks to
// Dafny's ghost-method induction tactic).
- ghost method Lemma_Auto(n: int)
+ lemma Lemma_Auto(n: int)
requires 0 <= n;
ensures 2 * Gauss(n) == n*(n+1);
{
}
- ghost method Theorem1_Auto(n: int)
+ lemma Theorem1_Auto(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
ensures 2 * Gauss(n) == n*(n+1);
@@ -79,7 +79,7 @@ class IntegerInduction {
// Here is another proof. It makes use of Dafny's induction heuristics to
// prove the lemma.
- ghost method Theorem2(n: int)
+ lemma Theorem2(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
{
@@ -90,7 +90,7 @@ class IntegerInduction {
}
}
- ghost method M(n: int)
+ lemma M(n: int)
requires 0 <= n;
{
assume (forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1)); // manually assume the induction hypothesis
@@ -99,7 +99,7 @@ class IntegerInduction {
// Another way to prove the lemma is to supply a postcondition on the Gauss function
- ghost method Theorem3(n: int)
+ lemma Theorem3(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
{
@@ -117,14 +117,14 @@ class IntegerInduction {
// Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction
- ghost method Theorem4()
+ lemma Theorem4()
ensures (forall n :: 0 <= n ==>
SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n));
{
// look ma, no hints!
}
- ghost method Theorem5(n: int)
+ lemma Theorem5(n: int)
requires 0 <= n;
ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
{
@@ -148,11 +148,11 @@ class IntegerInduction {
// Proving the "<==" case is simple; it's the "==>" case that requires induction.
// The example uses an attribute that requests induction on just "j". However, the proof also
// goes through by applying induction on both bound variables.
- function method IsSorted(s: seq<int>): bool
- ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);
+ function method IsSorted(s: seq<int>): bool //WISH remove autotriggers false
+ ensures IsSorted(s) ==> (forall i,j {:induction j} {:autotriggers false} :: 0 <= i < j < |s| ==> s[i] <= s[j]);
ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);
{
- (forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i])
+ (forall i {:nowarn} :: 1 <= i && i < |s| ==> s[i-1] <= s[i])
}
}
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index 41adcf50..2b5187a4 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
datatype List<X> = Nil | Cons(Node<X>, List<X>)
@@ -42,13 +42,13 @@ function ToSeq<X>(list: List<X>): seq<X>
case Nary(nn) => ToSeq(nn) + ToSeq(rest)
}
-ghost method Theorem<X>(list: List<X>)
+lemma Theorem<X>(list: List<X>)
ensures ToSeq(list) == ToSeq(FlattenMain(list));
{
Lemma(list, Nil);
}
-ghost method Lemma<X>(list: List<X>, ext: List<X>)
+lemma Lemma<X>(list: List<X>, ext: List<X>)
requires IsFlat(ext);
ensures ToSeq(list) + ToSeq(ext) == ToSeq(Flatten(list, ext));
{
@@ -73,27 +73,27 @@ function NegFac(n: int): int
if -1 <= n then -1 else - NegFac(n+1) * n
}
-ghost method LemmaAll()
+lemma LemmaAll()
ensures forall n :: NegFac(n) <= -1; // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
{
}
-ghost method LemmaOne(n: int)
+lemma LemmaOne(n: int)
ensures NegFac(n) <= -1; // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
{
}
-ghost method LemmaAll_Neg()
- ensures forall n :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
+lemma LemmaAll_Neg() //FIXME I don't understand the comment below; what trigger?
+ ensures forall n {:nowarn} :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
{
}
-ghost method LemmaOne_Neg(n: int)
+lemma LemmaOne_Neg(n: int) //FIXME What trigger?
ensures NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
{
}
-ghost method LemmaOneWithDecreases(n: int)
+lemma LemmaOneWithDecreases(n: int)
ensures NegFac(n) <= -1; // here, the programmer gives a good well-founded order, so this verifies
decreases -n;
{
diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect
index c8785e56..5de0ace6 100644
--- a/Test/dafny1/MoreInduction.dfy.expect
+++ b/Test/dafny1/MoreInduction.dfy.expect
@@ -1,17 +1,17 @@
-MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(82,20): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(92,21): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
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]) {
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 55701a93..d888a5cc 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -300,244 +300,244 @@ function AlwaysTrueFunction(): FunctionValue
// The theorems to be proved
// -----------------------------------------------------------------------------------
-ghost method P1()
+lemma P1()
ensures forall n, xs :: concat(take(n, xs), drop(n, xs)) == xs;
{
}
-ghost method P2()
+lemma P2()
ensures forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, concat(xs, ys));
{
}
-ghost method P3()
+lemma P3()
ensures forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True;
{
}
-ghost method P4()
+lemma P4()
ensures forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs));
{
}
-ghost method P5()
+lemma P5()
ensures forall n, xs, x ::
add(Suc(Zero), count(n, xs)) == count(n, Cons(x, xs))
==> n == x;
{
}
-ghost method P6()
+lemma P6()
ensures forall m, n :: minus(n, add(n, m)) == Zero;
{
}
-ghost method P7()
+lemma P7()
ensures forall m, n :: minus(add(n, m), n) == m;
{
}
-ghost method P8()
+lemma P8()
ensures forall k, m, n :: minus(add(k, m), add(k, n)) == minus(m, n);
{
}
-ghost method P9()
+lemma P9()
ensures forall i, j, k :: minus(minus(i, j), k) == minus(i, add(j, k));
{
}
-ghost method P10()
+lemma P10()
ensures forall m :: minus(m, m) == Zero;
{
}
-ghost method P11()
+lemma P11()
ensures forall xs :: drop(Zero, xs) == xs;
{
}
-ghost method P12()
+lemma P12()
ensures forall n, xs, f :: drop(n, apply(f, xs)) == apply(f, drop(n, xs));
{
}
-ghost method P13()
+lemma P13()
ensures forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs);
{
}
-ghost method P14()
+lemma P14()
ensures forall xs, ys, p :: filter(p, concat(xs, ys)) == concat(filter(p, xs), filter(p, ys));
{
}
-ghost method P15()
+lemma P15()
ensures forall x, xs :: len(ins(x, xs)) == Suc(len(xs));
{
}
-ghost method P16()
+lemma P16()
ensures forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x;
{
}
-ghost method P17()
+lemma P17()
ensures forall n :: leq(n, Zero) == True <==> n == Zero;
{
}
-ghost method P18()
+lemma P18()
ensures forall i, m :: less(i, Suc(add(i, m))) == True;
{
}
-ghost method P19()
+lemma P19()
ensures forall n, xs :: len(drop(n, xs)) == minus(len(xs), n);
{
}
-ghost method P20()
+lemma P20()
ensures forall xs :: len(sort(xs)) == len(xs);
{
// the proof of this theorem requires a lemma about "insort"
assert forall x, xs :: len(insort(x, xs)) == Suc(len(xs));
}
-ghost method P21()
+lemma P21()
ensures forall n, m :: leq(n, add(n, m)) == True;
{
}
-ghost method P22()
+lemma P22()
ensures forall a, b, c :: max(max(a, b), c) == max(a, max(b, c));
{
}
-ghost method P23()
+lemma P23()
ensures forall a, b :: max(a, b) == max(b, a);
{
}
-ghost method P24()
+lemma P24()
ensures forall a, b :: max(a, b) == a <==> leq(b, a) == True;
{
}
-ghost method P25()
+lemma P25()
ensures forall a, b :: max(a, b) == b <==> leq(a, b) == True;
{
}
-ghost method P26()
+lemma P26()
ensures forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True;
{
}
-ghost method P27()
+lemma P27()
ensures forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True;
{
}
-ghost method P28()
+lemma P28()
ensures forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True;
{
}
-ghost method P29()
+lemma P29()
ensures forall x, xs :: mem(x, ins1(x, xs)) == True;
{
}
-ghost method P30()
+lemma P30()
ensures forall x, xs :: mem(x, ins(x, xs)) == True;
{
}
-ghost method P31()
+lemma P31()
ensures forall a, b, c :: min(min(a, b), c) == min(a, min(b, c));
{
}
-ghost method P32()
+lemma P32()
ensures forall a, b :: min(a, b) == min(b, a);
{
}
-ghost method P33()
+lemma P33()
ensures forall a, b :: min(a, b) == a <==> leq(a, b) == True;
{
}
-ghost method P34()
+lemma P34()
ensures forall a, b :: min(a, b) == b <==> leq(b, a) == True;
{
}
-ghost method P35()
+lemma P35()
ensures forall xs :: dropWhileAlways(AlwaysFalseFunction(), xs) == xs;
{
}
-ghost method P36()
+lemma P36()
ensures forall xs :: takeWhileAlways(AlwaysTrueFunction(), xs) == xs;
{
}
-ghost method P37()
+lemma P37()
ensures forall x, xs :: not(mem(x, delete(x, xs))) == True;
{
}
-ghost method P38()
+lemma P38()
ensures forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs));
{
}
-ghost method P39()
+lemma P39()
ensures forall n, x, xs ::
add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs));
{
}
-ghost method P40()
+lemma P40()
ensures forall xs :: take(Zero, xs) == Nil;
{
}
-ghost method P41()
+lemma P41()
ensures forall n, xs, f :: take(n, apply(f, xs)) == apply(f, take(n, xs));
{
}
-ghost method P42()
+lemma P42()
ensures forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs));
{
}
-ghost method P43(p: FunctionValue)
+lemma P43(p: FunctionValue)
ensures forall xs :: concat(takeWhileAlways(p, xs), dropWhileAlways(p, xs)) == xs;
{
}
-ghost method P44()
+lemma P44()
ensures forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys);
{
}
-ghost method P45()
+lemma P45()
ensures forall x, xs, y, ys ::
zip(Cons(x, xs), Cons(y, ys)) ==
PCons(Pair.Pair(x, y), zip(xs, ys));
{
}
-ghost method P46()
+lemma P46()
ensures forall ys :: zip(Nil, ys) == PNil;
{
}
-ghost method P47()
+lemma P47()
ensures forall a :: height(mirror(a)) == height(a);
{
// proving this theorem requires a previously proved lemma:
@@ -546,20 +546,20 @@ ghost method P47()
// ...
-ghost method P54()
+lemma P54()
ensures forall m, n :: minus(add(m, n), n) == m;
{
// the proof of this theorem follows from two lemmas:
- assert forall m, n :: minus(add(n, m), n) == m;
+ assert forall m, n {:autotriggers false} :: minus(add(n, m), n) == m; // FIXME: Why does Autotriggers false make things verify?
assert forall m, n :: add(m, n) == add(n, m);
}
-ghost method P65()
+lemma P65()
ensures forall i, m :: less(i, Suc(add(m, i))) == True;
{
if (*) {
// the proof of this theorem follows from two lemmas:
- assert forall i, m :: less(i, Suc(add(i, m))) == True;
+ assert forall i, m {:autotriggers false} :: less(i, Suc(add(i, m))) == True; // FIXME: Why does Autotriggers false make things verify?
assert forall m, n :: add(m, n) == add(n, m);
} else {
// a different way to prove it uses the following lemma:
@@ -567,12 +567,12 @@ ghost method P65()
}
}
-ghost method P67()
+lemma P67()
ensures forall m, n :: leq(n, add(m, n)) == True;
{
if (*) {
// the proof of this theorem follows from two lemmas:
- assert forall m, n :: leq(n, add(n, m)) == True;
+ assert forall m, n {:autotriggers false} :: leq(n, add(n, m)) == True; // FIXME: Why does Autotriggers false make things verify?
assert forall m, n :: add(m, n) == add(n, m);
} else {
// a different way to prove it uses the following lemma:
@@ -583,19 +583,19 @@ ghost method P67()
// ---------
// Here is a alternate way of writing down the proof obligations:
-ghost method P1_alt(n: Nat, xs: List)
+lemma P1_alt(n: Nat, xs: List)
ensures concat(take(n, xs), drop(n, xs)) == xs;
{
}
-ghost method P2_alt(n: Nat, xs: List, ys: List)
+lemma P2_alt(n: Nat, xs: List, ys: List)
ensures add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys)));
{
}
// ---------
-ghost method Lemma_RevConcat(xs: List, ys: List)
+lemma Lemma_RevConcat(xs: List, ys: List)
ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
{
match (xs) {
@@ -606,7 +606,7 @@ ghost method Lemma_RevConcat(xs: List, ys: List)
}
}
-ghost method Theorem(xs: List)
+lemma Theorem(xs: List)
ensures reverse(reverse(xs)) == xs;
{
match (xs) {
diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 0eaed68c..a6e5e3aa 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Schorr-Waite algorithms, written and verified in Dafny.
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index b29a6829..b0877f9f 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Rustan Leino
@@ -180,7 +180,7 @@ class Main {
ensures forall n :: n in S && n.marked ==>
forall ch :: ch in n.children && ch != null ==> ch.marked
// every marked node was reachable from 'root' in the pre-state:
- ensures forall n :: n in S && n.marked ==> old(Reachable(root, n, S))
+ ensures forall n {:autotriggers false} :: n in S && n.marked ==> old(Reachable(root, n, S))
// the structure of the graph has not changed:
ensures forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
@@ -207,7 +207,7 @@ class Main {
forall j :: 0 <= j < n.childrenVisited ==>
n.children[j] == null || n.children[j].marked
invariant forall n :: n in stackNodes ==> n.childrenVisited < |n.children|
- invariant forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
+ invariant forall n {:autotriggers false} :: n in S && n.marked && n !in stackNodes && n != t ==>
forall ch :: ch in n.children && ch != null ==> ch.marked
invariant forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited)
@@ -219,7 +219,7 @@ class Main {
// every marked node is reachable:
invariant !fresh(path); // needed to show 'path' worthy as argument to old(Reachable(...))
invariant old(ReachableVia(root, path, t, S));
- invariant forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth)
+ invariant forall n, pth {:nowarn} :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth)
invariant forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>
old(ReachableVia(root, pth, n, S))
invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S))
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index da64d004..b9c83aff 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
datatype List = Nil | Cons(Expr, List)
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index a32e6e0b..7ac4e749 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// ultra filter
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 11:26:55 +0000