Introducing a new function symbol seqUpd

[mattulbrich]

Intended Change

There was no explicit update function for sequences in KeY (any more). I added seqUpd for that purpose.
The axiomatic rules is in seqRules.key and essentially reads:

 \find(alpha::seqGet(seqUpd(seq, idx, value), jdx))
 \replacewith(\if(0<=jdx & jdx < seqLen(seq) & idx=jdx) \then((alpha)value) \else(alpha::seqGet(seq, jdx)))

• The JML translation was adapted
• The JML in Java translation was extended and adapted

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base
• There are changes to the deployment/CI infrastructure (gradle, github, ...)
• Other:

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments). The added code essentially copies similar code around it and has the same level of documentation.
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs). There is no documentation for \seq to add to.
• I added new test case(s) for new functionality. There are no test cases for the other similar seqXXX functions to which one would add new test cases.
• I have tested the feature as follows: by extending an existing case study in KeY
• I have checked that runtime performance has not deteriorated.

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

[codecov]

Codecov Report

Attention: Patch coverage is 54.16667% with 418 lines in your changes are missing coverage. Please review.

Project coverage is 37.87%. Comparing base (c3b3268) to head (6791160).
Report is 77 commits behind head on main.

Files	Patch %	Lines
...rc/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java	61.48%	119 Missing ⚠️
...in/java/de/uka/ilkd/key/rule/SetStatementRule.java	25.58%	31 Missing and 1 partial ⚠️
...ka/ilkd/key/proof/mgt/SpecificationRepository.java	13.04%	17 Missing and 3 partials ⚠️
.../uka/ilkd/key/logic/equality/RenamingProperty.java	76.62%	7 Missing and 11 partials ⚠️
...a/ilkd/key/java/visitor/ProgVarReplaceVisitor.java	11.11%	16 Missing ⚠️
...va/de/uka/ilkd/key/java/recoderext/adt/SeqPut.java	0.00%	15 Missing ⚠️
...de/uka/ilkd/key/speclang/WellDefinednessCheck.java	7.14%	9 Missing and 4 partials ⚠️
...d/key/speclang/jml/translation/JMLSpecFactory.java	78.57%	7 Missing and 5 partials ⚠️
...lkd/key/java/visitor/ProgramVariableCollector.java	0.00%	11 Missing ⚠️
.../uka/ilkd/key/java/visitor/CreatingASTVisitor.java	0.00%	10 Missing ⚠️
... and 51 more

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3385      +/-   ##
============================================
+ Coverage     37.85%   37.87%   +0.02%     
- Complexity    17042    17082      +40     
============================================
  Files          2082     2092      +10     
  Lines        127290   127518     +228     
  Branches      21441    21466      +25     
============================================
+ Hits          48183    48295     +112     
- Misses        73194    73317     +123     
+ Partials       5913     5906       -7     

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

[WolframPfeifer]

Nice addition!

I see one minor problem for the code quality: The relevant classes/tokens/methods are sometimes called seqPut, sometimes seqReplace, sometimes seqUpd. I think that this is quite confusing, in particular for new developers. Can we just name everything consistently seqUpd?

[wadoon]

If we can get of the current ghost declaration processing, we might be able to get rid of the Recoder JML AST classes!

Change requests is blocking merge. Mattias clearly stated that you prefers the current state. It is only a minor readability/convinience thingy.