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 36.23%. Comparing base (e5853a5) to head (519a11c).
⚠️ Report is 26 commits behind head on main.

❗ There is a different number of reports uploaded between BASE (e5853a5) and HEAD (519a11c). Click for more details.

HEAD has 2 uploads less than BASE

Flag	BASE (e5853a5)	HEAD (519a11c)
	14	12

Additional details and impacted files

@@              Coverage Diff              @@
##               main    #3724       +/-   ##
=============================================
- Coverage     47.98%   36.23%   -11.76%     
+ Complexity    16045     1011    -15034     
=============================================
  Files          1683      166     -1517     
  Lines         96046     7929    -88117     
  Branches      15388     1168    -14220     
=============================================
- Hits          46091     2873    -43218     
+ Misses        44683     4798    -39885     
+ Partials       5272      258     -5014     

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