From 6766d9d3d836ca3d435ae87c4b3fe71a1741fcf4 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 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Test/VSI-Benchmarks') 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 { -- cgit v1.2.3