diff options
-rw-r--r-- | Binaries/DafnyPrelude.bpl | 9 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 1 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 2 | ||||
-rw-r--r-- | Test/dafny1/ListContents.dfy | 2 | ||||
-rw-r--r-- | Test/dafny1/SchorrWaite.dfy | 1 | ||||
-rw-r--r-- | Test/vacid0/Composite.dfy | 1 | ||||
-rw-r--r-- | Test/vacid0/LazyInitArray.dfy | 2 | ||||
-rw-r--r-- | Test/vacid0/SparseArray.dfy | 2 |
8 files changed, 9 insertions, 11 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 520f9c77..eeb4f103 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -153,7 +153,7 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) } 0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
(Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));
-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) }
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}
0 <= j && j < n && j < Seq#Length(s) ==>
Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
@@ -162,10 +162,15 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) } 0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
(Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));
-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }
+axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}
0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
+axiom (forall<T> s, t: Seq T ::
+ { Seq#Append(s, t) }
+ Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&
+ Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);
+
// ---------------------------------------------------------------
// -- If then else -----------------------------------------------
// ---------------------------------------------------------------
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 19f54d94..bb88b265 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -94,7 +94,6 @@ class Benchmark3 { call r.Enqueue(m);
pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]];
}
- assert (forall i :: 0 <= i && i < |perm| ==> perm[i] == pperm[i]); //lemma needed to trigger axiom
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index fdb23379..80d6b8d6 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -105,9 +105,7 @@ class Map<Key,Value> { call p, n, prev := FindIndex(key);
if (p != null) {
Keys := Keys[..n] + Keys[n+1..];
- assert Keys[..n] == old(Keys)[..n] && Keys[n..] == old(Keys)[n+1..];
Values := Values[..n] + Values[n+1..];
- assert Values[..n] == old(Values)[..n] && Values[n..] == old(Values)[n+1..];
nodes := nodes[..n] + nodes[n+1..];
if (prev == null) {
head := head.next;
diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy index 62636ce5..f672950b 100644 --- a/Test/dafny1/ListContents.dfy +++ b/Test/dafny1/ListContents.dfy @@ -78,10 +78,8 @@ class Node<T> { decreases if current != null then |current.list| else -1;
{
var nx := current.next;
- assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma
// ..., reverse, current, nx, ...
- assert current.data == current.list[0]; // lemma
current.next := reverse;
current.footprint := {current} + reverse.footprint;
current.list := [current.data] + reverse.list;
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index 3e64a4bd..52db9dca 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -67,7 +67,6 @@ class Main { {
var c := root.children[i];
if (c != null) {
- ghost var D := S - stackNodes; assert root in D;
call RecursiveMarkWorker(c, S, stackNodes + {root});
}
i := i + 1;
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy index ca5f206b..87e63e2c 100644 --- a/Test/vacid0/Composite.dfy +++ b/Test/vacid0/Composite.dfy @@ -91,7 +91,6 @@ class Composite { var p := parent;
parent := null;
if (p != null) {
- assert (p.left == this) != (p.right == this);
if (p.left == this) {
p.left := null;
} else {
diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy index 6ae00e24..c5a032fe 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -89,7 +89,7 @@ class LazyInitArray<T> { {
if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
} else {
- assert n <= e[i];
+ assert n <= e[i]; // lemma
b[i] := n;
c[n] := i;
ghost var t := d[n];
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index 0e6aff05..2c217264 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -87,7 +87,7 @@ class SparseArray<T> { {
if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
} else {
- assert n <= e[i];
+ assert n <= e[i]; // lemma
b := b[i := n];
c := c[n := i];
ghost var t := d[n];
|