-
Notifications
You must be signed in to change notification settings - Fork 257
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Allow termination ordering to be written in expressions #5252
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Comments
atomb
added
the
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
label
Mar 26, 2024
atomb
added a commit
that referenced
this issue
Apr 19, 2024
### Description This is a refactoring-only PR intended to make implementing [`decreases to`](#5252) more straightforward when we do it. ### How has this been tested? With the existing test suite, as it's purely a refactoring. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
atomb
added a commit
that referenced
this issue
May 29, 2024
### Description Implement the `decreases to` and `nonincreases to` expression forms. This allows you to state that the left-hand sequence of expressions decreases (or at least doesn't increase) to the right-hand sequence. One caveat: for now, `decreases to` is allowed only inside parentheses, to avoid parsing ambiguities. This is a strict subset of what we'd ideally like to support. I think it should be possible to allow it to appear elsewhere as part of a separate, backward-compatible PR. Fixes #5252 ### How has this been tested? Added `dafny0/DecreasesTo{1,2,3,4,5}.dfy` By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Summary
Make it possible to write explicit expressions, especially in assertions, that describe the proposition that a termination metric decreases.
Background and Motivation
As part of #2987, we want to be able to create an explicit assert statement for any proof goal that fails. Currently, stating that a termination metric decreases is awkward or impossible, for several reasons:
a, b, c
decreases toa', b', c'
is something roughly likea > a' || (a == a' && b > b') || (a == a' && b == b' && c > c')
, which is large and hard to read.a > a’
doesn’t currently mean the right thing for sequences or datatypes.Proposed Feature
I propose we introduce a custom expression form,
a, b, c decreases to a', b', c'
that is shorthand for roughly the larger expression shown above but with the correct semantics for==
and>
when considering sequences and datatypes.The parser will eagerly parse all commas when parsing this form, so parentheses may be required to disambiguate some instances, but frequently should be unnecessary.
Alternatives
Several alternatives are possible:
>
ordering for sequences or datatypes and use a termination predicate exactly of the form shown above. This could perhaps break existing code and would be verbose.The text was updated successfully, but these errors were encountered: