diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-11 14:20:02 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-11 14:20:02 -0800 |
| commit | eb30557d70adb414dfd0b620c032bc558c5f7fe4 (patch) | |
| tree | 86080b340b86112c7943223c4628c8922e54888c /Test/dafny0 | |
| parent | bf2bd08a7ebecfdec77e5bf64d1a4dda7973bcc6 (diff) | |
Dafny: make full predicate definitions available only inside a module (outside is just an implication: the predicate implies the body known so far)
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 14 | ||||
| -rw-r--r-- | Test/dafny0/Modules1.dfy | 32 |
2 files changed, 45 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 27c97dc2..532330b8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -685,6 +685,18 @@ Modules0.dfy(211,12): Error: match source expression 'l' has already been used a 30 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
+Modules1.dfy(74,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+Modules1.dfy(86,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+Modules1.dfy(88,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0
Execution trace:
(0,0): anon0
@@ -692,7 +704,7 @@ Modules1.dfy(58,3): Error: failure to decrease termination measure Execution trace:
(0,0): anon0
-Dafny program verifier finished with 16 verified, 2 errors
+Dafny program verifier finished with 19 verified, 5 errors
-------------------- BadFunction.dfy --------------------
BadFunction.dfy(6,3): Error: failure to decrease termination measure
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index ad17c7d8..5e2d0fff 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -57,3 +57,35 @@ method Botch1(x: int) {
Botch0(x); // error: failure to decrease termination metric
}
+
+// ------ modules ------------------------------------------------
+
+module A_Visibility {
+ class C {
+ static predicate P(x: int)
+ {
+ 0 <= x
+ }
+ }
+ method Main() {
+ var y;
+ if (C.P(y)) {
+ assert 0 <= y; // this much is known of C.P
+ assert 2 <= y; // error
+ } else {
+ assert C.P(8); // this is fine
+ }
+ }
+}
+
+module B_Visibility imports A_Visibility {
+ method Main() {
+ var y;
+ if (C.P(y)) {
+ assert 0 <= y; // this much is known of C.P
+ assert 2 <= y; // error
+ } else {
+ assert C.P(8); // error: C.P cannot be established outside the declaring module
+ }
+ }
+}
|