Universe Type Rules

[PiIsRational]

Intended Change

Add universe type rules and support for universe type annotations
as an alternative to dynamic frames in proofs and contract specifications.

Plan

• Wait for The Removal of Recoder #3120
• Support Array Types
• Better support for creation of objects with universe type annotations
• Code cleanup
• Document the changes

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are changes to the taclet rule base

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows:
  • specific examples using the universe type system

Additional information and contact(s)

@WolframPfeifer is involved in this pull request.

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

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 41.09%. Comparing base (7d01c6c) to head (33d1e5e).
⚠️ Report is 625 commits behind head on main.

❗ There is a different number of reports uploaded between BASE (7d01c6c) and HEAD (33d1e5e). Click for more details.

HEAD has 10 uploads less than BASE

Flag	BASE (7d01c6c)	HEAD (33d1e5e)
	14	4

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3724      +/-   ##
============================================
- Coverage     50.48%   41.09%   -9.40%     
+ Complexity    16158      461   -15697     
============================================
  Files          1620       66    -1554     
  Lines         92011     2740   -89271     
  Branches      14705      490   -14215     
============================================
- Hits          46455     1126   -45329     
+ Misses        40292     1540   -38752     
+ Partials       5264       74    -5190     

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

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[codecov-commenter]

⚠️ Please install the to ensure uploads and comments are reliably processed by Codecov.

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 13.94%. Comparing base (7d01c6c) to head (86d605e).
⚠️ Report is 659 commits behind head on main.
❗ Your organization needs to install the Codecov GitHub app to enable full functionality.

❗ There is a different number of reports uploaded between BASE (7d01c6c) and HEAD (86d605e). Click for more details.

HEAD has 6 uploads less than BASE

Flag	BASE (7d01c6c)	HEAD (86d605e)
	14	8

Additional details and impacted files

@@              Coverage Diff              @@
##               main    #3724       +/-   ##
=============================================
- Coverage     50.48%   13.94%   -36.54%     
+ Complexity    16158      461    -15697     
=============================================
  Files          1620      174     -1446     
  Lines         92011     8072    -83939     
  Branches      14705     1332    -13373     
=============================================
- Hits          46455     1126    -45329     
+ Misses        40292     6872    -33420     
+ Partials       5264       74     -5190     

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

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.