diff options
| author |  Rustan Leino <unknown> | 2013-07-29 14:35:27 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-07-29 14:35:27 -0700 |
| commit | 059ee1934382d1f2332b478d79b8a364ce8a002e (patch) | |
| tree | 961592fb7b7c5f7e352e132034d1fb4dded021a3 /Test/dafny0/OpaqueFunctions.dfy | |
| parent | fb6c171957142ce6119a7363d3cec66799b9966a (diff) | |
Make functions and predicates be opaque outside the defining module -- only their specifications (e.g., ensures clauses) are exported.
Diffstat (limited to 'Test/dafny0/OpaqueFunctions.dfy')
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy | 123 |
1 files changed, 123 insertions, 0 deletions
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy new file mode 100644 index 00000000..c15515d2 --- /dev/null +++ b/Test/dafny0/OpaqueFunctions.dfy @@ -0,0 +1,123 @@ +module A {
+ class C {
+ var x: int;
+ predicate Valid()
+ reads this;
+ {
+ 0 <= x
+ }
+ function Get(): int
+ reads this;
+ {
+ x
+ }
+ constructor ()
+ modifies this;
+ ensures Valid();
+ {
+ x := 8;
+ }
+ method M()
+ requires Valid();
+ {
+ assert Get() == x;
+ assert x == 8; // error
+ }
+ }
+}
+module A' refines A {
+ class C {
+ predicate Valid...
+ {
+ x == 8
+ }
+ method N()
+ requires Valid();
+ {
+ assert Get() == x;
+ assert x == 8;
+ }
+ }
+}
+
+module B {
+ import X as A
+ method Main() {
+ var c := new X.C();
+ c.M(); // fine
+ c.x := c.x + 1;
+ c.M(); // error, because Valid() is opaque
+ }
+ method L(c: X.C)
+ requires c != null;
+ modifies c;
+ {
+ assert c.Get() == c.x; // error because Get() s opaque
+ if * {
+ assert c.Valid(); // error, because Valid() is opaque
+ } else if * {
+ c.x := 7;
+ assert c.Valid(); // error, because Valid() is opaque
+ } else {
+ c.x := 8;
+ assert c.Valid(); // error, because Valid() is opaque
+ }
+ }
+}
+module B_direct {
+ import X as A'
+ method Main() {
+ var c := new X.C();
+ c.M(); // fine
+ c.x := c.x + 1;
+ if * {
+ assert c.Valid(); // error, because Valid() is opaque
+ } else {
+ c.M(); // error, because Valid() is opaque
+ }
+ }
+ method L(c: X.C)
+ requires c != null;
+ modifies c;
+ {
+ assert c.Get() == c.x; // error because Get() s opaque
+ if * {
+ assert c.Valid(); // error, because Valid() is opaque
+ } else if * {
+ c.x := 7;
+ assert c.Valid(); // error, because Valid() is opaque
+ } else {
+ c.x := 8;
+ assert c.Valid(); // error, because Valid() is opaque
+ }
+ }
+}
+module B' refines B {
+ import X = A' // this by itself produces no more error
+ method Main'() {
+ var c := new X.C();
+ c.M(); // fine
+ c.x := c.x + 1;
+ if * {
+ assert c.Valid(); // error, because Valid() is opaque
+ } else {
+ c.M(); // error, because Valid() is opaque
+ }
+ }
+ method L'(c: X.C)
+ requires c != null;
+ modifies c;
+ {
+ assert c.Get() == c.x; // error because Get() s opaque
+ if * {
+ assert c.Valid(); // error, because Valid() is opaque
+ } else if * {
+ c.x := 7;
+ assert c.Valid(); // error, because Valid() is opaque
+ } else {
+ c.x := 8;
+ assert c.Valid(); // error, because Valid() is opaque
+ }
+ }
+}
+
|