Added support for 'dirty' forall statements.

One can now write forall statements without bodies
(but with ensures clauses) as follows:

forall s | s in S ensures s < 0;

where S is set<int>.

The ensures clauses are assumed but not checked.

1 files changed, 7 insertions, 0 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index e49f9823..f3297ed7 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -905,3 +905,10 @@ module LhsLvalue {
 

   method MyLemma() returns (w: int)

 }

+

+// ------------------- dirty loops -------------------

+

+method DirtyM(S: set<int>) {

+  forall s | s in S ensures s < 0;

+  assert s < 0; // error: s is unresolved

+}