summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/VSI-Benchmarks/b3.dfy10
-rw-r--r--Test/VSI-Benchmarks/b4.dfy15
-rw-r--r--Test/VSI-Benchmarks/b6.dfy22
-rw-r--r--Test/VSI-Benchmarks/b7.dfy10
-rw-r--r--Test/VSI-Benchmarks/b8.dfy53
-rw-r--r--Test/dafny0/Answer8
-rw-r--r--Test/dafny0/TypeParameters.dfy44
7 files changed, 102 insertions, 60 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 4f717f48..4f44612d 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -13,22 +13,22 @@
//would be nice if we could mark pperm as a ghost variable
class Queue<T> {
- var contents: seq<int>;
+ var contents: seq<T>;
method Init();
modifies this;
ensures |contents| == 0;
- method Enqueue(x: int);
+ method Enqueue(x: T);
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: int);
+ method Dequeue() returns (x: T);
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
- function Head(): int
+ function Head(): T
requires 0 < |contents|;
reads this;
{ contents[0] }
- function Get(i: int): int
+ function Get(i: int): T
requires 0 <= i && i < |contents|;
reads this;
{ contents[i] }
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index 5a9d46c8..e3a99884 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -43,16 +43,10 @@ class Map<Key,Value> {
requires Valid();
modifies this;
ensures Valid();
- // no key is lost:
- ensures (forall k :: k in old(keys) ==> k in keys);
- // at most one key is introduced:
- ensures (forall k :: k in keys ==> k in old(keys) || k == key);
- // the given key has the given value:
- ensures (exists i :: 0 <= i && i < |keys| &&
- keys[i] == key && values[i] == val);
- // other values don't change:
- ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
- values[i] == old(values)[i]);
+ ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>
+ keys[i] == key && values[i] == val &&
+ (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
+ ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
{
call j := FindIndex(key);
if (j == -1) {
@@ -60,7 +54,6 @@ class Map<Key,Value> {
values := values + [val];
assert values[|keys|-1] == val; // lemma
} else {
- keys := keys[..j] + [key] + keys[j+1..];
values := values[..j] + [val] + values[j+1..];
assert values[j] == val; //lemma
}
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index 48306e9b..d320f9e9 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -1,7 +1,7 @@
-class Collection {
+class Collection<T> {
var footprint:set<object>;
- var elements:seq<int>;
+ var elements:seq<T>;
function Valid():bool
reads this, footprint;
@@ -24,7 +24,7 @@ class Collection {
footprint := {this};
}
- method GetItem(i:int ) returns (x:int)
+ method GetItem(i:int ) returns (x:T)
requires Valid();
requires 0<=i && i<|elements|;
ensures elements[i] ==x;
@@ -32,7 +32,7 @@ class Collection {
x:=elements[i];
}
- method Add(x:int )
+ method Add(x:T )
requires Valid();
modifies footprint;
ensures Valid() && fresh(footprint - old(footprint));
@@ -41,21 +41,21 @@ class Collection {
elements:= elements + [x];
}
- method GetIterator() returns (iter:Iterator)
+ method GetIterator() returns (iter:Iterator<T>)
requires Valid();
ensures iter != null && iter.Valid();
ensures fresh(iter.footprint) && iter.pos == -1;
ensures iter.c == this;
{
- iter:= new Iterator;
+ iter:= new Iterator<T>;
call iter.Init(this);
}
}
-class Iterator {
+class Iterator<T> {
- var c:Collection;
+ var c:Collection<T>;
var pos:int;
var footprint:set<object>;
@@ -66,7 +66,7 @@ class Iterator {
this in footprint && c!= null && -1<= pos && null !in footprint
}
- method Init(coll:Collection)
+ method Init(coll:Collection<T>)
requires coll != null;
modifies this;
ensures Valid() && fresh(footprint -{this}) && pos ==-1;
@@ -94,7 +94,7 @@ class Iterator {
0<= pos && pos < |c.elements|
}
- method GetCurrent() returns (x:int)
+ method GetCurrent() returns (x:T)
requires Valid() && HasCurrent();
ensures c.elements[pos] == x;
{
@@ -108,7 +108,7 @@ class Client
method Main()
{
- var c:= new Collection;
+ var c:= new Collection<int>;
call c.Init();
call c.Add(33);
call c.Add(45);
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index f7d51058..ddad7599 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -7,22 +7,22 @@
class Queue<T> {
- var contents: seq<int>;
+ var contents: seq<T>;
method Init();
modifies this;
ensures |contents| == 0;
- method Enqueue(x: int);
+ method Enqueue(x: T);
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: int);
+ method Dequeue() returns (x: T);
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
- function Head(): int
+ function Head(): T
requires 0 < |contents|;
reads this;
{ contents[0] }
- function Get(i: int): int
+ function Get(i: int): T
requires 0 <= i && i < |contents|;
reads this;
{ contents[i] }
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 51172419..c3374605 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -5,22 +5,22 @@
// the following words (until we read null) form the terms definition. Then the stream provides the next term etc.
class Queue<T> {
- var contents: seq<Word>;
+ var contents: seq<T>;
method Init();
modifies this;
ensures |contents| == 0;
- method Enqueue(x: Word);
+ method Enqueue(x: T);
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: Word);
+ method Dequeue() returns (x: T);
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
- function Head(): Word
+ function Head(): T
requires 0 < |contents|;
reads this;
{ contents[0] }
- function Get(i: int): Word
+ function Get(i: int): T
requires 0 <= i && i < |contents|;
reads this;
{ contents[i] }
@@ -56,18 +56,20 @@ class Glossary {
invariant glossary.Valid();
invariant glossary !in rs.footprint;
invariant null !in glossary.keys;
- //to do add invariant invariant (forall d:: d in glossary.values ==>!(null in d)); ***
+ invariant (forall d :: d in glossary.values ==> null !in d);
invariant q !in rs.footprint;
- // ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)
+ invariant q.contents == glossary.keys;
// we leave out the decreases clause - unbounded stream
{
call term,definition := readDefinition(rs);
- if (term == null)
- {
+ if (term == null) {
break;
- }
- call glossary.Add(term,definition);
- call q.Enqueue(term);
+ }
+ call present, d := glossary.Find(term);
+ if (!present) {
+ call glossary.Add(term,definition);
+ call q.Enqueue(term);
+ }
}
call rs.Close();
@@ -79,12 +81,14 @@ class Glossary {
invariant wr.Valid() && fresh(wr.footprint);
invariant glossary.Valid();
invariant glossary !in wr.footprint && null !in glossary.keys;
+ invariant (forall d :: d in glossary.values ==> null !in d);
invariant q !in wr.footprint;
+ invariant (forall k :: k in q.contents ==> k in glossary.keys);
decreases |q.contents|;
{
- call term:= q.Dequeue();
- call present,definition:= glossary.Find(term);
- assume present; // to change this into an assert we need the loop invariant ** above that we commented out
+ call term := q.Dequeue();
+ call present,definition := glossary.Find(term);
+ assert present;
// write term with a html anchor
call wr.PutWordInsideTag(term, term);
@@ -95,12 +99,13 @@ class Glossary {
invariant wr.Valid() && fresh(wr.footprint);
invariant glossary.Valid();
invariant glossary !in wr.footprint && null !in glossary.keys;
+ invariant (forall d :: d in glossary.values ==> null !in d);
invariant q !in wr.footprint;
invariant qcon == q.contents;
+ invariant (forall k :: k in q.contents ==> k in glossary.keys);
decreases |definition| -i;
{
var w := definition[i];
- assume w != null; // to convert this into an assert we need invariant *** above
call present, d := glossary.Find(w);
if (present)
{
@@ -130,6 +135,7 @@ class Glossary {
while (true)
invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));
invariant null !in definition;
+ // we leave out the decreases clause - unbounded stream
{
call w := rs.GetWord();
if (w == null)
@@ -283,16 +289,10 @@ class Map<Key,Value> {
requires Valid();
modifies this;
ensures Valid();
- // no key is lost:
- ensures (forall k :: k in old(keys) ==> k in keys);
- // at most one key is introduced:
- ensures (forall k :: k in keys ==> k in old(keys) || k == key);
- // the given key has the given value:
- ensures (exists i :: 0 <= i && i < |keys| &&
- keys[i] == key && values[i] == val);
- // other values don't change:
- ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
- values[i] == old(values)[i]);
+ ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>
+ keys[i] == key && values[i] == val &&
+ (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
+ ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
{
call j := FindIndex(key);
if (j == -1) {
@@ -300,7 +300,6 @@ class Map<Key,Value> {
values := values + [val];
assert values[|keys|-1] == val; // lemma
} else {
- keys := keys[..j] + [key] + keys[j+1..];
values := values[..j] + [val] + values[j+1..];
assert values[j] == val; //lemma
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 64c43c87..78982f01 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -96,5 +96,11 @@ Execution trace:
Dafny program verifier finished with 5 verified, 3 errors
-------------------- TypeParameters.dfy --------------------
+TypeParameters.dfy(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ (0,0): anon0
+TypeParameters.dfy(63,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 7 verified, 2 errors
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 3f57f369..794f2f95 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -19,3 +19,47 @@ class C<U> {
function G<Y>(): Y;
}
+
+class SetTest {
+ method Add<T>(s: set<T>, x: T) returns (t: set<T>)
+ ensures t == s + {x};
+ {
+ t := s + {x};
+ }
+
+ method Good()
+ {
+ var s := {2, 5, 3};
+ call t := Add(s, 7);
+ assert {5,7,2,3} == t;
+ }
+
+ method Bad()
+ {
+ var s := {2, 50, 3};
+ call t := Add(s, 7);
+ assert {5,7,2,3} == t; // error
+ }
+}
+
+class SequenceTest {
+ method Add<T>(s: seq<T>, x: T) returns (t: seq<T>)
+ ensures t == s + [x];
+ {
+ t := s + [x];
+ }
+
+ method Good()
+ {
+ var s := [2, 5, 3];
+ call t := Add(s, 7);
+ assert [2,5,3,7] == t;
+ }
+
+ method Bad()
+ {
+ var s := [2, 5, 3];
+ call t := Add(s, 7);
+ assert [2,5,7,3] == t || [2,5,3] == t;
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 23:31:41 +0000