search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.91k stars 262 forks source link

Allow forall statements in expressions #146

Open wilcoxjay opened 7 years ago

wilcoxjay commented 7 years ago

Occasionally, when a function has a universally quantified precondition, it would be convenient to be able to use a forall statement to prove the precondition inline in an expression context.

RustanLeino commented 7 years ago

Nice idea. I think this would be simple to implement. It would involve another use of the StmtExpr production, which already handles (calls and the more similar) assert/assume/calc statements.

wilcoxjay commented 7 years ago

It's good to hear that this shouldn't introduce any new difficulties in translation.

One thing I'm worried about is parsing it. I think it will be impossible to distinguish forall statement-expressions from universal quantifiers until the opening curly brace or ensures token. I don't think we can even distinguish these with a lookahead, because we need to skip over arbitrary expressions. Instead, we may need to introduce new nonterminals for "a prefix of either a universal quantifier or a forall statement-expression".