feat: Allow forall statements in statement expressions

[RustanLeino]

This PR adds forall statements to the statements supported in StmtExprs. Previously, one had to write

assert forall x | R(x) :: P(x) by {
  forall x | R(x)
    ensures P(x)
  {
    // proof that R(x) ==> P(x)
  }
}
ExprBody

as an expression. Now, one can simply write

forall x | R(x)
  ensures P(x)
{
  // proof that R(x) ==> P(x)
}
ExprBody

The PR also deprecates the ancient syntax where parentheses enclosing the bound variables in the forall statement.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

Two minor issues. Overall good implementation.

[MikaelMayer]

That works. It means we could theoretically do the same for if statements (last week I would have loved to have that) and I think that could be useful too and less surprising in the future, although out of scope for this PR.

[RustanLeino]

I agree it's out of scope for this PR, but I do find it an interesting idea. I suppose such an if statement would still just be for the StmtExpr, rather than being an alternative syntax for if-then-else expressions? This would then allow you to write some proofs inside the if statement and follow that by the expression you want to return. (I have never felt the need for this myself, but perhaps only because I knew the feature wasn't available.)

Some new users confuse if-then-else expressions and if statements (which, curiously, seems not to be a confusion in languages that use the more cryptic ? : for the former). On one hand, also allowing if statements in expressions might add to that confusion. But on the other hand, maybe this would give us a place in the parser to give a better error message if the program gets this wrong.

While we're thinking about such things, one could also imagine other statements, in particular while loops, in expressions. Again, such a while statement would just be for the StmtExpr, to allow an inline proof that uses a loop.

[MikaelMayer]

I'd rather remove the parentheses on our test suite. LLMs are going to learn from it :-)
To test the warning message, prefer a dedicated file that includes deprecated in its name and make sure to put as a comment where you expect the warning

[RustanLeino]

Okay, I'll remove them from this place, too. (I had kept them in one place in order to test the warning message, but I agree with you that we're better served by not teaching LLMs out there deprecated syntax.)

[RustanLeino]

Here's what I did, following your remark: I moved the forall-statement deprecation tests to dafny0/Deprecation.dfy (and added some more such tests). And I added comments on the lines in the test file to indicate where we expect error messages.

I also renamed the Parallel*.dfy tests ForallStmt*.dfy. (Originally, the forall statement had been named foreach. But that suggests a sequential ordering. So, the statement was renamed parallel. This confused people, so (years ago) the statement was once again renamed to the current forall.)

[keyboardDrummer]

IMO the way Dafny defines expressions and statement is unnecessarily confusing and we should resolve that. Many concepts occur both in the expression and the statement space, but either behave or appear slightly differently, and then some things that behave like statements are also available in expressions using "statement expressions", which I've never seen before in a language and IMO goes against the concept of an expression: that execution order is not relevant to its semantics.

I think part of the solution is to merge Dafny functions and methods: allowing methods to be called where currently only functions can be, removing the need for functions. This requires proving that the method is pure, that it has no side-effects and behaves deterministically, which is something we currently do not support, but I think it would be a great improvement.

I'm hopeful this would allow removing statement expressions, even though they could still be useful in contracts to prove preconditions of calls that occur in them.

I'm not a big fan of var expressions, since they look like variables while they do not behave like them: they're not reassignable. I also think the order is incorrect: when working with expressions the declarations should be specified top down, the top-level expression first, and the subexpressions later, similar to how where in Haskell works.

For if statements and expressions, I think the problem is that the keywords are the same but the syntax is different. Either we should unify the syntax, or introduce separate keywords/operators.

In conclusion, I would rather have us focus our efforts on removing the need for statements expressions, than expanding what's possible with them.

[RustanLeino]

@keyboardDrummer I disagree on many accounts.

It's not surprising that you haven't seen statement expressions in other languages, since their only purpose is to introduce information to the verifier. Dafny also has by clauses and witness clauses, which give information to the verifier, and these do not exist in languages that are not focused on verification.

Dafny has a clean separation between expressions and statements. This lets the language distinguish between effectful things and "pure" things. It is difficult to achieve such a separation in a language that only has, say, methods -- for example, in Java, it is difficult to define what a "pure method" would be, with a definition that allows the method to be used in expressions suitable for the verifier. Merging expressions and statements in Dafny would only make Dafny unsuitable for verification.

Note that the statements that are allowed in statement expressions are like lemmas in that they don't change the program state.

Do you have a suggestion for a new keyword for either if statements or if-then-else expressions?

Variables are introduced with the var keyword. But those variables introduced in an expression are not mutable.

Back to the forall statement. There is sometimes a need to introduce universally quantified information for the verifier. Today, that can be done in expressions only by the clumsy assert forall ... by { forall ... { ... } } construction shown in the description of this PR. The only reason forall statements were not among the statements allowed in a statement expression before was that they appeared to introduce parsing problems. As this PR demonstrates, it is not difficult to change the grammar to distinguish between forall expressions and forall statements. Hence, the feature introduced by this PR is a win for the customer, and I think it rather makes the language more consistent rather than polluting it with another feature.

[keyboardDrummer]

it is difficult to define what a "pure method" would be, with a definition that allows the method to be used in expressions suitable for the verifier

What's missing in the definition I provided? The method may not modify any state (modifies {}) and must be deterministic, (any two invocations with equal parameters (including heap) return an equal result, using Dafny's existing definition of equality)

Back to the forall statement.
...

I agree that given the existence of statement expressions, it is better if forall statements are included in those. However, whether it's a good investment to add them hinges on whether we want to keep statement expressions.

Do you have a suggestion for a new keyword for either if statements or if-then-else expressions?

If we don't unify the syntax, then I think using ternary operators (? :) for the expression version would be better than how it is now.

However, I think ideally it would be a single syntax for both expressions and statements. There was a discussion in this ticket #2899 and it would probably be best to continue there. I still like @MikaelMayer 's proposal there.

Variables are introduced with the var keyword. But those variables introduced in an expression are not mutable.

I'd discuss more but it'd be better to use a separate GH issue for that. My bad for mentioning it here in the first place. Created an issue: #5914

[RustanLeino]

While those things are being discussed elsewhere, can we move forward with accepting this PR? @MikaelMayer @keyboardDrummer

[MikaelMayer]

That works for me as it.

Thank you @keyboardDrummer for reminding me of the suggestion for a new if syntax ! I had totally forgotten about it. Now that I think of it, it's just that the regular if-then-else is like a match without braces.