Skip to content

Conversation

@FliegendeWurst
Copy link
Member

@FliegendeWurst FliegendeWurst commented Jan 19, 2026

Intended Change

The Integer class is a bit useless without providing at least valueOf and intValue, so I added specifications for those methods. And the field value to store the int value.

The List::remove method to remove elements by index is useful to have.

The NoSuchElementException class is required to implement iterators.

Type of pull request

  • New feature (non-breaking change which adds functionality)
  • Other: change to JavaRedux (bootstrap classpath)

Ensuring quality

  • I have tested the feature as follows: used the newly specified methods in a simple example

Additional information and contact(s)

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

@codecov
Copy link

codecov bot commented Jan 19, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 47.98%. Comparing base (2aa39bb) to head (e26aadc).
⚠️ Report is 45 commits behind head on main.

Additional details and impacted files
@@             Coverage Diff              @@
##               main    #3719      +/-   ##
============================================
- Coverage     47.99%   47.98%   -0.01%     
- Complexity    16046    16059      +13     
============================================
  Files          1683     1683              
  Lines         96044    96094      +50     
  Branches      15387    15394       +7     
============================================
+ Hits          46093    46114      +21     
- Misses        44681    44713      +32     
+ Partials       5270     5267       -3     

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

@FliegendeWurst FliegendeWurst changed the title JavaRedux: Integer methods + NoSuchElementException JavaRedux: Integer methods + List::remove + NoSuchElementException Jan 21, 2026
@FliegendeWurst
Copy link
Member Author

I would like to add a test that checks the below is provable, how would I go about that?

    /*@ public normal_behavior
      @ ensures \result;
      @ assignable \nothing;
      @*/
    static boolean testRemove() {
        List list = new ArrayList();
        list.add("a");
        list.add("b");
        list.add("c");
        Object removed = list.remove(0);
        return removed == "a" && list.get(0) == "b" && list.get(1) == "c";
    }

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant