Conversation
| \heuristics(simplify) | ||
| }; | ||
|
|
||
| msetUnionSubset { |
There was a problem hiding this comment.
This rule is at the moment not automatically applied as mSetEl is not instantiated. It seems also not to be correct because the test should check for all mSetEl in s?
After a fix it should not be in simplify as it might result in an infinite loop.
| \heuristics(polySimp_expand, polySimp_addOrder) | ||
| }; | ||
|
|
||
| msetUnionAssociativity { |
There was a problem hiding this comment.
Here and in other places we should define a term order for multisets and use that one. The ordering using poly_... checks whether its arguments are monomials and plynomials which does not work here as expected.
| \heuristics(simplify) | ||
| }; | ||
|
|
||
| msetSumWithMSetEmpty1 { |
There was a problem hiding this comment.
with a working term order only one of the msetSumWithMSetEmpty1/2 rules should be needed
| \heuristics(polySimp_expand, polySimp_addAssoc) | ||
| }; | ||
|
|
||
| msetDiffWithMSetEmpty1 { |
There was a problem hiding this comment.
similar remark as for msetSumWithMSetEmpty
| \heuristics(simplify) | ||
| }; | ||
|
|
||
| msetIntersecSubset { |
| Mset msetSum(Mset, Mset); | ||
| Mset msetRange {false, false, true}(int, int, any); | ||
| } | ||
|
|
There was a problem hiding this comment.
Some of the rules check for subset. We should add a predicate for that and use that one in the assumes of the rules instead of an if-then-else
|
@lks9 The review remarks are mostly for myself, so that I don't forget to address them when looking into the strategies for this PR |
|
Error message: |
|
KaKeY: If not ready until July 8th, the PR is postponed to milestone v3.1.0 |
|
I would suggest removing the rules for union, intersection, and diff. They have never been correct. For our verification purposes, sum, single, and range are the operators to use. I see no need for union, intersection, and diff. Should we also remove the constructors for union, intersection, and diff? I would say, comment them out for future additions. I was absent in the KaKeY because I did not know that you would discuss this MR. If you think it can/should be finished by July 8th, I can help. |
|
@lks9 I am rewriting them currently to parametric versions and remove the union, intersec and diff. We can then have a look at the result together thanks next week. Thanks! |
|
The PR is moved to 3.1
Without solving both issues first, the use of the mset theory is rather limited and we will not have a solution for them before 3.0 |
5 participants
Intended Change
This adds multisets in KeY, to show permutation properties. This complements the existing formalizations using
seqPermandbsum.(\mset int k; low <= k <= high; t)extended JML quantifiermsetRange{int k;}(low, high, t)to JavaDL and other constructors such asmsetSingle,msetSumPlan
There were some fixes needed to actually prove permutation properties of quicksort or similar.
applyEqorhideAuxiliaryEq. Three instantiations ofhideAuxiliaryEqwere needed, Quicksort_sort.zproof.zipEqualityConstraint.java, functionnormalize()does not break anythingType of pull request
Additional information
Quicksort could not be shown without the changes to
EqualityConstraint.java. As far as I understand it, theisRigid()guard prevents normalization and is therefore a completeness bug in the current version of KeY. Credits go to @unp1. Apparently, in an old KeY 1.x version, theisRigid()guard was needed for soundness as it would prevent normalization with constrained program variables.The basic idea of the MSet rules is as follows:
msetRangeinto amsetSumof themsetSinglewith the updated element andmsetRangefor the remaining part without the update.msetSumis converted into a normal form using associativity and commutativity.A = BintoA_decomposed = B. To bringBin the same form (although there are no updates),msetRangeis also decomposed on side B an equation using the rulemset_extract_triggeredand friends.Alternatively to the decomposition approach, we could also back-convert the normal form of
msetSums (e.g.A_decomposed) into a bigmsetRange. However, we have not implemented this.The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.