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 |
4 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.