summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/VSI-Benchmarks/b1.dfy5
-rw-r--r--Test/dafny0/Answer38
-rw-r--r--Test/dafny0/BinaryTree.dfy4
-rw-r--r--Test/dafny0/Modules0.dfy72
-rw-r--r--Test/dafny0/Modules1.dfy62
-rw-r--r--Test/dafny0/SchorrWaite.dfy6
-rw-r--r--Test/dafny0/SmallTests.dfy2
-rw-r--r--Test/dafny0/Use.dfy8
-rw-r--r--Test/dafny0/runtest.bat2
9 files changed, 174 insertions, 25 deletions
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
index ba293008..70522aaf 100644
--- a/Test/VSI-Benchmarks/b1.dfy
+++ b/Test/VSI-Benchmarks/b1.dfy
@@ -35,8 +35,11 @@ class Benchmark1 {
method Mul(x: int, y: int) returns (r: int)
ensures r == x*y;
+ decreases x < 0, x;
{
- if (x < 0) {
+ if (x == 0) {
+ r := 0;
+ } else if (x < 0) {
call r := Mul(-x, y);
r := -r;
} else {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5dadda4b..ae2aa454 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -6,7 +6,7 @@ class MyClass<T, U> {
var x: int;
method M(s: bool, lotsaObjects: set<object>)
- returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>):
+ returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)
requires s;
modifies this, lotsaObjects;
ensures t == t;
@@ -266,10 +266,24 @@ Execution trace:
Dafny program verifier finished with 21 verified, 29 errors
-------------------- Modules0.dfy --------------------
+Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
-Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
-3 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(51,6): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
+Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
+Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
+Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module $default must transitively import YY)
+7 resolution/type errors detected in Modules0.dfy
+
+-------------------- Modules1.dfy --------------------
+Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
+Execution trace:
+ (0,0): anon0
+Modules1.dfy(61,3): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 16 verified, 2 errors
-------------------- Queue.dfy --------------------
@@ -300,31 +314,31 @@ Dafny program verifier finished with 10 verified, 0 errors
Dafny program verifier finished with 13 verified, 0 errors
-------------------- Use.dfy --------------------
-Use.dfy(15,18): Error: assertion violation
+Use.dfy(14,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(26,18): Error: assertion violation
+Use.dfy(24,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(35,18): Error: assertion violation
+Use.dfy(33,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(56,12): Error: assertion violation
+Use.dfy(52,12): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(88,17): Error: assertion violation
+Use.dfy(82,17): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(130,23): Error: assertion violation
+Use.dfy(124,23): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(144,5): Error: assertion violation
+Use.dfy(136,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(144,5): Error: assertion violation
+Use.dfy(136,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(215,19): Error: assertion violation
+Use.dfy(207,19): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 276b6c0e..714e9d58 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -55,6 +55,7 @@ class IntSet {
ensures n == null ==> fresh(m.footprint) && m.contents == {x};
ensures n != null ==> m == n && n.contents == old(n.contents) + {x};
ensures n != null ==> fresh(n.footprint - old(n.footprint));
+ decreases if n == null then {} else n.footprint;
{
if (n == null) {
m := new Node;
@@ -145,6 +146,7 @@ class Node {
method Find(x: int) returns (present: bool)
requires Valid();
ensures present <==> x in contents;
+ decreases footprint;
{
if (x == data) {
present := true;
@@ -164,6 +166,7 @@ class Node {
ensures node != null ==> node.Valid();
ensures node == null ==> old(contents) <= {x};
ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {x};
+ decreases footprint;
{
node := this;
if (left != null && x < data) {
@@ -201,6 +204,7 @@ class Node {
ensures node == null ==> old(contents) == {min};
ensures node != null ==> node.footprint <= footprint && node.contents == old(contents) - {min};
ensures min in old(contents) && (forall x :: x in old(contents) ==> min <= x);
+ decreases footprint;
{
if (left == null) {
min := data;
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index cf616fba..0e0d3ab3 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -32,3 +32,75 @@ module I imports J {
module J imports G, M {
}
+
+// --------------- calls
+
+module X2 imports X1 {
+ class MyClass2 {
+ method Down(x1: MyClass1, x0: MyClass0) {
+ call x1.Down(x0);
+ }
+ method WayDown(x0: MyClass0, g: ClassG) {
+ call x0.Down();
+ call g.T(); // allowed, because this follows import relation
+ var t := g.TFunc(); // allowed, because this follows import relation
+ }
+ method Up() {
+ }
+ method Somewhere(y: MyClassY) {
+ call y.M(); // error: does not follow import relation
+ }
+ }
+}
+
+module X1 imports X0 {
+ class MyClass1 {
+ method Down(x0: MyClass0) {
+ call x0.Down();
+ }
+ method Up(x2: MyClass2) {
+ call x2.Up(); // error: does not follow import relation
+ }
+ }
+}
+
+module X0 {
+ class MyClass0 {
+ method Down() {
+ }
+ method Up(x1: MyClass1, x2: MyClass2) {
+ call x1.Up(x2); // error: does not follow import relation
+ }
+ }
+}
+
+module YY {
+ class MyClassY {
+ method M() { }
+ method P(g: ClassG) {
+ call g.T(); // allowed, because this follows import relation
+ var t := g.TFunc(); // allowed, because this follows import relation
+ }
+ }
+}
+
+class ClassG {
+ method T() { }
+ function method TFunc(): int { 10 }
+ method V(y: MyClassY) {
+ call y.M(); // error: does not follow import relation
+ }
+}
+
+method Ping() {
+ call Pong(); // allowed: intra-module call
+}
+
+method Pong() {
+ call Ping(); // allowed: intra-module call
+}
+
+method ProcG(g: ClassG) {
+ call g.T(); // allowed: intra-module call
+ var t := g.TFunc(); // allowed: intra-module call
+}
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
new file mode 100644
index 00000000..cfefa7fa
--- /dev/null
+++ b/Test/dafny0/Modules1.dfy
@@ -0,0 +1,62 @@
+module A imports B {
+ class X {
+ function Fx(z: Z): int
+ requires z != null;
+ decreases 5, 4, 3;
+ { z.G() } // fine; this goes to a different module
+ }
+ datatype Y {
+ Cons(int, Y);
+ Empty;
+ }
+}
+
+class C {
+ method M() { }
+ function F(): int { 818 }
+}
+
+method MyMethod() { }
+
+var MyField: int;
+
+module B {
+ class Z {
+ method K() { }
+ function G(): int
+ decreases 10, 8, 6;
+ { 25 }
+ }
+}
+
+static function MyFunction(): int { 5 }
+
+class D { }
+
+method Proc0(x: int)
+ decreases x;
+{
+ if (0 <= x) {
+ call Proc1(x - 1);
+ }
+}
+
+method Proc1(x: int)
+ decreases x;
+{
+ if (0 <= x) {
+ call Proc0(x - 1);
+ }
+}
+
+method Botch0(x: int)
+ decreases x;
+{
+ call Botch1(x - 1); // error: failure to keep termination metric bounded
+}
+
+method Botch1(x: int)
+ decreases x;
+{
+ call Botch0(x); // error: failure to decrease termination metric
+}
diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index f429b9ed..97317792 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -36,6 +36,7 @@ class Main {
requires (forall n :: n in S && n.marked ==>
n in stackNodes ||
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ requires (forall n :: n in stackNodes ==> n != null && n.marked);
modifies S;
ensures root.marked;
// nodes reachable from 'root' are marked:
@@ -46,6 +47,7 @@ class Main {
ensures (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
+ decreases S - stackNodes;
{
if (! root.marked) {
root.marked := true;
@@ -66,6 +68,7 @@ class Main {
{
var c := root.children[i];
if (c != null) {
+ var D := S - stackNodes; assert root in D;
call RecursiveMarkWorker(c, S, stackNodes + {root});
}
i := i + 1;
@@ -146,7 +149,6 @@ class Main {
function Reachable(from: Node, to: Node, S: set<Node>): bool
requires null !in S;
reads S;
- decreases 1;
{
(exists via: Path :: ReachableVia(from, via, to, S))
}
@@ -154,7 +156,7 @@ class Main {
function ReachableVia(from: Node, via: Path, to: Node, S: set<Node>): bool
requires null !in S;
reads S;
- decreases 0, via;
+ decreases via;
{
match via
case Empty => from == to
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index b627df75..ba6c8e0c 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -2,7 +2,7 @@ class Node {
var next: Node;
function IsList(r: set<Node>): bool
- reads r;
+ reads r;
{
this in r &&
(next != null ==> next.IsList(r - {this}))
diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index e006823e..58cb6bea 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -2,7 +2,6 @@ class T {
var x: int;
use function F(y: int): int
- decreases 0;
{
2*y
}
@@ -16,7 +15,6 @@ class T {
}
use function FF(y: int): int
- decreases 1;
{
F(y)
}
@@ -36,12 +34,10 @@ class T {
}
use function G(y: int): bool
- decreases 0;
{
0 <= y
}
use function GG(y: int): bool
- decreases 1;
{
G(y)
}
@@ -58,13 +54,11 @@ class T {
use function H(): int
reads this;
- decreases 0;
{
x
}
use function HH(): int
reads this;
- decreases 1;
{
H()
}
@@ -133,13 +127,11 @@ class T {
use function K(): bool
reads this;
- decreases 0;
{
x <= 100
}
use function KK(): bool
reads this;
- decreases 1;
{
K()
}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 2bec0a4d..003566f3 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (BQueue.bpl) do (
)
for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy
- Modules0.dfy Queue.dfy ListCopy.dfy
+ Modules0.dfy Modules1.dfy Queue.dfy ListCopy.dfy
BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 20:13:52 +0000