Removal of Triple, and Quadruple #3529
Conversation
wadoon
force-pushed
the
weigl/recordsftw
branch
from
325d25b
to
0eec2d4
Compare
wadoon
force-pushed
the
weigl/recordsftw
branch
from
130c4c3
to
f658d4f
Compare
|
There was a problem hiding this comment.
Thanks! In my opinion, it is a very good idea to remove these two classes, and use records with good names instead.
I only have some minor remarks:
- In some comments, "first" and "second" have been replaced too aggressively ...
- Some uses of var should be removed in my opinion.
- Some record parameters could use better names instead of "first", "second", ...
| Location location = new Location(url, Position.newOneBased(script.second, script.third)); | ||
|
|
||
| return new Pair<>(script.first, location); | ||
| /** |
There was a problem hiding this comment.
Should we then maybe just delete this method?
| @@ -134,4 +133,13 @@ protected static SequentFormula replace(PosInOccurrence pio, Term newTerm, Servi | |||
| public boolean isApplicableOnSubTerms() { | |||
| return false; | |||
| } | |||
|
|
|||
There was a problem hiding this comment.
The documentation is only a placeholder. I also would rather have this record in a separate file, since it is used in multiple other files ...
| @@ -112,9 +111,10 @@ public class IntermediateProofReplayer { | |||
| private final LinkedList<Pair<Node, NodeIntermediate>> queue = | |||
| new LinkedList<>(); | |||
|
|
|||
| private record PartnerNode(Node first, PosInOccurrence second, NodeIntermediate third) {} | |||
There was a problem hiding this comment.
Do you understand what these parameters are used for? Can you maybe give them better names?
|
|
||
| final Triple<Term, Term, Term> ownSEState = | ||
| var ownSEState = |
There was a problem hiding this comment.
I think the type should be made explicit here. Also, SETriple is not really a triple any more, right? So maybe also the method should be renamed ...
| } | ||
|
|
||
| private record Guard(JavaBlock first, Term second, Term third) {} |
There was a problem hiding this comment.
Same as earlier: Can you give the parameters/fields of the record useful names?
| * @param heapVar The heap variable for which the values should be merged. | ||
| * @param heap1 The first heap term. | ||
| * @param heap2 The second heap term. | ||
| * @param state1 SE state for the first heap term. | ||
| * @param state2 SE state for the second heap term | ||
| * @param heap1 The distinguishingFormula heap term. | ||
| * @param heap2 The ifTerm heap term. | ||
| * @param state1 SE state for the distinguishingFormula heap term. | ||
| * @param state2 SE state for the ifTerm heap term |
There was a problem hiding this comment.
Looks like you wrongly replaced some words in the whole file (also earlier in the file) ...
| @@ -132,22 +131,28 @@ public static Term createIfThenElseTerm(final SymbolicExecutionState state1, | |||
| * <code>{ v := \if (c1) \then (t1) \else (t2) }</code>, where c1 is the path condition of | |||
| * state1. However, the method also tries an optimization: The path condition c2 of state2 could | |||
| * be used if it is shorter than c1. Moreover, equal parts of c1 and c2 could be omitted, since | |||
| * the condition shall only distinguish between the states. The first element of the triple is | |||
| * the discriminating condition, the second and third elements are the respective parts for the | |||
| * the condition shall only distinguish between the states. The distinguishingFormula element of | |||
There was a problem hiding this comment.
Same as earlier: Too aggressive textual replacements.
| Triple<IObserverFunction, Term, Term> dep = | ||
| new JmlIO(services).context(context).translateDependencyContract(originalDep); | ||
| return cf.dep(kjt, targetHeap, dep, dep.first.isStatic() ? null : context.selfVar()); | ||
| var dep = new JmlIO(services).context(context).translateDependencyContract(originalDep); |
There was a problem hiding this comment.
I think this is a bad use of var ...
Refactoring
This PR starts the removal of generic data classes in favor of Java records (aka. named tuples). In this PR, only
TripleandQuadrupleare removed.In general, generic parametric data classes (
Tuple,Union, ...) lead to unreadable, incomprehensible code, e.g., what does the entityTriple<StatementBlock, URI, Integer>express? Answer: It is the key in a map to find block contracts. Using the recordBlockContractKeyexpresses this better than triple of something.Therefore, records give you the chance of defining useful variable names, and documentation, and also avoid auto-boxing (hence NPE).
Intended Change
No use of
Triple<…>andQuadruple<…>.Type of pull request
Ensuring quality