Generalize ParsableVariable and Schemavariables #3436

Drodt · 2024-03-05T15:25:52Z

Related Issue

Intended Change

This PR moves the ParsableVariable interface to ncore, makes it no longer an Operator and renames AbstractSV to OperatorSV as this interface now handles all schema variables that may be operators.

It also handles the refactorings necessary to adapt to this change. I.e., changing types where necessary, changing how modality schema vars are matched, and some changes to the term builder.

Also fixes the Github workflow.

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).
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: ...
I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

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

codecov · 2024-03-05T15:54:21Z

Codecov Report

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

Project coverage is 37.96%. Comparing base (7254776) to head (07ad420).
Report is 116 commits behind head on main.

❗ Current head 07ad420 differs from pull request most recent head a16defe

Please upload reports for the commit a16defe to get more accurate results.

Files	Patch %	Lines
...de/uka/ilkd/key/speclang/WellDefinednessCheck.java	0.00%	43 Missing ⚠️
...a/ilkd/key/rule/tacletbuilder/TacletGenerator.java	36.00%	32 Missing ⚠️
...ava/de/uka/ilkd/key/smt/newsmt2/SeqDefHandler.java	0.00%	17 Missing ⚠️
.../src/main/java/de/uka/ilkd/key/rule/TacletApp.java	65.90%	8 Missing and 7 partials ⚠️
...e/uka/ilkd/key/speclang/MethodWellDefinedness.java	0.00%	15 Missing ⚠️
...e/uka/ilkd/key/rule/AuxiliaryContractBuilders.java	12.50%	9 Missing and 5 partials ⚠️
.../uka/ilkd/key/speclang/DependencyContractImpl.java	13.33%	13 Missing ⚠️
.../main/java/de/uka/ilkd/key/java/TypeConverter.java	14.28%	7 Missing and 5 partials ⚠️
...c/main/java/de/uka/ilkd/key/logic/TermBuilder.java	33.33%	9 Missing and 1 partial ⚠️
.../key/speclang/FunctionalOperationContractImpl.java	65.51%	10 Missing ⚠️
... and 56 more

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3436      +/-   ##
============================================
+ Coverage     37.86%   37.96%   +0.10%     
+ Complexity    17079    17058      -21     
============================================
  Files          2092     2081      -11     
  Lines        127596   126912     -684     
  Branches      21478    21332     -146     
============================================
- Hits          48316    48186     -130     
+ Misses        73355    72819     -536     
+ Partials       5925     5907      -18

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

…casting TermSV to ProgramVariable not applicable

…3484)

* refs/heads/main: Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test repair soundness of assignment2UpdateRules with checked overflows spotless Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version API design throw an error if choices used in a taclet are not declared correct inRange(..) predicates for overflow check semantics fix creating of branches for overflow checking

* main: (77 commits) Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test change gradle github action to new syntax adding comments to jml spec factory default contracts repair soundness of assignment2UpdateRules with checked overflows spotless EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Changed types in replacement map for WD taclets, since PR KeYProject#3436 made casting TermSV to ProgramVariable not applicable spotlessing ... making RuleCommand work if already fully instantiated RuleCommand can now deal with rules that have schema variables for logical variables. Fix loading of taclet proof obligations (issue KeYProject#3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof obligation Code clean up (remove unused method) Fix loading of closed proofs (GUI threw error) Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method ...

* main: (77 commits) Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test change gradle github action to new syntax adding comments to jml spec factory default contracts repair soundness of assignment2UpdateRules with checked overflows spotless EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable spotlessing ... making RuleCommand work if already fully instantiated RuleCommand can now deal with rules that have schema variables for logical variables. Fix loading of taclet proof obligations (issue #3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof obligation Code clean up (remove unused method) Fix loading of closed proofs (GUI threw error) Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method ...

* main: (33 commits) Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test change gradle github action to new syntax adding comments to jml spec factory default contracts repair soundness of assignment2UpdateRules with checked overflows spotless EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version ...

Drodt and others added 19 commits March 5, 2024 12:10

Start moving parsable variable

4df5279

spotless

01454e6

Fix 100 errors

ade0e3b

Fix 100 more errors

88a8f62

Fix even more errors

8806a72

Fix type error

2fdb6dc

Fix errors after changing ParsableVars

2e2c26e

Delete Legacy Matcher and adapt VM matcher for new Modality operator

2a18de1

Fix errors resulting from changing ParseableVar

09f8202

Fix parsing of variable conditions

6596ccb

Fix taclet equality test

932bde8

Fix taclet prefix check when parsing

2cfc9db

Spotless fixes

c07862b

Fix settings test for SE

af533c6

Beautified code

c915026

Rename AbstractSV to OperatorSV

d1bd2b1

Spotless

4ae0b65

Spotless

b2dbeba

Move ParsableVariable to ncore

a3ad16f

Drodt added 2 commits March 6, 2024 16:44

Fix? resolving error

9085ec3

Spotless

a6e4d68

unp1 self-requested a review March 7, 2024 08:29

Remove todo

07ad420

unp1 assigned Drodt and unp1 Mar 15, 2024

unp1 added the RFC "Request for comments" is the appeal for making and expressing your opinion on a topic. label Mar 15, 2024

Drodt added 3 commits May 2, 2024 09:51

Merge branch 'main' into move-parsable-var

72e4fa5

Fix merge conflicts & spotless

d108683

Fix checkstyle workflow

d41bb6e

Drodt added Review Request Waiting for review and removed RFC "Request for comments" is the appeal for making and expressing your opinion on a topic. labels May 8, 2024

Merge branch 'main' into move-parsable-var

304fd3d

Drodt mentioned this pull request May 22, 2024

Realize generic navigation structure #3472

Merged

Merge branch 'main' into move-parsable-var

fb93c9c

unp1 approved these changes May 22, 2024

View reviewed changes

unp1 enabled auto-merge May 22, 2024 09:15

Fix comment

a16defe

unp1 added this pull request to the merge queue May 22, 2024

Merged via the queue into KeYProject:main with commit 55ab074 May 22, 2024
13 checks passed

unp1 deleted the move-parsable-var branch May 22, 2024 11:32

mi-ki added a commit that referenced this pull request Jun 20, 2024

Changed types in replacement map for WD taclets, since PR #3436 made …

6c0875c

…casting TermSV to ProgramVariable not applicable

mi-ki mentioned this pull request Jun 20, 2024

Fixed operator replacements in WD taclets after changes in PR #3436 #3484

Merged

github-merge-queue bot pushed a commit that referenced this pull request Jun 24, 2024

Fixed operator replacements in WD taclets after changes in PR #3436 (#…

a442cdf

…3484)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Generalize ParsableVariable and Schemavariables #3436

Generalize ParsableVariable and Schemavariables #3436

Drodt commented Mar 5, 2024 •

edited

Loading

codecov bot commented Mar 5, 2024 •

edited

Loading

Generalize ParsableVariable and Schemavariables #3436

Generalize ParsableVariable and Schemavariables #3436

Conversation

Drodt commented Mar 5, 2024 • edited Loading

Related Issue

Intended Change

Type of pull request

Ensuring quality

Additional information and contact(s)

codecov bot commented Mar 5, 2024 • edited Loading

Codecov Report

Drodt commented Mar 5, 2024 •

edited

Loading

codecov bot commented Mar 5, 2024 •

edited

Loading