summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/Answer2
-rw-r--r--Test/dafny0/Compilation.dfy52
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();
+ }
+}