Skip to content

JavaRedux: Integer methods + List::remove + NoSuchElementException #3719

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
FliegendeWurst wants to merge 3 commits into
base: main
Choose a base branch
from
Open

JavaRedux: Integer methods + List::remove + NoSuchElementException #3719

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1604185
JavaRedux: Integer methods valueOf and intValue
FliegendeWurst Jan 14, 2026
c8bd40a
JavaRedux: NoSuchElementException class
FliegendeWurst Jan 14, 2026
e26aadc
JavaRedux: List::remove
FliegendeWurst Jan 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ java.util.ListIterator
java.lang.Long
java.lang.Boolean
java.util.Map
java.util.NoSuchElementException
java.util.Set
java.io.FilterOutputStream
java.io.InputStream
Expand Down
10 changes: 10 additions & 0 deletions key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Integer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ public final class Integer implements java.lang.Comparable
public final static java.lang.Class TYPE;
public final static int SIZE = 32;

private /*@ spec_public @*/ final int value;

public static java.lang.String toString(int arg0, int arg1);
public static java.lang.String toHexString(int arg0);
public static java.lang.String toOctalString(int arg0);
Expand All @@ -19,11 +21,19 @@ public final class Integer implements java.lang.Comparable
public static int parseInt(java.lang.String arg0) throws java.lang.NumberFormatException;
public static java.lang.Integer valueOf(java.lang.String arg0, int arg1) throws java.lang.NumberFormatException;
public static java.lang.Integer valueOf(java.lang.String arg0) throws java.lang.NumberFormatException;
/*@ public normal_behavior
@ ensures \result.value == arg0;
@ assignable \nothing;
@*/
public static java.lang.Integer valueOf(int arg0);
public Integer(int arg0);

@mattulbrich mattulbrich Aug 15, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

should there not also be an assignment to value or at least a contract with the effect in the constructor?

Similar to the static method above.

public Integer(java.lang.String arg0) throws java.lang.NumberFormatException;
public byte byteValue();
public short shortValue();
/*@ public normal_behavior
@ ensures \result == value;
@ assignable \strictly_nothing;
@*/
public int intValue();
public long longValue();

@mattulbrich mattulbrich Aug 15, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

at least the long conversion can be formulated in JML too.

// public float floatValue();
Expand Down
10 changes: 9 additions & 1 deletion key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/List.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,15 @@ public interface List extends java.util.Collection
@*/
public java.lang.Object get(int arg0);
public java.lang.Object set(int arg0, java.lang.Object arg1);


/*@ public normal_behavior
@ requires 0 <= idx && idx < seq.length;
@ ensures ((Object)\old(seq)[idx]) == \result;
@ ensures seq == \seq_concat(\old(seq)[0 .. idx], \old(seq)[idx + 1 .. \old(seq).length]);
@ assignable seq;
@*/
public java.lang.Object remove(int idx);

public int indexOf(java.lang.Object arg0);
public int lastIndexOf(java.lang.Object arg0);

Expand Down
9 changes: 9 additions & 0 deletions ...e/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/NoSuchElementException.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
package java.util;

import java.lang.RuntimeException;

public class NoSuchElementException extends RuntimeException {
public NoSuchElementException();

public NoSuchElementException(String s);
}
Loading