From 08a4a9054ea4651f409ca7275a70dca67b4254cf Mon Sep 17 00:00:00 2001 From: rustanleino Date: Tue, 16 Mar 2010 08:53:22 +0000 Subject: Dafny: * Added modules with imports. These can be used to deal with termination checks without going into method/function implementations. Imports must be acyclic. * Added a default module. It contains all classes/datatypes defined outside the lexical scope of any other module. * Added a default class. It contains all class members defined outside the lexical scope of any module and class. This means that one can write small Dafny programs without any mention of a "class"! * Revised scheme for termination metrics. Inter-module calls are allowed iff they follow the import relation. Intra-module calls where the callee is in another strongly connected component of the call graph are always allowed. Intra-module calls in the same strongly connected component are verified to terminate via decreases clauses. * Removed previous hack that allowed methods with no decreases clauses not to be subjected to termination checking. * Removed or simplified decreases clauses in test suite, where possible. * Fixed error in Test/VSI-Benchmarks/b1.dfy --- Test/VSI-Benchmarks/b1.dfy | 5 +++- Test/dafny0/Answer | 38 ++++++++++++++++-------- Test/dafny0/BinaryTree.dfy | 4 +++ Test/dafny0/Modules0.dfy | 72 +++++++++++++++++++++++++++++++++++++++++++++ Test/dafny0/Modules1.dfy | 62 ++++++++++++++++++++++++++++++++++++++ Test/dafny0/SchorrWaite.dfy | 6 ++-- Test/dafny0/SmallTests.dfy | 2 +- Test/dafny0/Use.dfy | 8 ----- Test/dafny0/runtest.bat | 2 +- 9 files changed, 174 insertions(+), 25 deletions(-) create mode 100644 Test/dafny0/Modules1.dfy (limited to 'Test') 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 { var x: int; method M(s: bool, lotsaObjects: set) - returns (t: object, u: set, v: seq>): + returns (t: object, u: set, v: seq>) 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): 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): 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): 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 -- cgit v1.2.3