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 | aa1db181e9aa277a1cca3c7f3e54c0f2b0d19d41 (patch) | |
| tree | 49c594018fb786cd53c394978c43677604f0c90d /Test | |
| parent | 20bbf073f2dd3801933c484b5670be164ebd4015 (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')
| -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
+ }
+ }
+}
|