diff options
Diffstat (limited to 'Test/dafny0')
-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();
+ }
+}
|