-
Notifications
You must be signed in to change notification settings - Fork 36
Generate easier POs for non-trivial diverges clauses #3430
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
base: main
Are you sure you want to change the base?
Conversation
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## main #3430 +/- ##
=========================================
Coverage 37.77% 37.77%
+ Complexity 17031 17030 -1
=========================================
Files 2076 2076
Lines 126950 126953 +3
Branches 21381 21381
=========================================
+ Hits 47952 47954 +2
Misses 73092 73092
- Partials 5906 5907 +1 ☔ View full report in Codecov by Sentry. |
@@ -926,10 +926,13 @@ public ImmutableSet<Contract> createFunctionalOperationContracts(String name, IP | |||
result = result.add(contract); | |||
} else { | |||
// create two contracts for each diamond and box modality | |||
Map<LocationVariable, Term> boxPres = new LinkedHashMap<>(pres); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Shouldn't this be a copy of clauses.requires
? Previously that map was used when constructing the FunctionalOperationContract.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That seems like an oversight in the old version. I see no reason why this should be clauses.requires
. The pre-conditions should be identical for diamond and box modalities.
@Drodt Just looking through old PRs ... What is the state of this one? Is it finished and reviewable? |
Related Issue
This pull request fixes #29.
Intended Change
A non-trivial (i.e, neither
true
norfalse
) diverges clause results in two contracts to be verified. Previously, there was one where the value of the clause (herediv
) is not true and the method therefore terminates, and one where the method does not terminate.E.g., the two POs would look like
pre & !div -> <m()>post
andpre -> [m()] post
. This resulted in more complex proofs, because the case wherediv
is false had to be considered as well for the second PO.This PR changes the POs to
pre & !div -> <m()>post
andpre & div -> [m()] post
Hence, we have a proper cut.
Type of pull request
Ensuring quality
Additional information and contact(s)
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.