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.

[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 https://github.com/dafny-lang/dafny/issues/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: https://github.com/dafny-lang/dafny/issues/5914

[RustanLeino]

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