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/Modules1.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/Modules1.dfy')
| -rw-r--r-- | Test/dafny0/Modules1.dfy | 62 |
1 files changed, 62 insertions, 0 deletions
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
+}
|