Dafny: firmed up the module system

1 files changed, 33 insertions, 0 deletions

diff --git a/Test/dafny0/ModulesCycle.dfy b/Test/dafny0/ModulesCycle.dfy
new file mode 100644
index 00000000..a7f1caa2
--- /dev/null
+++ b/Test/dafny0/ModulesCycle.dfy
@@ -0,0 +1,33 @@
+module M {

+  class T { }

+  class U { }

+}

+

+module N {

+}

+

+module U imports N {

+}

+

+module V imports T {  // error: T is not a module

+}

+

+module A imports B, M {

+  class Y { }

+}

+

+module B imports N, M {

+  class X { }

+}

+

+module G imports A, M, A, H, B {  // error: cycle in import graph

+}

+

+module H imports A, N, I {

+}

+

+module I imports J {

+}

+

+module J imports G, M {

+}