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

0 files changed, 0 insertions, 0 deletions