diff options
| author |  qunyanm <unknown> | 2016-01-29 13:01:02 -0800 |
|---|---|---|
| committer | qunyanm <unknown> | 2016-01-29 13:01:02 -0800 |
| commit | e4da5fcd52bbdd0b8345056a3475333d6e27e65f (patch) | |
| tree | 243761b75f83fa1d74bce22a91e2d2a2316e1cf2 /Test | |
| parent | 7fb4b7f9ad53ad793eb7a66cf5ca89499d275121 (diff) | |
Implement module export so we can export a subset of items defined in the
module.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/ModuleExport.dfy | 68 | ||||
| -rw-r--r-- | Test/dafny0/ModuleExport.dfy.expect | 9 |
2 files changed, 77 insertions, 0 deletions
diff --git a/Test/dafny0/ModuleExport.dfy b/Test/dafny0/ModuleExport.dfy new file mode 100644 index 00000000..81fe0ed5 --- /dev/null +++ b/Test/dafny0/ModuleExport.dfy @@ -0,0 +1,68 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module A {
+ default export Public { f, h}
+ export E1 { f, g}
+ export E2 extends Public, E1 {T}
+ export Friend extends Public {g, T}
+ export Fruit {Data}
+
+ method h() {}
+ function f(): int { 818 }
+ function g() : int { 819 }
+ function k() : int { 820 }
+
+ class T
+ {
+ static method l() {}
+ }
+
+ datatype Data = Lemon | Kiwi(int)
+
+}
+
+module B {
+ import X = A.Public
+ method m() {
+ X.h(); // OK
+ assert X.f() == 818; // OK
+ assert X.g() == 819; // error
+ assert X.k() == 820; // error
+ X.T.l(); // error
+ }
+}
+
+module C {
+ import X = A.Friend
+ method m() {
+ X.h(); // OK
+ assert X.f() == 818; // OK
+ assert X.g() == 819; // OK
+ assert X.k() == 820; // error
+ X.T.l(); // OK
+ }
+}
+
+module D {
+ import opened A
+ method m() {
+ h(); // OK
+ assert f() == 818; // OK
+ assert g() == 819; // error
+ assert k() == 820; // error
+ }
+}
+
+module E {
+ import opened A.Fruit
+
+ function G(d: Data): int
+ requires d != Data.Lemon
+ {
+ match d
+ case Lemon => G(d)
+ case Kiwi(x) => 7
+ case Orang => 8 // error
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/ModuleExport.dfy.expect b/Test/dafny0/ModuleExport.dfy.expect new file mode 100644 index 00000000..c7444bdb --- /dev/null +++ b/Test/dafny0/ModuleExport.dfy.expect @@ -0,0 +1,9 @@ +ModuleExport.dfy(30,11): Error: unresolved identifier: g
+ModuleExport.dfy(31,11): Error: unresolved identifier: k
+ModuleExport.dfy(32,4): Error: unresolved identifier: T
+ModuleExport.dfy(32,7): Error: expected method call, found expression
+ModuleExport.dfy(42,11): Error: unresolved identifier: k
+ModuleExport.dfy(52,9): Error: unresolved identifier: g
+ModuleExport.dfy(53,9): Error: unresolved identifier: k
+ModuleExport.dfy(66,2): Error: member Orang does not exist in datatype Data
+8 resolution/type errors detected in ModuleExport.dfy
|