More general equalsModProperty

[tobias-rnh]

Intended Change

Building on top of #3386, the interface EqualsModProperty has now been changed so that it can be used not just with Terms but theoretically any class if a proper Property is implemented. The signature of the method has also been slightly modified so that it is able to handle equality checks that utilize additional parameters (like was the case with equalsModRenaming defined on SourceElements that is also refactored with this PR).
To refactor equalsModRenaming of SourceElement, a new Interface TreeWalker and implementing class JavaASTTreeWalker have been introduced that make it possible to move through the tree of SourceElements step by step.
The new general navigation structure is used to move through the tree of SourceElements.

Plan

Direct tests for JavaASTTreeWalker (currently only indirectly tested through tests for equalsModProperty)
Even more doc comments

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: Already existing and new tests

Additional information and contact(s)

EqualsModProperty

The old TermEqualsModProperty

public interface TermEqualsModProperty {
    boolean equalsModProperty(Object o, TermProperty property);
    int hashCodeModProperty(TermProperty property);
}

has now been parameterized with a type T so that it can accommodate other classes than just Term:

public interface EqualsModProperty<T> {
    <V> boolean equalsModProperty(Object o, Property<T> property, V... v);
    int hashCodeModProperty(Property<T> property);
}

equalsModProperty is furthermore parameterized with a type V that can account for additional parameters needed for the equality check.

Properties

public interface TermProperty {
    Boolean equalsModThisProperty(Term term1, Term term2);
    int hashCodeModThisProperty(Term term);
}

is now parameterized with a type T so that it can accommodate other classes than just Term:

public interface Property<T> {
    <V> boolean equalsModThisProperty(T t1, T t2, V... v);
    int hashCodeModThisProperty(T t);
}

equalsModThisProperty is furthermore parameterized with a type V that can account for additional parameters needed for the equality check.

Refactoring of equalsModRenaming

As equals and equalsModRenaming for SourceElements were basically doing the same thing except for a few classes (equals mostly called equalsModRenaming), the idea was that the content of equalsModRenaming is moved to equals entirely. The special cases that did not call equalsModRenaming in equals or made use of the NameAbstractionTable are now handled by a JavaASTTreeWalker.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[tobias-rnh]

This time the unit tests for windows fail but they run on my machine.
The CodeQuality checks checkstyle_new and pmd seem to also not be working now, however the error messages seem to not be related to my changes.

[Drodt]

3 things to do before merge:

1. Fix merge conflicts.
2. Some Classes (e.g., StatementBlock) now have equals methods but no corresponding hash methods. Those would need to be added.
3. Add default methods to EqualsModProperty interface like equalsModRemaning that call equalsModProperty with the corresponding property.

[codecov]

Codecov Report

Attention: Patch coverage is 41.42012% with 99 lines in your changes missing coverage. Please review.

Project coverage is 38.09%. Comparing base (a4de274) to head (dd8d2ef).
Report is 5 commits behind head on main.

Files	Patch %	Lines
.../logic/equality/RenamingSourceElementProperty.java	52.54%	14 Missing and 14 partials ⚠️
...ava/de/uka/ilkd/key/smt/AbstractSMTTranslator.java	0.00%	7 Missing ⚠️
.../ilkd/key/java/statement/TransactionStatement.java	0.00%	2 Missing and 3 partials ⚠️
...de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java	0.00%	4 Missing ⚠️
.../main/java/de/uka/ilkd/key/java/SourceElement.java	25.00%	2 Missing and 1 partial ⚠️
...kd/key/java/expression/literal/BooleanLiteral.java	40.00%	1 Missing and 2 partials ⚠️
...lkd/key/java/expression/literal/DoubleLiteral.java	0.00%	3 Missing ⚠️
...ilkd/key/java/expression/literal/FloatLiteral.java	0.00%	3 Missing ⚠️
.../ilkd/key/java/expression/literal/RealLiteral.java	0.00%	3 Missing ⚠️
...lkd/key/java/expression/literal/StringLiteral.java	0.00%	1 Missing and 2 partials ⚠️
... and 27 more

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3459      +/-   ##
============================================
+ Coverage     38.04%   38.09%   +0.05%     
- Complexity    17117    17175      +58     
============================================
  Files          2105     2107       +2     
  Lines        127439   127517      +78     
  Branches      21401    21436      +35     
============================================
+ Hits          48487    48581      +94     
+ Misses        72978    72950      -28     
- Partials       5974     5986      +12     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[tobias-rnh]

3 things to do before merge:

1. Fix merge conflicts.

Done.

2. Some Classes (e.g., `StatementBlock`) now have `equals` methods but no corresponding `hash` methods. Those would need to be added.

Most of the time, this was a false alert. The hashCode() method is not directly overridden, but the method computeHashCode() that does the actual computation in hashCode() is overridden. For some classes, however, I have added implementations of computeHashCode().

3. Add default methods to `EqualsModProperty` interface like `equalsModRemaning` that call `equalsModProperty` with the corresponding property.

As discussed, we do not add default methods. Most of the properties like TermLabelsProperty are only defined for terms, and there are no comparable properties defined for other instances of the generic type T.

[tobias-rnh]

I have changed equalsModThisProperty in RenamingSourceElementProperty to use the general navigation structure instead of the TreeWalker. Because of this, I have removed the TreeWalker entirely.
This PR could now be merged after all the tests have passed.