KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Removal of Triple, and Quadruple #3399

Open wadoon opened 6 months ago

wadoon commented 6 months ago

Refactoring

This PR starts the removal of generic data classes in favor of Java records (aka. named tuples). In this PR, only Triple and Quadruple are removed.

In general, generic parametric data classes (Tuple, Union, ...) lead to unreadable, incomprehensible code, e.g., what does the entity Triple<StatementBlock, URI, Integer> express? Answer: It is the key in a map to find block contracts. Using the record BlockContractKey expresses 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<…> and Quadruple<…>.

Type of pull request

Ensuring quality

codecov[bot] commented 2 months ago

Codecov Report

Attention: Patch coverage is 44.55959% with 107 lines in your changes missing coverage. Please review.

Project coverage is 38.16%. Comparing base (0ebb8b5) to head (2eae40e). Report is 3 commits behind head on main.

Files Patch % Lines
.../java/de/uka/ilkd/key/rule/WhileInvariantRule.java 17.14% 29 Missing :warning:
...g/key_project/slicing/ui/RuleStatisticsDialog.java 0.00% 23 Missing :warning:
...org/key_project/slicing/ui/ShowNodeInfoAction.java 0.00% 9 Missing :warning:
...d/key/speclang/jml/translation/JMLSpecFactory.java 12.50% 5 Missing and 2 partials :warning:
...ka/ilkd/key/proof/mgt/SpecificationRepository.java 66.66% 6 Missing :warning:
...org/key_project/slicing/graph/DependencyGraph.java 60.00% 6 Missing :warning:
...n/java/org/key_project/slicing/RuleStatistics.java 68.75% 5 Missing :warning:
...java/de/uka/ilkd/key/speclang/ContractFactory.java 0.00% 4 Missing :warning:
...trategy/definition/StrategySettingsDefinition.java 0.00% 4 Missing :warning:
...l/mergerule/SymbolicExecutionStateWithProgCnt.java 33.33% 4 Missing :warning:
... and 7 more
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3399 +/- ## ========================================= Coverage 38.16% 38.16% + Complexity 17222 17220 -2 ========================================= Files 2109 2109 Lines 127643 127624 -19 Branches 21458 21456 -2 ========================================= - Hits 48710 48706 -4 + Misses 72943 72932 -11 + Partials 5990 5986 -4 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.