diff options
-rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 3 | ||||
-rw-r--r-- | Test/dafny0/RefinementErrors.dfy | 37 | ||||
-rw-r--r-- | Test/dafny0/RefinementErrors.dfy.expect | 3 |
3 files changed, 39 insertions, 4 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 2d32f78a..f430933b 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -1532,9 +1532,6 @@ namespace Microsoft.Dafny });
} else if (s is CallStmt) {
reporter.Error(s.Tok, "cannot have call statement");
- } else if (s is ForallStmt) {
- if (((ForallStmt)s).Kind == ForallStmt.ParBodyKind.Assign) // allow Proof and Call (as neither touch any existing state)
- reporter.Error(s.Tok, "cannot have forall statement");
} else {
if (s is WhileStmt || s is AlternativeLoopStmt) {
loopLevels++;
diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy index 121b33aa..8d60a8e4 100644 --- a/Test/dafny0/RefinementErrors.dfy +++ b/Test/dafny0/RefinementErrors.dfy @@ -59,3 +59,40 @@ module BB refines B { { 10 } } } + +module Forall0 { + class C { + var a: int + method M() + modifies this + { + } + lemma Lemma(x: int) + { + } + } +} +module Forall1 refines Forall0 { + class C { + var b: int + method M... + { + forall x { Lemma(x); } // allowed + var s := {4}; + forall x | x in s ensures x == 4 { } // allowed + forall x { // allowed + calc { + x in s; + == + x == 4; + } + } + forall c | c in {this} { + c.b := 17; // allowed + } + forall c | c in {this} { + c.a := 17; // error: not allowed to update previously defined field + } + } + } +} diff --git a/Test/dafny0/RefinementErrors.dfy.expect b/Test/dafny0/RefinementErrors.dfy.expect index 40cdb081..bac6612d 100644 --- a/Test/dafny0/RefinementErrors.dfy.expect +++ b/Test/dafny0/RefinementErrors.dfy.expect @@ -9,4 +9,5 @@ RefinementErrors.dfy(38,13): Error: type parameters are not allowed to be rename RefinementErrors.dfy(39,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')
RefinementErrors.dfy(40,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines
RefinementErrors.dfy(57,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G
-11 resolution/type errors detected in RefinementErrors.dfy
+RefinementErrors.dfy(94,10): Error: refinement method cannot assign to a field defined in parent module ('a')
+12 resolution/type errors detected in RefinementErrors.dfy
|