{@code Class} has no public constructor. Instead {@code Class} + * objects are constructed automatically by the Java Virtual Machine as classes + * are loaded and by calls to the {@code defineClass} method in the class + * loader. + * + *
The following example uses a {@code Class} object to print the + * class name of an object: + * + *
+ * void printClassName(Object obj) {
+ * System.out.println("The class of " + obj +
+ * " is " + obj.getClass().getName());
+ * }
+ * It is also possible to get the {@code Class} object for a named + * type (or for void) using a class literal. See Section 15.8.2 of + * The Java™ Language Specification. + * For example: + * + *
+ * {@code System.out.println("The name of class Foo is: "+Foo.class.getName());} + *+ * + * @param
application/x-www-form-urlencoded
+ * MIME format.
+ * + * The conversion process is the reverse of that used by the URLEncoder class. It is assumed + * that all characters in the encoded string are one of the following: + * "{@code a}" through "{@code z}", + * "{@code A}" through "{@code Z}", + * "{@code 0}" through "{@code 9}", and + * "{@code -}", "{@code _}", + * "{@code .}", and "{@code *}". The + * character "{@code %}" is allowed but is interpreted + * as the start of a special escaped sequence. + *
+ * The following rules are applied in the conversion: + * + *
+ * There are two possible ways in which this decoder could deal with + * illegal strings. It could either leave illegal characters alone or + * it could throw an {@link java.lang.IllegalArgumentException}. + * Which approach the decoder takes is left to the + * implementation. + * + * @author Mark Chamness + * @author Michael McCloskey + * @since 1.2 + */ + +public class URLDecoder { + + // The platform default encoding + static String dfltEncName = URLEncoder.dfltEncName; + + /** + * Decodes a {@code x-www-form-urlencoded} string. + * The platform's default encoding is used to determine what characters + * are represented by any consecutive sequences of the form + * "{@code %xy}". + * @param s the {@code String} to decode + * @deprecated The resulting string may vary depending on the platform's + * default encoding. Instead, use the decode(String,String) method + * to specify the encoding. + * @return the newly decoded {@code String} + */ + @Deprecated + public static String decode(String s) { + + String str = null; + + try { + str = decode(s, dfltEncName); + } catch (UnsupportedEncodingException e) { + // The system should always have the platform default + } + + return str; + } + + /** + * Decodes a {@code application/x-www-form-urlencoded} string using a specific + * encoding scheme. + * The supplied encoding is used to determine + * what characters are represented by any consecutive sequences of the + * form "{@code %xy}". + *
+ * Note: The
+ * World Wide Web Consortium Recommendation states that
+ * UTF-8 should be used. Not doing so may introduce
+ * incompatibilities.
+ *
+ * @param s the {@code String} to decode
+ * @param enc The name of a supported
+ * character
+ * encoding.
+ * @return the newly decoded {@code String}
+ * @exception UnsupportedEncodingException
+ * If character encoding needs to be consulted, but
+ * named character encoding is not supported
+ * @see URLEncoder#encode(java.lang.String, java.lang.String)
+ * @since 1.4
+ */
+ public static String decode(String s, String enc)
+ throws UnsupportedEncodingException{
+
+ boolean needToChange = false;
+ int numChars = s.length();
+ StringBuffer sb = new StringBuffer(numChars > 500 ? numChars / 2 : numChars);
+ int i = 0;
+
+ if (enc.length() == 0) {
+ throw new UnsupportedEncodingException ("URLDecoder: empty string enc parameter");
+ }
+
+ char c;
+ byte[] bytes = null;
+ while (i < numChars) {
+ c = s.charAt(i);
+ switch (c) {
+ case '+':
+ sb.append(' ');
+ i++;
+ needToChange = true;
+ break;
+ case '%':
+ /*
+ * Starting with this instance of %, process all
+ * consecutive substrings of the form %xy. Each
+ * substring %xy will yield a byte. Convert all
+ * consecutive bytes obtained this way to whatever
+ * character(s) they represent in the provided
+ * encoding.
+ */
+
+ try {
+
+ // (numChars-i)/3 is an upper bound for the number
+ // of remaining bytes
+ if (bytes == null)
+ bytes = new byte[(numChars-i)/3];
+ int pos = 0;
+
+ while ( ((i+2) < numChars) &&
+ (c=='%')) {
+ int v = Integer.parseInt(s.substring(i+1,i+3),16);
+ if (v < 0)
+ throw new IllegalArgumentException("URLDecoder: Illegal hex characters in escape (%) pattern - negative value");
+ bytes[pos++] = (byte) v;
+ i+= 3;
+ if (i < numChars)
+ c = s.charAt(i);
+ }
+
+ // A trailing, incomplete byte encoding such as
+ // "%x" will cause an exception to be thrown
+
+ if ((i < numChars) && (c=='%'))
+ throw new IllegalArgumentException(
+ "URLDecoder: Incomplete trailing escape (%) pattern");
+
+ sb.append(new String(bytes, 0, pos, enc));
+ } catch (NumberFormatException e) {
+ throw new IllegalArgumentException(
+ "URLDecoder: Illegal hex characters in escape (%) pattern - "
+ + e.getMessage());
+ }
+ needToChange = true;
+ break;
+ default:
+ sb.append(c);
+ i++;
+ break;
+ }
+ }
+
+ return (needToChange? sb.toString() : s);
+ }
+}
diff --git a/src/main/java/java/net/URLEncoder.java b/src/main/java/java/net/URLEncoder.java
new file mode 100644
index 0000000..86377b7
--- /dev/null
+++ b/src/main/java/java/net/URLEncoder.java
@@ -0,0 +1,292 @@
+/*
+ * Copyright (c) 1995, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.net;
+
+import java.io.ByteArrayOutputStream;
+import java.io.BufferedWriter;
+import java.io.OutputStreamWriter;
+import java.io.IOException;
+import java.io.UnsupportedEncodingException;
+import java.io.CharArrayWriter;
+import java.nio.charset.Charset;
+import java.nio.charset.IllegalCharsetNameException;
+import java.nio.charset.UnsupportedCharsetException ;
+import java.util.BitSet;
+import java.security.AccessController;
+import java.security.PrivilegedAction;
+import sun.security.action.GetBooleanAction;
+import sun.security.action.GetPropertyAction;
+
+/**
+ * Utility class for HTML form encoding. This class contains static methods
+ * for converting a String to the application/x-www-form-urlencoded MIME
+ * format. For more information about HTML form encoding, consult the HTML
+ * specification.
+ *
+ *
+ * When encoding a String, the following rules apply: + * + *
+ * For example using UTF-8 as the encoding scheme the string "The + * string ü@foo-bar" would get converted to + * "The+string+%C3%BC%40foo-bar" because in UTF-8 the character + * ü is encoded as two bytes C3 (hex) and BC (hex), and the + * character @ is encoded as one byte 40 (hex). + * + * @author Herb Jellinek + * @since JDK1.0 + */ +public class URLEncoder { + static BitSet dontNeedEncoding; + static final int caseDiff = ('a' - 'A'); + static String dfltEncName = null; + + static { + + /* The list of characters that are not encoded has been + * determined as follows: + * + * RFC 2396 states: + * ----- + * Data characters that are allowed in a URI but do not have a + * reserved purpose are called unreserved. These include upper + * and lower case letters, decimal digits, and a limited set of + * punctuation marks and symbols. + * + * unreserved = alphanum | mark + * + * mark = "-" | "_" | "." | "!" | "~" | "*" | "'" | "(" | ")" + * + * Unreserved characters can be escaped without changing the + * semantics of the URI, but this should not be done unless the + * URI is being used in a context that does not allow the + * unescaped character to appear. + * ----- + * + * It appears that both Netscape and Internet Explorer escape + * all special characters from this list with the exception + * of "-", "_", ".", "*". While it is not clear why they are + * escaping the other characters, perhaps it is safest to + * assume that there might be contexts in which the others + * are unsafe if not escaped. Therefore, we will use the same + * list. It is also noteworthy that this is consistent with + * O'Reilly's "HTML: The Definitive Guide" (page 164). + * + * As a last note, Intenet Explorer does not encode the "@" + * character which is clearly not unreserved according to the + * RFC. We are being consistent with the RFC in this matter, + * as is Netscape. + * + */ + + dontNeedEncoding = new BitSet(256); + int i; + for (i = 'a'; i <= 'z'; i++) { + dontNeedEncoding.set(i); + } + for (i = 'A'; i <= 'Z'; i++) { + dontNeedEncoding.set(i); + } + for (i = '0'; i <= '9'; i++) { + dontNeedEncoding.set(i); + } + dontNeedEncoding.set(' '); /* encoding a space to a + is done + * in the encode() method */ + dontNeedEncoding.set('-'); + dontNeedEncoding.set('_'); + dontNeedEncoding.set('.'); + dontNeedEncoding.set('*'); + + dfltEncName = AccessController.doPrivileged( + new GetPropertyAction("file.encoding") + ); + } + + /** + * You can't call the constructor. + */ + private URLEncoder() { } + + /** + * Translates a string into {@code x-www-form-urlencoded} + * format. This method uses the platform's default encoding + * as the encoding scheme to obtain the bytes for unsafe characters. + * + * @param s {@code String} to be translated. + * @deprecated The resulting string may vary depending on the platform's + * default encoding. Instead, use the encode(String,String) + * method to specify the encoding. + * @return the translated {@code String}. + */ + @Deprecated + public static String encode(String s) { + + String str = null; + + try { + str = encode(s, dfltEncName); + } catch (UnsupportedEncodingException e) { + // The system should always have the platform default + } + + return str; + } + + /** + * Translates a string into {@code application/x-www-form-urlencoded} + * format using a specific encoding scheme. This method uses the + * supplied encoding scheme to obtain the bytes for unsafe + * characters. + *
+ * Note: The + * World Wide Web Consortium Recommendation states that + * UTF-8 should be used. Not doing so may introduce + * incompatibilities. + * + * @param s {@code String} to be translated. + * @param enc The name of a supported + * character + * encoding. + * @return the translated {@code String}. + * @exception UnsupportedEncodingException + * If the named encoding is not supported + * @see URLDecoder#decode(java.lang.String, java.lang.String) + * @since 1.4 + */ + public static String encode(String s, String enc) + throws UnsupportedEncodingException { + + boolean needToChange = false; + StringBuffer out = new StringBuffer(s.length()); + Charset charset; + CharArrayWriter charArrayWriter = new CharArrayWriter(); + + if (enc == null) + throw new NullPointerException("charsetName"); + + try { + charset = Charset.forName(enc); + } catch (IllegalCharsetNameException e) { + throw new UnsupportedEncodingException(enc); + } catch (UnsupportedCharsetException e) { + throw new UnsupportedEncodingException(enc); + } + + for (int i = 0; i < s.length();) { + int c = (int) s.charAt(i); + //System.out.println("Examining character: " + c); + if (dontNeedEncoding.get(c)) { + if (c == ' ') { + c = '+'; + needToChange = true; + } + //System.out.println("Storing: " + c); + out.append((char)c); + i++; + } else { + // convert to external encoding before hex conversion + do { + charArrayWriter.write(c); + /* + * If this character represents the start of a Unicode + * surrogate pair, then pass in two characters. It's not + * clear what should be done if a bytes reserved in the + * surrogate pairs range occurs outside of a legal + * surrogate pair. For now, just treat it as if it were + * any other character. + */ + if (c >= 0xD800 && c <= 0xDBFF) { + /* + System.out.println(Integer.toHexString(c) + + " is high surrogate"); + */ + if ( (i+1) < s.length()) { + int d = (int) s.charAt(i+1); + /* + System.out.println("\tExamining " + + Integer.toHexString(d)); + */ + if (d >= 0xDC00 && d <= 0xDFFF) { + /* + System.out.println("\t" + + Integer.toHexString(d) + + " is low surrogate"); + */ + charArrayWriter.write(d); + i++; + } + } + } + i++; + } while (i < s.length() && !dontNeedEncoding.get((c = (int) s.charAt(i)))); + + charArrayWriter.flush(); + String str = new String(charArrayWriter.toCharArray()); + byte[] ba = str.getBytes(charset); + for (int j = 0; j < ba.length; j++) { + out.append('%'); + char ch = Character.forDigit((ba[j] >> 4) & 0xF, 16); + // converting to use uppercase letter as part of + // the hex value if ch is a letter. + if (Character.isLetter(ch)) { + ch -= caseDiff; + } + out.append(ch); + ch = Character.forDigit(ba[j] & 0xF, 16); + if (Character.isLetter(ch)) { + ch -= caseDiff; + } + out.append(ch); + } + charArrayWriter.reset(); + needToChange = true; + } + } + + return (needToChange? out.toString() : s); + } +} diff --git a/src/main/java/java/util/AbstractList.java b/src/main/java/java/util/AbstractList.java new file mode 100644 index 0000000..91745e5 --- /dev/null +++ b/src/main/java/java/util/AbstractList.java @@ -0,0 +1,895 @@ +/* + * Copyright (c) 1997, 2012, Oracle and/or its affiliates. All rights reserved. + * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER. + * + * This code is free software; you can redistribute it and/or modify it + * under the terms of the GNU General Public License version 2 only, as + * published by the Free Software Foundation. Oracle designates this + * particular file as subject to the "Classpath" exception as provided + * by Oracle in the LICENSE file that accompanied this code. + * + * This code is distributed in the hope that it will be useful, but WITHOUT + * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or + * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License + * version 2 for more details (a copy is included in the LICENSE file that + * accompanied this code). + * + * You should have received a copy of the GNU General Public License version + * 2 along with this work; if not, write to the Free Software Foundation, + * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. + * + * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA + * or visit www.oracle.com if you need additional information or have any + * questions. + */ + +package java.util; + +import org.cprover.CProver; + +/** + * This class provides a skeletal implementation of the {@link List} + * interface to minimize the effort required to implement this interface + * backed by a "random access" data store (such as an array). For sequential + * access data (such as a linked list), {@link AbstractSequentialList} should + * be used in preference to this class. + * + *
To implement an unmodifiable list, the programmer needs only to extend + * this class and provide implementations for the {@link #get(int)} and + * {@link List#size() size()} methods. + * + *
To implement a modifiable list, the programmer must additionally + * override the {@link #set(int, Object) set(int, E)} method (which otherwise + * throws an {@code UnsupportedOperationException}). If the list is + * variable-size the programmer must additionally override the + * {@link #add(int, Object) add(int, E)} and {@link #remove(int)} methods. + * + *
The programmer should generally provide a void (no argument) and collection + * constructor, as per the recommendation in the {@link Collection} interface + * specification. + * + *
Unlike the other abstract collection implementations, the programmer does + * not have to provide an iterator implementation; the iterator and + * list iterator are implemented by this class, on top of the "random access" + * methods: + * {@link #get(int)}, + * {@link #set(int, Object) set(int, E)}, + * {@link #add(int, Object) add(int, E)} and + * {@link #remove(int)}. + * + *
The documentation for each non-abstract method in this class describes its + * implementation in detail. Each of these methods may be overridden if the + * collection being implemented admits a more efficient implementation. + * + *
This class is a member of the
+ *
+ * Java Collections Framework.
+ *
+ * @author Josh Bloch
+ * @author Neal Gafter
+ * @since 1.2
+ */
+
+public abstract class AbstractList Lists that support this operation may place limitations on what
+ * elements may be added to this list. In particular, some
+ * lists will refuse to add null elements, and others will impose
+ * restrictions on the type of elements that may be added. List
+ * classes should clearly specify in their documentation any restrictions
+ * on what elements may be added.
+ *
+ * This implementation calls {@code add(size(), e)}.
+ *
+ * Note that this implementation throws an
+ * {@code UnsupportedOperationException} unless
+ * {@link #add(int, Object) add(int, E)} is overridden.
+ *
+ * @param e element to be appended to this list
+ * @return {@code true} (as specified by {@link Collection#add})
+ * @throws UnsupportedOperationException if the {@code add} operation
+ * is not supported by this list
+ * @throws ClassCastException if the class of the specified element
+ * prevents it from being added to this list
+ * @throws NullPointerException if the specified element is null and this
+ * list does not permit null elements
+ * @throws IllegalArgumentException if some property of this element
+ * prevents it from being added to this list
+ */
+ public boolean add(E e) {
+ add(size(), e);
+ return true;
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ * @throws IndexOutOfBoundsException {@inheritDoc}
+ */
+ abstract public E get(int index);
+
+ /**
+ * {@inheritDoc}
+ *
+ * This implementation always throws an
+ * {@code UnsupportedOperationException}.
+ *
+ * @throws UnsupportedOperationException {@inheritDoc}
+ * @throws ClassCastException {@inheritDoc}
+ * @throws NullPointerException {@inheritDoc}
+ * @throws IllegalArgumentException {@inheritDoc}
+ * @throws IndexOutOfBoundsException {@inheritDoc}
+ */
+ public E set(int index, E element) {
+ // throw new UnsupportedOperationException();
+ CProver.notModelled();
+ return CProver.nondetWithNullForNotModelled();
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ * This implementation always throws an
+ * {@code UnsupportedOperationException}.
+ *
+ * @throws UnsupportedOperationException {@inheritDoc}
+ * @throws ClassCastException {@inheritDoc}
+ * @throws NullPointerException {@inheritDoc}
+ * @throws IllegalArgumentException {@inheritDoc}
+ * @throws IndexOutOfBoundsException {@inheritDoc}
+ */
+ public void add(int index, E element) {
+ throw new UnsupportedOperationException();
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ * This implementation always throws an
+ * {@code UnsupportedOperationException}.
+ *
+ * @throws UnsupportedOperationException {@inheritDoc}
+ * @throws IndexOutOfBoundsException {@inheritDoc}
+ */
+ public E remove(int index) {
+ throw new UnsupportedOperationException();
+ }
+
+
+ // Search Operations
+
+ /**
+ * {@inheritDoc}
+ *
+ * This implementation first gets a list iterator (with
+ * {@code listIterator()}). Then, it iterates over the list until the
+ * specified element is found or the end of the list is reached.
+ *
+ * @throws ClassCastException {@inheritDoc}
+ * @throws NullPointerException {@inheritDoc}
+ */
+ public int indexOf(Object o) {
+ // ListIterator This implementation first gets a list iterator that points to the end
+ * of the list (with {@code listIterator(size())}). Then, it iterates
+ * backwards over the list until the specified element is found, or the
+ * beginning of the list is reached.
+ *
+ * @throws ClassCastException {@inheritDoc}
+ * @throws NullPointerException {@inheritDoc}
+ */
+ public int lastIndexOf(Object o) {
+ // ListIterator This implementation calls {@code removeRange(0, size())}.
+ *
+ * Note that this implementation throws an
+ * {@code UnsupportedOperationException} unless {@code remove(int
+ * index)} or {@code removeRange(int fromIndex, int toIndex)} is
+ * overridden.
+ *
+ * @throws UnsupportedOperationException if the {@code clear} operation
+ * is not supported by this list
+ */
+ public void clear() {
+ // removeRange(0, size());
+ CProver.notModelled();
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ * This implementation gets an iterator over the specified collection
+ * and iterates over it, inserting the elements obtained from the
+ * iterator into this list at the appropriate position, one at a time,
+ * using {@code add(int, E)}.
+ * Many implementations will override this method for efficiency.
+ *
+ * Note that this implementation throws an
+ * {@code UnsupportedOperationException} unless
+ * {@link #add(int, Object) add(int, E)} is overridden.
+ *
+ * @throws UnsupportedOperationException {@inheritDoc}
+ * @throws ClassCastException {@inheritDoc}
+ * @throws NullPointerException {@inheritDoc}
+ * @throws IllegalArgumentException {@inheritDoc}
+ * @throws IndexOutOfBoundsException {@inheritDoc}
+ */
+ public boolean addAll(int index, Collection c) {
+ rangeCheckForAdd(index);
+ boolean modified = false;
+ for (E e : c) {
+ add(index++, e);
+ modified = true;
+ }
+ return modified;
+ }
+
+
+ // Iterators
+
+ /**
+ * Returns an iterator over the elements in this list in proper sequence.
+ *
+ * This implementation returns a straightforward implementation of the
+ * iterator interface, relying on the backing list's {@code size()},
+ * {@code get(int)}, and {@code remove(int)} methods.
+ *
+ * Note that the iterator returned by this method will throw an
+ * {@link UnsupportedOperationException} in response to its
+ * {@code remove} method unless the list's {@code remove(int)} method is
+ * overridden.
+ *
+ * This implementation can be made to throw runtime exceptions in the
+ * face of concurrent modification, as described in the specification
+ * for the (protected) {@link #modCount} field.
+ *
+ * @return an iterator over the elements in this list in proper sequence
+ */
+ public Iterator This implementation returns {@code listIterator(0)}.
+ *
+ * @see #listIterator(int)
+ *
+ * @diffblue.fullSupport
+ * @diffblue.untested
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // This method is inherited by ArrayList$SubList.
+ public ListIterator This implementation returns a straightforward implementation of the
+ * {@code ListIterator} interface that extends the implementation of the
+ * {@code Iterator} interface returned by the {@code iterator()} method.
+ * The {@code ListIterator} implementation relies on the backing list's
+ * {@code get(int)}, {@code set(int, E)}, {@code add(int, E)}
+ * and {@code remove(int)} methods.
+ *
+ * Note that the list iterator returned by this implementation will
+ * throw an {@link UnsupportedOperationException} in response to its
+ * {@code remove}, {@code set} and {@code add} methods unless the
+ * list's {@code remove(int)}, {@code set(int, E)}, and
+ * {@code add(int, E)} methods are overridden.
+ *
+ * This implementation can be made to throw runtime exceptions in the
+ * face of concurrent modification, as described in the specification for
+ * the (protected) {@link #modCount} field.
+ *
+ * @throws IndexOutOfBoundsException {@inheritDoc}
+ */
+ public ListIterator This implementation returns a list that subclasses
+ * {@code AbstractList}. The subclass stores, in private fields, the
+ * offset of the subList within the backing list, the size of the subList
+ * (which can change over its lifetime), and the expected
+ * {@code modCount} value of the backing list. There are two variants
+ * of the subclass, one of which implements {@code RandomAccess}.
+ * If this list implements {@code RandomAccess} the returned list will
+ * be an instance of the subclass that implements {@code RandomAccess}.
+ *
+ * The subclass's {@code set(int, E)}, {@code get(int)},
+ * {@code add(int, E)}, {@code remove(int)}, {@code addAll(int,
+ * Collection)} and {@code removeRange(int, int)} methods all
+ * delegate to the corresponding methods on the backing abstract list,
+ * after bounds-checking the index and adjusting for the offset. The
+ * {@code addAll(Collection c)} method merely returns {@code addAll(size,
+ * c)}.
+ *
+ * The {@code listIterator(int)} method returns a "wrapper object"
+ * over a list iterator on the backing list, which is created with the
+ * corresponding method on the backing list. The {@code iterator} method
+ * merely returns {@code listIterator()}, and the {@code size} method
+ * merely returns the subclass's {@code size} field.
+ *
+ * All methods first check to see if the actual {@code modCount} of
+ * the backing list is equal to its expected value, and throw a
+ * {@code ConcurrentModificationException} if it is not.
+ *
+ * @throws IndexOutOfBoundsException if an endpoint index value is out of range
+ * {@code (fromIndex < 0 || toIndex > size)}
+ * @throws IllegalArgumentException if the endpoint indices are out of order
+ * {@code (fromIndex > toIndex)}
+ */
+ public List
+ *
+ * This implementation first checks if the specified object is this
+ * list. If so, it returns {@code true}; if not, it checks if the
+ * specified object is a list. If not, it returns {@code false}; if so,
+ * it iterates over both lists, comparing corresponding pairs of elements.
+ * If any comparison returns {@code false}, this method returns
+ * {@code false}. If either iterator runs out of elements before the
+ * other it returns {@code false} (as the lists are of unequal length);
+ * otherwise it returns {@code true} when the iterations complete.
+ *
+ * @param o the object to be compared for equality with this list
+ * @return {@code true} if the specified object is equal to this list
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // We currently cannot enable this method, or it will cause infinite
+ // unwinding loops for methods in ArrayList that use Object.equals, like
+ // remove(Object) and contains(Object).
+ public boolean equals(Object o) {
+ // if (o == this)
+ // return true;
+ // if (!(o instanceof List))
+ // return false;
+
+ // ListIterator This implementation uses exactly the code that is used to define the
+ * list hash function in the documentation for the {@link List#hashCode}
+ * method.
+ *
+ * @return the hash code value for this list
+ */
+ // DIFFBLUE MODEL LIBRARY
+ // Always returns 0, for consistency with Object.hashCode().
+ public int hashCode() {
+ // int hashCode = 1;
+ // for (E e : this)
+ // hashCode = 31*hashCode + (e==null ? 0 : e.hashCode());
+ // return hashCode;
+ return 0;
+ }
+
+ /**
+ * Removes from this list all of the elements whose index is between
+ * {@code fromIndex}, inclusive, and {@code toIndex}, exclusive.
+ * Shifts any succeeding elements to the left (reduces their index).
+ * This call shortens the list by {@code (toIndex - fromIndex)} elements.
+ * (If {@code toIndex==fromIndex}, this operation has no effect.)
+ *
+ * This method is called by the {@code clear} operation on this list
+ * and its subLists. Overriding this method to take advantage of
+ * the internals of the list implementation can substantially
+ * improve the performance of the {@code clear} operation on this list
+ * and its subLists.
+ *
+ * This implementation gets a list iterator positioned before
+ * {@code fromIndex}, and repeatedly calls {@code ListIterator.next}
+ * followed by {@code ListIterator.remove} until the entire range has
+ * been removed. Note: if {@code ListIterator.remove} requires linear
+ * time, this implementation requires quadratic time.
+ *
+ * @param fromIndex index of first element to be removed
+ * @param toIndex index after last element to be removed
+ */
+ protected void removeRange(int fromIndex, int toIndex) {
+ // ListIterator This field is used by the iterator and list iterator implementation
+ * returned by the {@code iterator} and {@code listIterator} methods.
+ * If the value of this field changes unexpectedly, the iterator (or list
+ * iterator) will throw a {@code ConcurrentModificationException} in
+ * response to the {@code next}, {@code remove}, {@code previous},
+ * {@code set} or {@code add} operations. This provides
+ * fail-fast behavior, rather than non-deterministic behavior in
+ * the face of concurrent modification during iteration.
+ *
+ * Use of this field by subclasses is optional. If a subclass
+ * wishes to provide fail-fast iterators (and list iterators), then it
+ * merely has to increment this field in its {@code add(int, E)} and
+ * {@code remove(int)} methods (and any other methods that it overrides
+ * that result in structural modifications to the list). A single call to
+ * {@code add(int, E)} or {@code remove(int)} must add no more than
+ * one to this field, or the iterators (and list iterators) will throw
+ * bogus {@code ConcurrentModificationExceptions}. If an implementation
+ * does not wish to provide fail-fast iterators, this field may be
+ * ignored.
+ */
+ protected transient int modCount = 0;
+
+ // DIFFBLUE MODEL LIBRARY
+ // String operations can significantly slow down JBMC in some
+ // cases. This should be reviewed again with improved versions of the string
+ // solver.
+ private void rangeCheckForAdd(int index) {
+ if (index < 0 || index > size())
+ // throw new IndexOutOfBoundsException(outOfBoundsMsg(index));
+ throw new IndexOutOfBoundsException();
+ }
+
+ // DIFFBLUE MODEL LIBRARY
+ // String operations can significantly slow down JBMC in some
+ // cases. This should be reviewed again with improved versions of the string
+ // solver.
+ // private String outOfBoundsMsg(int index) {
+ // return "Index: "+index+", Size: "+size();
+ // }
+
+ /**
+ * @diffblue.fullSupport
+ * In the JDK, this method is inherited from AbstractCollection.
+ * This may be slow to generate traces for LinkedList-type
+ * Lists.
+ * See docs in {@link AbstractCollection#toString()}
+ */
+ @Override
+ public String toString() {
+ StringBuilder b = new StringBuilder();
+ b.append('[');
+
+ int len = size();
+ // append first length - 1 elements
+ for (int i = 0; i < len - 1; i++) {
+ b.append(get(i));
+ b.append(", ");
+ }
+
+ // then the final element
+ if (len > 0) {
+ b.append(get(len - 1));
+ }
+
+ b.append(']');
+ return b.toString();
+ }
+
+ // DIFFBLUE MODEL LIBRARY
+ // This method is called by CBMC just after nondeterministic object
+ // creation, i.e. the constraints that it specifies are only enforced at
+ // that time and do not have to hold globally.
+ // We generally want to make sure that all necessary invariants of the class
+ // are satisfied, and potentially restrict some fields to speed up test
+ // generation.
+ @org.cprover.MustNotThrow
+ protected void cproverNondetInitialize() {
+ CProver.assume(modCount >= 0);
+ }
+}
+
+class SubList
+ *
+ * The process of implementing a set by extending this class is identical
+ * to that of implementing a Collection by extending AbstractCollection,
+ * except that all of the methods and constructors in subclasses of this
+ * class must obey the additional constraints imposed by the Set
+ * interface (for instance, the add method must not permit addition of
+ * multiple instances of an object to a set).
+ *
+ * Note that this class does not override any of the implementations from
+ * the AbstractCollection class. It merely adds implementations
+ * for equals and hashCode.
+ *
+ * This class is a member of the
+ *
+ * Java Collections Framework.
+ *
+ * @param
+ *
+ * This implementation first checks if the specified object is this
+ * set; if so it returns true. Then, it checks if the
+ * specified object is a set whose size is identical to the size of
+ * this set; if not, it returns false. If so, it returns
+ * containsAll((Collection) o).
+ *
+ * @param o object to be compared for equality with this set
+ * @return true if the specified object is equal to this set
+ */
+ public boolean equals(Object o) {
+ // if (o == this)
+ // return true;
+
+ // if (!(o instanceof Set))
+ // return false;
+ // Collection c = (Collection) o;
+ // if (c.size() != size())
+ // return false;
+ // try {
+ // return containsAll(c);
+ // } catch (ClassCastException unused) {
+ // return false;
+ // } catch (NullPointerException unused) {
+ // return false;
+ // }
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /**
+ * Returns the hash code value for this set. The hash code of a set is
+ * defined to be the sum of the hash codes of the elements in the set,
+ * where the hash code of a null element is defined to be zero.
+ * This ensures that s1.equals(s2) implies that
+ * s1.hashCode()==s2.hashCode() for any two sets s1
+ * and s2, as required by the general contract of
+ * {@link Object#hashCode}.
+ *
+ * This implementation iterates over the set, calling the
+ * hashCode method on each element in the set, and adding up
+ * the results.
+ *
+ * @return the hash code value for this set
+ * @see Object#equals(Object)
+ * @see Set#equals(Object)
+ */
+ public int hashCode() {
+ // int h = 0;
+ // Iterator This implementation determines which is the smaller of this set
+ * and the specified collection, by invoking the size
+ * method on each. If this set has fewer elements, then the
+ * implementation iterates over this set, checking each element
+ * returned by the iterator in turn to see if it is contained in
+ * the specified collection. If it is so contained, it is removed
+ * from this set with the iterator's remove method. If
+ * the specified collection has fewer elements, then the
+ * implementation iterates over the specified collection, removing
+ * from this set each element returned by the iterator, using this
+ * set's remove method.
+ *
+ * Note that this implementation will throw an
+ * UnsupportedOperationException if the iterator returned by the
+ * iterator method does not implement the remove method.
+ *
+ * @param c collection containing elements to be removed from this set
+ * @return true if this set changed as a result of the call
+ * @throws UnsupportedOperationException if the removeAll operation
+ * is not supported by this set
+ * @throws ClassCastException if the class of an element of this set
+ * is incompatible with the specified collection
+ * (optional)
+ * @throws NullPointerException if this set contains a null element and the
+ * specified collection does not permit null elements
+ * (optional),
+ * or if the specified collection is null
+ * @see #remove(Object)
+ * @see #contains(Object)
+ */
+ public boolean removeAll(Collection c) {
+ // Objects.requireNonNull(c);
+ // boolean modified = false;
+
+ // if (size() > c.size()) {
+ // for (Iterator i = c.iterator(); i.hasNext(); )
+ // modified |= remove(i.next());
+ // } else {
+ // for (Iterator i = iterator(); i.hasNext(); ) {
+ // if (c.contains(i.next())) {
+ // i.remove();
+ // modified = true;
+ // }
+ // }
+ // }
+ // return modified;
+ CProver.notModelled();
+ return CProver.nondetBoolean();
+ }
+
+ /*
+ * @diffblue.noSupport
+ * This method cannot be modelled because the iterator
+ * cannot be guaranteed to be return the elements in the same
+ * order from models-library as in the jdk.
+ * It is added here to override AbstractCollection as a safeguard so
+ * that if in the future toString() is implemented it more generally
+ * in AbstractCollection, this will not allow Sets to use that
+ * method, which would generate traces that do not pass because
+ * equality between the returned Strings cannot be asserted.
+ */
+ @Override
+ public String toString() {
+ CProver.notModelled();
+ return CProver.nondetWithoutNullForNotModelled();
+ }
+
+}
diff --git a/src/main/java/java/util/ArrayList.java b/src/main/java/java/util/ArrayList.java
new file mode 100644
index 0000000..f378380
--- /dev/null
+++ b/src/main/java/java/util/ArrayList.java
@@ -0,0 +1,1853 @@
+/*
+ * Copyright (c) 1997, 2013, Oracle and/or its affiliates. All rights reserved.
+ * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
+ *
+ * This code is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License version 2 only, as
+ * published by the Free Software Foundation. Oracle designates this
+ * particular file as subject to the "Classpath" exception as provided
+ * by Oracle in the LICENSE file that accompanied this code.
+ *
+ * This code is distributed in the hope that it will be useful, but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+ * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
+ * version 2 for more details (a copy is included in the LICENSE file that
+ * accompanied this code).
+ *
+ * You should have received a copy of the GNU General Public License version
+ * 2 along with this work; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
+ *
+ * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
+ * or visit www.oracle.com if you need additional information or have any
+ * questions.
+ */
+
+package java.util;
+
+import java.util.function.Consumer;
+import java.util.function.Predicate;
+import java.util.function.UnaryOperator;
+
+import org.cprover.CProver;
+
+/**
+ * Resizable-array implementation of the List interface. Implements
+ * all optional list operations, and permits all elements, including
+ * null. In addition to implementing the List interface,
+ * this class provides methods to manipulate the size of the array that is
+ * used internally to store the list. (This class is roughly equivalent to
+ * Vector, except that it is unsynchronized.)
+ *
+ * The size, isEmpty, get, set,
+ * iterator, and listIterator operations run in constant
+ * time. The add operation runs in amortized constant time,
+ * that is, adding n elements requires O(n) time. All of the other operations
+ * run in linear time (roughly speaking). The constant factor is low compared
+ * to that for the LinkedList implementation.
+ *.grow
+ * Each ArrayList instance has a capacity. The capacity is
+ * the size of the array used to store the elements in the list. It is always
+ * at least as large as the list size. As elements are added to an ArrayList,
+ * its capacity grows automatically. The details of the growth policy are not
+ * specified beyond the fact that adding an element has constant amortized
+ * time cost.
+ *
+ * An application can increase the capacity of an ArrayList instance
+ * before adding a large number of elements using the ensureCapacity
+ * operation. This may reduce the amount of incremental reallocation.
+ *
+ * Note that this implementation is not synchronized.
+ * If multiple threads access an ArrayList instance concurrently,
+ * and at least one of the threads modifies the list structurally, it
+ * must be synchronized externally. (A structural modification is
+ * any operation that adds or deletes one or more elements, or explicitly
+ * resizes the backing array; merely setting the value of an element is not
+ * a structural modification.) This is typically accomplished by
+ * synchronizing on some object that naturally encapsulates the list.
+ *
+ * If no such object exists, the list should be "wrapped" using the
+ * {@link Collections#synchronizedList Collections.synchronizedList}
+ * method. This is best done at creation time, to prevent accidental
+ * unsynchronized access to the list:
+ * The iterators returned by this class's {@link #iterator() iterator} and
+ * {@link #listIterator(int) listIterator} methods are fail-fast:
+ * if the list is structurally modified at any time after the iterator is
+ * created, in any way except through the iterator's own
+ * {@link ListIterator#remove() remove} or
+ * {@link ListIterator#add(Object) add} methods, the iterator will throw a
+ * {@link ConcurrentModificationException}. Thus, in the face of
+ * concurrent modification, the iterator fails quickly and cleanly, rather
+ * than risking arbitrary, non-deterministic behavior at an undetermined
+ * time in the future.
+ *
+ * Note that the fail-fast behavior of an iterator cannot be guaranteed
+ * as it is, generally speaking, impossible to make any hard guarantees in the
+ * presence of unsynchronized concurrent modification. Fail-fast iterators
+ * throw {@code ConcurrentModificationException} on a best-effort basis.
+ * Therefore, it would be wrong to write a program that depended on this
+ * exception for its correctness: the fail-fast behavior of iterators
+ * should be used only to detect bugs.
+ *
+ * This class is a member of the
+ *
+ * Java Collections Framework.
+ *
+ * @author Josh Bloch
+ * @author Neal Gafter
+ * @see Collection
+ * @see List
+ * @see LinkedList
+ * @see Vector
+ * @since 1.2
+ *
+ * @diffblue.limitedSupport
+ *
+ * For performance reasons, there may be restrictions on the number of elements
+ * that can be stored in the model of ArrayList:
+ * The The number of elements in the list is limited by
+ * CProver.defaultContainerCapacity().
+ * The number of elements in the list is limited to
+ * CProver.defaultContainerCapacity() for performance reasons.
+ *
+ * List list = Collections.synchronizedList(new ArrayList(...));
+ *
+ *
+ *
+ */
+
+public class ArrayListinitialCapacity value is limited to 2^27, to avoid
+ * generating tests that might exceed the memory limits of the JVM.
+ * The number of elements of an array list created this way is limited by
+ * CProver.defaultContainerCapacity() for performance reasons.
+ *