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)
• [x] New feature (non-breaking change which adds functionality)
• [ ] Breaking change (fix or feature that would cause existing functionality to change)
• [x] There are changes to the (Java) code
• [x] 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.
• [x] 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[bot]]

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 :warning:
...in/java/de/uka/ilkd/key/rule/SetStatementRule.java	25.58%	31 Missing and 1 partial :warning:
...ka/ilkd/key/proof/mgt/SpecificationRepository.java	13.04%	17 Missing and 3 partials :warning:
.../uka/ilkd/key/logic/equality/RenamingProperty.java	76.62%	7 Missing and 11 partials :warning:
...a/ilkd/key/java/visitor/ProgVarReplaceVisitor.java	11.11%	16 Missing :warning:
...va/de/uka/ilkd/key/java/recoderext/adt/SeqPut.java	0.00%	15 Missing :warning:
...de/uka/ilkd/key/speclang/WellDefinednessCheck.java	7.14%	9 Missing and 4 partials :warning:
...d/key/speclang/jml/translation/JMLSpecFactory.java	78.57%	7 Missing and 5 partials :warning:
...lkd/key/java/visitor/ProgramVariableCollector.java	0.00%	11 Missing :warning:
.../uka/ilkd/key/java/visitor/CreatingASTVisitor.java	0.00%	10 Missing :warning:
... and 51 more

Additional details and impacted files

```diff @@ 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 ```

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