Allow any construct to be tracked by "necessary assumptions" #730
Assignees
Labels
Comments
Which Boogie feature or flag are you referring to? |
I didn't know about this flag :-) And I see that it is not documented. Sounds like a good plan to have a more meaningful name that is well documented. |
keyboardDrummer
pushed a commit
that referenced
this issue
Jun 6, 2023
This generalizes the previous feature of tracking "necessary
assumptions".
That feature, previously enabled with `-printNecessaryAssumptions`,
allowed each `assume` statement to be annotated with an `{:id ...}`
attribute, and Boogie would then report which assumptions were necessary
to complete the verification by requesting an unsat core from Z3.
Now that attribute can be placed on many other program elements:
* `assume` statements
* `assert` statements
* assignments
* calls
* requires clauses
* ensures clauses
Each of these is then labeled in the SMT encoding and will potentially
show up in the unsat core.
The new `-printVerificationCoverage` option (which replaces the old one)
prints the members of this broader set of program elements that show up
in the unsat core. With `-trace`, it also prints the coverage
information for each procedure as it finishes. The coverage information
for each procedure is also available in the `VCResult` produced at the
end of each verification.
Fixes #730.
atomb
added a commit
to dafny-lang/dafny
that referenced
this issue
Jul 21, 2023
This adds a couple of Dafny-relevant things: * A soundness fix for boogie-org/boogie#749. I thought this would resolve #4053, because it resolves a soundness issue discovered during the investigation of that issue, but it doesn't. Apparently there's _another_ soundness issue hiding in there. * Support for coverage analysis: which program constructs annotated with an `{:id ...}` attribute contributed to verification? Dafny currently does not add `{:id ..}` attributes, but we plan to make it automatically do so (optionally) in the near future. See boogie-org/boogie#730. * Allow absolute paths to Boogie solver plugins. 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
Boogie currently allows the use of unsat cores to track which
assumestatements are necessary during verification.This feature can be much more widely useful. The assumptions that arise from
requiresclauses, loop invariants, and even assignments could be tracked, as well. Achieving this is mostly a matter of plumbing around:idattributes.Even beyond that, assertions could be included, as well. Doing so will allow Boogie to track a notion of verification coverage, such as described here or here. Doing this is slightly less straightforward, and could require changes to how Boogie structures its VCs.
This notion of coverage encompasses vacuity (as described by the first of those two papers). If verification requires, for instance, the preconditions to a procedure but none of the body, then either the preconditions are contradictory or any assertions or postconditions are trivial.
I plan to implement this myself, but am creating this issue to track progress.
The text was updated successfully, but these errors were encountered: