diff options
| author |  rustanleino <unknown> | 2010-03-16 08:53:22 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-16 08:53:22 +0000 |
| commit | 6766d9d3d836ca3d435ae87c4b3fe71a1741fcf4 (patch) | |
| tree | fc1103759db2b9b5fe551564f050b7705f143fc0 /Test/dafny0/SmallTests.dfy | |
| parent | cc63641cd0211b2f585330c9d65208665671991b (diff) | |
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
Diffstat (limited to 'Test/dafny0/SmallTests.dfy')
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
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}))
|