JavaRedux: Integer methods + List::remove + NoSuchElementException

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT

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

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/Integer.java

@@ -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);
@@ -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);
    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();
 //   public float floatValue();

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/List.java

@@ -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);
 

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/NoSuchElementException.java

@@ -0,0 +1,9 @@
+package java.util;
+
+import java.lang.RuntimeException;
+
+public class NoSuchElementException extends RuntimeException {
+   public NoSuchElementException();
+
+   public NoSuchElementException(String s);
+}