diff options
| author |  Jason Koenig <unknown> | 2012-07-17 15:35:27 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-17 15:35:27 -0700 |
| commit | caf298f8cab0138c0dde7328b0565642094256a7 (patch) | |
| tree | 1e517562f5ce6bcdcee2d648e3695ece7462511b /Test | |
| parent | 7c5b29cfb26c4fe04de732ae7f79d12d840c679e (diff) | |
Dafny: compilation of abstract modules, including local definitions (as in module A as B = C)
* * *
Dafny: compilation of abstract modules, including local definitions (as in module A as B = C)
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 52 |
2 files changed, 53 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 41a42319..cfa79f1a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1917,5 +1917,5 @@ Execution trace: Dafny program verifier finished with 19 verified, 2 errors
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 23 verified, 0 errors
Compiled assembly into Compilation.exe
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index bf21432f..fe6eda47 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -57,3 +57,55 @@ module CoRecursion { }
}
}
+
+ghost module S {
+ class C {
+ var f: int;
+ method m()
+ }
+}
+
+module T refines S {
+ class C {
+ method m() {
+ print "in T.C.m()";
+ }
+ }
+}
+module A {
+ module X as S = T;
+ module Y as S = T;
+ module Z = T;
+ static method run() {
+ var x := new X.C;
+ x.m();
+ var y := new Y.C;
+ y.m();
+ var z := new Z.C;
+ z.m();
+ }
+}
+
+method NotMain() {
+ A.run();
+}
+
+
+ghost module S1 {
+ module B as S = T;
+ static method do()
+}
+
+module T1 refines S1 {
+ static method do() {
+ var x := 3;
+ }
+}
+module A1 {
+ module X as S1 = T1;
+ static method run() {
+ X.do();
+ var x := new X.B.C;
+ x.m();
+ }
+}
|