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/VSI-Benchmarks | |
| 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/VSI-Benchmarks')
| -rw-r--r-- | Test/VSI-Benchmarks/b1.dfy | 5 |
1 files changed, 4 insertions, 1 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 {
|