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/Modules0.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/Modules0.dfy')
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index cf616fba..0e0d3ab3 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -32,3 +32,75 @@ module I imports J { module J imports G, M {
}
+
+// --------------- calls
+
+module X2 imports X1 {
+ class MyClass2 {
+ method Down(x1: MyClass1, x0: MyClass0) {
+ call x1.Down(x0);
+ }
+ method WayDown(x0: MyClass0, g: ClassG) {
+ call x0.Down();
+ call g.T(); // allowed, because this follows import relation
+ var t := g.TFunc(); // allowed, because this follows import relation
+ }
+ method Up() {
+ }
+ method Somewhere(y: MyClassY) {
+ call y.M(); // error: does not follow import relation
+ }
+ }
+}
+
+module X1 imports X0 {
+ class MyClass1 {
+ method Down(x0: MyClass0) {
+ call x0.Down();
+ }
+ method Up(x2: MyClass2) {
+ call x2.Up(); // error: does not follow import relation
+ }
+ }
+}
+
+module X0 {
+ class MyClass0 {
+ method Down() {
+ }
+ method Up(x1: MyClass1, x2: MyClass2) {
+ call x1.Up(x2); // error: does not follow import relation
+ }
+ }
+}
+
+module YY {
+ class MyClassY {
+ method M() { }
+ method P(g: ClassG) {
+ call g.T(); // allowed, because this follows import relation
+ var t := g.TFunc(); // allowed, because this follows import relation
+ }
+ }
+}
+
+class ClassG {
+ method T() { }
+ function method TFunc(): int { 10 }
+ method V(y: MyClassY) {
+ call y.M(); // error: does not follow import relation
+ }
+}
+
+method Ping() {
+ call Pong(); // allowed: intra-module call
+}
+
+method Pong() {
+ call Ping(); // allowed: intra-module call
+}
+
+method ProcG(g: ClassG) {
+ call g.T(); // allowed: intra-module call
+ var t := g.TFunc(); // allowed: intra-module call
+}
|