0001: // @(#)$Id: JMLObjectSequence.java 1.3 Mon, 09 May 2005 15:27:50 +0200 engelc $
0002:
0003: // Copyright (C) 1998, 1999 Iowa State University
0004:
0005: // This file is part of JML
0006:
0007: // JML is free software; you can redistribute it and/or modify
0008: // it under the terms of the GNU General Public License as published by
0009: // the Free Software Foundation; either version 2, or (at your option)
0010: // any later version.
0011:
0012: // JML is distributed in the hope that it will be useful,
0013: // but WITHOUT ANY WARRANTY; without even the implied warranty of
0014: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0015: // GNU General Public License for more details.
0016:
0017: // You should have received a copy of the GNU General Public License
0018: // along with JML; see the file COPYING. If not, write to
0019: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
0020:
0021: package org.jmlspecs.models;
0022:
0023: import java.math.BigInteger;
0024:
0025: /** Sequences of objects. This type uses "=="
0026: * to compare elements, and does not clone elements that are passed into
0027: * and returned from the sequence's methods.
0028: *
0029: * <p> The informal model for a JMLObjectSequence is a finite
0030: * mathematical sequence of elements (of type {@link Object}). In
0031: * some examples, we will write
0032: * <<em>a</em>,<em>b</em>,<em>c</em>> for a mathematical
0033: * sequence of length 3, containing elements <em>a</em>, <em>b</em>,
0034: * and <em>c</em>. Elements of sequences are "indexed" from 0, so the
0035: * length of a sequence is always 1 more than the index of the last
0036: * element in the sequence.
0037: *
0038: * @version $Revision: 1.3 $
0039: * @author Gary T. Leavens
0040: * @author Albert L. Baker
0041: * @see JMLCollection
0042: * @see JMLType
0043: * @see JMLValueSequence
0044: * @see JMLObjectSequenceEnumerator
0045: *
0046: */
0047: //-@ immutable
0048: public/*@ pure @*/class JMLObjectSequence implements JMLCollection {
0049:
0050: //*********************** equational theory ***********************
0051:
0052: /*@ public invariant (\forall JMLObjectSequence s2;
0053: @ (\forall Object e1, e2;
0054: @ (\forall \bigint n;
0055: @ equational_theory(this, s2, e1, e2, n) )));
0056: @*/
0057:
0058: /** An equational specification of the properties of sequences.
0059: */
0060: /*@ public normal_behavior
0061: @ {|
0062: @ // The following are defined by observations (itemAt) and induction.
0063: @
0064: @ ensures \result <==> !(new JMLObjectSequence()).has(e1);
0065: @ also
0066: @ ensures \result <==> (new JMLObjectSequence()).size() == 0;
0067: @ also
0068: @ ensures \result <==> (new JMLObjectSequence(e1)).size() == 1;
0069: @ also
0070: @ ensures \result <==>
0071: @ e1 != null ==>
0072: @ (new JMLObjectSequence(e1)).itemAt(0) == e1;
0073: @ also
0074: @ ensures \result <==>
0075: @ e1 != null ==>
0076: @ s.insertFront(e1).first() == e1;
0077: @ also
0078: @ ensures \result <==>
0079: @ e1 != null ==>
0080: @ s.insertBack(e1).last() == e1;
0081: @ also
0082: @ ensures \result <==>
0083: @ e1 != null ==>
0084: @ s.insertFront(e1).itemAt(0) == e1;
0085: @ also
0086: @ ensures \result <==>
0087: @ s.insertFront(e1).size() == s.size() + 1;
0088: @ also
0089: @ ensures \result <==>
0090: @ e1 != null ==>
0091: @ s.insertBack(e1).itemAt(s.size()) == e1;
0092: @ also
0093: @ ensures \result <==>
0094: @ s.insertBack(e1).size() == s.size() + 1;
0095: @ also
0096: @ ensures \result <==>
0097: @ // !FIXME! The following may be inconsistent: argument to itemAt might
0098: @ // be equal to size, but it is required to be less than size.
0099: @ -1 <= n && n < s.size() && e1 != null
0100: @ ==> s.insertAfterIndex(n, e1).itemAt(n+1) == e1;
0101: @ also
0102: @ ensures \result <==>
0103: @ -1 <= n && n < s.size()
0104: @ ==> s.insertAfterIndex(n, e1).size() == s.size() + 1;
0105: @ also
0106: @ ensures \result <==>
0107: @ 0 <= n && n <= s.size() && e1 != null
0108: @ ==> s.insertBeforeIndex(n, e1).itemAt(n) == e1;
0109: @ also
0110: @ ensures \result <==>
0111: @ 0 <= n && n <= s.size()
0112: @ ==> s.insertBeforeIndex(n, e1).size() == s.size() + 1;
0113: @ also
0114: @ ensures \result <==>
0115: @ s.isPrefix(s2)
0116: @ == (\forall int i; 0 <= i && i < s.int_length();
0117: @ (s2.itemAt(i) != null
0118: @ && s2.itemAt(i) == (s.itemAt(i)))
0119: @ || (s2.itemAt(i) == null && s.itemAt(i) == null) );
0120: @ also
0121: @ ensures \result <==>
0122: @ s.isSubsequence(s2)
0123: @ == s.int_length() <= s2.int_length()
0124: @ && (s.isPrefix(s2) || s.isSubsequence(s2.trailer()) );
0125: @
0126: @ // The following are all defined as abbreviations.
0127: @
0128: @ also
0129: @ ensures \result <==>
0130: @ s.isEmpty() == (s.size() == 0);
0131: @ also
0132: @ ensures \result <==>
0133: @ s.isEmpty() == (s.length == 0);
0134: @ also
0135: @ ensures \result <==>
0136: @ (new JMLObjectSequence(e1)).equals(
0137: @ new JMLObjectSequence().insertFront(e1));
0138: @ also
0139: @ ensures \result <==>
0140: @ (new JMLObjectSequence(e1)).equals(
0141: @ new JMLObjectSequence().insertBack(e1));
0142: @ also
0143: @ ensures \result <==>
0144: @ (new JMLObjectSequence(e1)).equals(
0145: @ new JMLObjectSequence().insertAfterIndex(-1, e1));
0146: @ also
0147: @ ensures \result <==>
0148: @ (new JMLObjectSequence(e1)).equals(
0149: @ new JMLObjectSequence().insertBeforeIndex(0, e1));
0150: @ also
0151: @ ensures \result <==>
0152: @ (s.size() >= 1 ==> s.equals(s.trailer().insertFront(s.first())));
0153: @ also
0154: @ ensures \result <==>
0155: @ (s.size() >= 1 ==> s.equals(s.header().insertBack(s.last())));
0156: @ also
0157: @ ensures \result <==>
0158: @ s.isProperSubsequence(s2)
0159: @ == ( s.isSubsequence(s2) && !s.equals(s2));
0160: @ also
0161: @ ensures \result <==>
0162: @ s.isSupersequence(s2) == s2.isSubsequence(s);
0163: @ also
0164: @ ensures \result <==>
0165: @ s.isProperSupersequence(s2) == s2.isProperSubsequence(s);
0166: @ |}
0167: @
0168: public pure model boolean equational_theory(JMLObjectSequence s,
0169: JMLObjectSequence s2,
0170: Object e1,
0171: Object e2, \bigint n);
0172: @*/
0173:
0174: /*@ requires true;
0175: @ public static model pure BigInteger bigintToBigInteger(\bigint biValue);
0176: @*/
0177:
0178: /*@ public normal_behavior
0179: @ requires oBi.equals(BigInteger.ZERO);
0180: @ ensures \result == (\bigint)0;
0181: @ public static model pure \bigint bigIntegerToBigint(BigInteger oBi);
0182: @*/
0183:
0184: //@ public invariant elementType <: \type(Object);
0185: /*@ public invariant
0186: @ (\forall Object o; o != null && has(o);
0187: @ \typeof(o) <: elementType);
0188: @*/
0189:
0190: //@ public invariant_redundantly isEmpty() ==> !containsNull;
0191: protected final JMLListObjectNode theSeq;
0192: // in objectState;
0193: //@ invariant theSeq != null ==> theSeq.owner == this;
0194:
0195: protected final BigInteger _length;
0196:
0197: // in objectState;
0198: //@ public model \bigint length;
0199: //@ protected represents length <- bigIntegerToBigint(_length);
0200:
0201: //@ protected invariant theSeq == null <==> length == 0;
0202: //@ protected invariant length >= 0;
0203:
0204: /*@ protected invariant theSeq != null ==> length == theSeq.length();
0205: @ protected invariant length == length();
0206: @*/
0207:
0208: //@ public invariant owner == null;
0209: /*@ public normal_behavior
0210: @ assignable objectState, elementType, containsNull, owner;
0211: @ ensures isEmpty();
0212: @ ensures_redundantly size() == 0;
0213: @*/
0214: public JMLObjectSequence() {
0215: theSeq = null;
0216: _length = BigInteger.ZERO;
0217: }
0218:
0219: /*@ public normal_behavior
0220: @ assignable objectState, elementType, containsNull, owner;
0221: @ ensures int_length() == 1;
0222: @ ensures (e == null ==> itemAt(0) == null)
0223: @ && (e != null ==> itemAt(0) == e);
0224: @*/
0225: public JMLObjectSequence(Object e) {
0226: theSeq = JMLListObjectNode.cons(e, null); // cons() clones e, if needed
0227: _length = BigInteger.ONE;
0228: }
0229:
0230: /*@ public normal_behavior
0231: @ requires ls == null <==> len == 0;
0232: @ requires len >= 0;
0233: @ assignable objectState, elementType, containsNull, owner;
0234: @ ensures ls != null ==> elementType == ls.elementType;
0235: @ ensures ls != null ==> containsNull == ls.containsNull;
0236: @ ensures ls == null ==> elementType <: \type(Object);
0237: @ ensures ls == null ==> !containsNull;
0238: model protected JMLObjectSequence (JMLListObjectNode ls, \bigint len);
0239: @*/
0240:
0241: /** Initialize this sequence based on the given representation.
0242: */
0243: //@ requires ls == null <==> len == 0;
0244: //@ requires len >= 0;
0245: //@ assignable objectState, elementType, containsNull, owner;
0246: //@ ensures ls != null ==> elementType == ls.elementType;
0247: //@ ensures ls != null ==> containsNull == ls.containsNull;
0248: //@ ensures ls == null ==> elementType <: \type(Object);
0249: //@ ensures ls == null ==> !containsNull;
0250: protected JMLObjectSequence(JMLListObjectNode ls, int len) {
0251: theSeq = ls;
0252: _length = BigInteger.valueOf(len);
0253: }
0254:
0255: //**************************** Static methods ****************************
0256:
0257: /** The empty JMLObjectSequence.
0258: * @see #JMLObjectSequence()
0259: */
0260: public static final/*@ non_null @*/JMLObjectSequence EMPTY = new JMLObjectSequence();
0261:
0262: /** Return the singleton sequence containing the given element.
0263: * @see #JMLObjectSequence(Object)
0264: */
0265: /*@ public normal_behavior
0266: @ assignable \nothing;
0267: @ ensures \result != null && \result.equals(new JMLObjectSequence(e));
0268: @*/
0269: public static/*@ pure @*//*@ non_null @*/
0270: JMLObjectSequence singleton(Object e) {
0271: return new JMLObjectSequence(e);
0272: }
0273:
0274: /** Return the sequence containing all the elements in the given
0275: * array in the same order as the elements appear in the array.
0276: */
0277: /*@ public normal_behavior
0278: @ requires a != null;
0279: @ assignable \nothing;
0280: @ ensures \result != null && \result.size() == a.length
0281: @ && (\forall int i; 0 <= i && i < a.length;
0282: @ (\result.itemAt(i) == null
0283: @ ? a[i] == null
0284: @ : \result.itemAt(i) == a[i]));
0285: @*/
0286: public static/*@ pure @*//*@ non_null @*/
0287: JMLObjectSequence convertFrom(/*@ non_null @*/Object[] a) {
0288: /*@ non_null @*/JMLObjectSequence ret = EMPTY;
0289: for (int i = a.length - 1; 0 <= i; i--) {
0290: ret = ret.insertFront(a[i]);
0291: }
0292: return ret;
0293: }
0294:
0295: /** Return the sequence containing the first 'size' elements in the given
0296: * array in the same order as the elements appear in the array.
0297: */
0298: /*@ public normal_behavior
0299: @ requires a != null && 0 <= size && size < a.length;
0300: @ assignable \nothing;
0301: @ ensures \result != null && \result.size() == size
0302: @ && (\forall int i; 0 <= i && i < size;
0303: @ (\result.itemAt(i) == null
0304: @ ? a[i] == null
0305: @ : \result.itemAt(i) == a[i]));
0306: @
0307: @ implies_that
0308: @ requires size < a.length;
0309: @*/
0310: public static/*@ pure @*//*@ non_null @*/
0311: JMLObjectSequence convertFrom(/*@ non_null @*/Object[] a, int size) {
0312: /*@ non_null @*/JMLObjectSequence ret = EMPTY;
0313: for (int i = size - 1; 0 <= i; i--) {
0314: ret = ret.insertFront(a[i]);
0315: }
0316: return ret;
0317: }
0318:
0319: /** Return the sequence containing all the object in the
0320: * given collection in the same order as the elements appear in the
0321: * collection.
0322: *
0323: * @throws ClassCastException if some element in c is not an instance of
0324: * Object.
0325: * @see #containsAll(java.util.Collection)
0326: */
0327: /*@ public normal_behavior
0328: @ requires c != null
0329: @ && c.elementType <: \type(Object);
0330: @ requires c.size() < Integer.MAX_VALUE;
0331: @ assignable \nothing;
0332: @ ensures \result != null && \result.size() == c.size()
0333: @ && (\forall Object x; c.contains(x) <==> \result.has(x));
0334: @ also
0335: @ public exceptional_behavior
0336: @ requires c != null && (\exists Object o; c.contains(o);
0337: @ !(o instanceof Object));
0338: @ assignable \nothing;
0339: @ signals (ClassCastException);
0340: @*/
0341: public static/*@ pure @*//*@ non_null @*/
0342: JMLObjectSequence convertFrom(
0343: /*@ non_null @*/java.util.Collection c)
0344: throws ClassCastException {
0345: /*@ non_null @*/JMLObjectSequence ret = EMPTY;
0346: java.util.Iterator celems = c.iterator();
0347: while (celems.hasNext()) {
0348: Object o = celems.next();
0349: if (o == null) {
0350: ret = ret.insertBack(null);
0351: } else {
0352: ret = ret.insertBack(o);
0353: }
0354: }
0355: return ret;
0356: }
0357:
0358: /** Return the sequence containing all the object in the
0359: * given JMLCollection in the same order as the elements appear in the
0360: * collection.
0361: *
0362: * @throws ClassCastException if some element in c is not an instance of
0363: * Object.
0364: */
0365: /*@ public normal_behavior
0366: @ requires c != null
0367: @ && c.elementType <: \type(Object);
0368: @ requires c.size() < Integer.MAX_VALUE;
0369: @ assignable \nothing;
0370: @ ensures \result != null
0371: @ && (\forall Object x; c.has(x) <==> \result.has(x));
0372: @ ensures_redundantly \result.size() == c.size();
0373: @ also
0374: @ public exceptional_behavior
0375: @ requires c != null && (\exists Object o; c.has(o);
0376: @ !(o instanceof Object));
0377: @ assignable \nothing;
0378: @ signals (ClassCastException);
0379: @*/
0380: public static/*@ pure @*//*@ non_null @*/
0381: JMLObjectSequence convertFrom(/*@ non_null @*/JMLCollection c)
0382: throws ClassCastException {
0383: /*@ non_null @*/JMLObjectSequence ret = EMPTY;
0384: JMLIterator celems = c.iterator();
0385: while (celems.hasNext()) {
0386: Object o = celems.next();
0387: if (o == null) {
0388: ret = ret.insertBack(null);
0389: } else {
0390: ret = ret.insertBack(o);
0391: }
0392: }
0393: return ret;
0394: }
0395:
0396: //**************************** Observers **********************************
0397:
0398: /** Return the element at the given zero-based index.
0399: * @param i the zero-based index into the sequence.
0400: * @exception JMLSequenceException if the index oBiI is out of range.
0401: * @see #get(int)
0402: * @see #has(Object)
0403: * @see #count(Object)
0404: */
0405: /*@ // _ alsoIfValue _ //FIXME! later
0406: @ public normal_behavior
0407: @ requires 0 <= i && i < length;
0408: @ ensures \result != null ==> \typeof(\result) <: elementType;
0409: @ ensures !containsNull ==> \result != null;
0410: @ also
0411: @ public exceptional_behavior
0412: @ requires !(0 <= i && i < length);
0413: @ signals (JMLSequenceException);
0414: model public Object itemAt(\bigint i) throws JMLSequenceException;
0415: @*/
0416:
0417: /** Return the element at the given zero-based index.
0418: * @param i the zero-based index into the sequence.
0419: * @exception JMLSequenceException if the index i is out of range.
0420: * @see #get(int)
0421: * @see #has(Object)
0422: * @see #count(Object)
0423: * @see #itemAt(\bigint)
0424: */
0425: /*@
0426: @ public normal_behavior
0427: @ requires 0 <= i && i < int_size();
0428: @ ensures \result != null ==> \typeof(\result) <: elementType;
0429: @ ensures !containsNull ==> \result != null;
0430: @ also
0431: @ public exceptional_behavior
0432: @ requires !(0 <= i && i < int_size());
0433: @ signals (JMLSequenceException);
0434: @*/
0435: public Object itemAt(int i) throws JMLSequenceException {
0436: if (i < 0 || i >= int_length()) {
0437: throw new JMLSequenceException("Index out of range.");
0438: } else {
0439: JMLListObjectNode this Walker = theSeq;
0440:
0441: int k = 0;
0442: //@ loop_invariant 0 <= k && k <= i && thisWalker != null;
0443: for (; k < i; k++) {
0444: this Walker = this Walker.next;
0445: }
0446: return (this Walker.head()); // head() clones if necessary
0447: }
0448: }
0449:
0450: /** Return the element at the given zero-based index; a synonym
0451: * for {@link #itemAt}.
0452: * @param i the zero-based index into the sequence.
0453: * @exception IndexOutOfBoundsException if the index i is out of range.
0454: * @see #itemAt(\bigint)
0455: */
0456: /*@ public normal_behavior
0457: @ requires 0 <= i && i < length; //FIXME, might use size();
0458: @ ensures
0459: @ (* \result == null, if the ith element of this is null;
0460: @ otherwise, \result "==" the ith element of this *);
0461: @ also
0462: @ public exceptional_behavior
0463: @ requires !(0 <= i && i < length); //FIXME, might use size());
0464: @ signals (IndexOutOfBoundsException);
0465: @
0466: @ model public Object get(\bigint i) throws IndexOutOfBoundsException ;
0467: @*/
0468:
0469: /** Return the element at the given zero-based index; a synonym
0470: * for {@link #itemAt}.
0471: * @param i the zero-based index into the sequence.
0472: * @exception IndexOutOfBoundsException if the index i is out of range.
0473: * @see #itemAt(int)
0474: */
0475: /*@ public normal_behavior
0476: @ requires 0 <= i && i < length;
0477: @ also
0478: @ public exceptional_behavior
0479: @ requires !(0 <= i && i < length);
0480: @ signals (IndexOutOfBoundsException);
0481: @
0482: @*/
0483: public Object get(int i) throws IndexOutOfBoundsException {
0484: try {
0485: Object ret = itemAt(i);
0486: return ret;
0487: } catch (JMLSequenceException e) {
0488: IndexOutOfBoundsException e2 = new IndexOutOfBoundsException();
0489: e2.initCause(e);
0490: throw e2;
0491: }
0492: }
0493:
0494: /*@
0495: @ public normal_behavior
0496: @ ensures \result == length;
0497: @ public model pure \bigint size();
0498: @*/
0499:
0500: /*@
0501: @ public normal_behavior
0502: @ ensures \result == length;
0503: @ public model pure \bigint length();
0504: @*/
0505:
0506: /*@ also
0507: @ protected normal_behavior
0508: @ requires size() <= Integer.MAX_VALUE;
0509: @ ensures \result == size();
0510: @
0511: @*/
0512: public int int_size() {
0513: return _length.intValue();
0514: }
0515:
0516: /*@
0517: @ public normal_behavior
0518: @ requires size() <= Integer.MAX_VALUE;
0519: @ ensures \result == size();
0520: @*/
0521: public int int_length() {
0522: return _length.intValue();
0523: }
0524:
0525: /*@
0526: @ public normal_behavior
0527: @ requires item != null;
0528: @ ensures \result
0529: @ == (\num_of \bigint i; 0 <= i && i < length();
0530: @ itemAt(i) != null
0531: @ && itemAt(i) == item);
0532: @ also
0533: @ public normal_behavior
0534: @ requires item == null;
0535: @ ensures \result == (\num_of \bigint i; 0 <= i && i < length();
0536: @ itemAt(i) == null);
0537: model public \bigint bi_count(Object item);
0538: @*/
0539:
0540: /*@
0541: @ public normal_behavior
0542: @ requires item != null;
0543: @ ensures \result
0544: @ == (\num_of int i; 0 <= i && i < int_length();
0545: @ itemAt(i) != null
0546: @ && itemAt(i) == item);
0547: @ also
0548: @ public normal_behavior
0549: @ requires item == null;
0550: @ ensures \result == (\num_of int i; 0 <= i && i < int_length();
0551: @ itemAt(i) == null);
0552: @*/
0553: public int count(Object item) {
0554: JMLListObjectNode ptr = this .theSeq;
0555: int cnt = 0;
0556: while (ptr != null) {
0557: if (ptr.headEquals(item)) {
0558: cnt++;
0559: }
0560: ptr = ptr.next;
0561: }
0562: return cnt;
0563: }
0564:
0565: /*@ also
0566: @ public normal_behavior
0567: @ {|
0568: @ requires elem != null;
0569: @ ensures \result <==>
0570: @ (\exists int i; 0 <= i && i < int_length();
0571: @ itemAt(i) == elem);
0572: @ also
0573: @ requires elem == null;
0574: @ ensures \result <==>
0575: @ (\exists int i; 0 <= i && i < int_length();
0576: @ itemAt(i) == null);
0577: @ |}
0578: @*/
0579: public boolean has(Object elem) {
0580: return theSeq != null && theSeq.has(elem);
0581: }
0582:
0583: /*@ public normal_behavior
0584: @ requires c != null;
0585: @ ensures \result <==> (\forall Object o; c.contains(o); this.has(o));
0586: @*/
0587: public boolean containsAll(/*@ non_null @*/java.util.Collection c) {
0588: java.util.Iterator celems = c.iterator();
0589: while (celems.hasNext()) {
0590: Object o = celems.next();
0591: if (!has(o)) {
0592: return false;
0593: }
0594: }
0595: return true;
0596: }
0597:
0598: /*@ public normal_behavior
0599: @ requires s2 != null;
0600: @ ensures \result <==>
0601: @ int_length() <= s2.int_length()
0602: @ && (\forall int i; 0 <= i && i < int_length();
0603: @ (s2.itemAt(i) != null
0604: @ && s2.itemAt(i) == (itemAt(i)))
0605: @ || (s2.itemAt(i) == null && itemAt(i) == null) );
0606: @*/
0607: public boolean isPrefix(/*@ non_null @*/JMLObjectSequence s2) {
0608: return int_length() <= s2.int_length()
0609: && (theSeq == null || theSeq.isPrefixOf(s2.theSeq));
0610: }
0611:
0612: /*@ public normal_behavior
0613: @ requires s2 != null;
0614: @ ensures \result <==> this.isPrefix(s2) && !this.equals(s2);
0615: @*/
0616: public boolean isProperPrefix(/*@ non_null @*/JMLObjectSequence s2) {
0617: return int_length() != s2.int_length() && isPrefix(s2);
0618: }
0619:
0620: /*@ public normal_behavior
0621: @ requires s2 != null;
0622: @ ensures \result <==>
0623: @ int_length() <= s2.int_length()
0624: @ && this.equals(s2.removePrefix(s2.int_length() - int_length()));
0625: @*/
0626: public boolean isSuffix(/*@ non_null @*/JMLObjectSequence s2) {
0627: if (int_length() > s2.int_length()) {
0628: return false;
0629: } else if (int_length() == 0) {
0630: return true;
0631: }
0632: JMLListObjectNode suffix = s2.theSeq.removePrefix(s2
0633: .int_length()
0634: - int_length());
0635: return theSeq.equals(suffix);
0636: }
0637:
0638: /*@ public normal_behavior
0639: @ requires s2 != null;
0640: @ ensures \result <==> this.isSuffix(s2) && !this.equals(s2);
0641: @*/
0642: public boolean isProperSuffix(/*@ non_null @*/JMLObjectSequence s2) {
0643: return int_length() != s2.int_length() && isSuffix(s2);
0644: }
0645:
0646: /** Test whether this object's value is equal to the given argument.
0647: * @see #isSuffix
0648: * @see #int_size()
0649: */
0650: /*@ also
0651: @ public normal_behavior
0652: @ requires obj != null && obj instanceof JMLObjectSequence;
0653: @ ensures \result <==>
0654: @ isPrefix((JMLObjectSequence)obj)
0655: @ && ((JMLObjectSequence)obj).isPrefix(this);
0656: @ ensures_redundantly \result ==>
0657: @ containsNull == ((JMLObjectSequence)obj).containsNull;
0658: @ also
0659: @ public normal_behavior
0660: @ requires obj == null || !(obj instanceof JMLObjectSequence);
0661: @ ensures !\result;
0662: @*/
0663: public/*@ pure @*/boolean equals(Object obj) {
0664: return (obj != null && obj instanceof JMLObjectSequence)
0665: && (int_length() == ((JMLObjectSequence) obj)
0666: .int_length())
0667: && isPrefix((JMLObjectSequence) obj);
0668: }
0669:
0670: /** Return a hash code for this object.
0671: */
0672: public int hashCode() {
0673: return (theSeq == null ? 0 : theSeq.hashCode());
0674: }
0675:
0676: /** Tells whether this sequence is empty.
0677: * @see #int_size()
0678: * @see #int_length()
0679: */
0680: /*@ public normal_behavior
0681: @ ensures \result == (int_length() == 0);
0682: @*/
0683: public/*@ pure @*/boolean isEmpty() {
0684: return theSeq == null;
0685: }
0686:
0687: /*@ public normal_behavior
0688: @ requires has(item);
0689: @ {|
0690: @ requires item != null;
0691: @ ensures itemAt(\result) == item
0692: @ && (\forall \bigint i; 0 <= i && i < \result;
0693: @ !(itemAt(i) == item));
0694: @ ensures_redundantly (* \result is the first index
0695: @ at which item occurs in this *);
0696: @ also
0697: @ requires item == null;
0698: @ ensures itemAt(\result) == null
0699: @ && (\forall \bigint i; 0 <= i && i < \result;
0700: @ itemAt(i) != null);
0701: @ |}
0702: @ also
0703: @ public exceptional_behavior
0704: @ requires !has(item);
0705: @ signals (JMLSequenceException);
0706: model public \bigint bi_indexOf(Object item) throws JMLSequenceException ;
0707: @*/
0708:
0709: /*@ public normal_behavior
0710: @ requires has(item);
0711: @ {|
0712: @ requires item != null;
0713: @ ensures itemAt(\result) == item
0714: @ && (\forall int i; 0 <= i && i < \result;
0715: @ !(itemAt(i) == item));
0716: @ ensures_redundantly (* \result is the first index
0717: @ at which item occurs in this *);
0718: @ also
0719: @ requires item == null;
0720: @ ensures itemAt(\result) == null
0721: @ && (\forall int i; 0 <= i && i < \result;
0722: @ itemAt(i) != null);
0723: @ |}
0724: @ also
0725: @ public exceptional_behavior
0726: @ requires !has(item);
0727: @ signals (JMLSequenceException);
0728: @*/
0729: public int indexOf(Object item) throws JMLSequenceException {
0730: if (theSeq == null) {
0731: throw new JMLSequenceException(ITEM_PREFIX + item
0732: + IS_NOT_FOUND);
0733: }
0734: int idx = theSeq.indexOf(item);
0735: if (idx == -1) {
0736: throw new JMLSequenceException(ITEM_PREFIX + item
0737: + IS_NOT_FOUND);
0738: } else {
0739: return idx;
0740: }
0741: }
0742:
0743: private static final String ITEM_PREFIX = "item ";
0744: private static final String IS_NOT_FOUND = " is not in this sequence.";
0745:
0746: /*@
0747: @ public normal_behavior
0748: @ requires int_length() > 0;
0749: @ {|
0750: @ requires itemAt(0) != null;
0751: @ ensures \result == (itemAt(0));
0752: @ also
0753: @ requires itemAt(0) == null;
0754: @ ensures \result == null;
0755: @ |}
0756: @ also
0757: @ public exceptional_behavior
0758: @ requires int_length() == 0;
0759: @ signals (JMLSequenceException);
0760: @*/
0761: public/*@ pure @*/Object first() throws JMLSequenceException {
0762: if (theSeq == null) {
0763: throw new JMLSequenceException(
0764: "Tried first() on empty sequence.");
0765: } else {
0766: return (theSeq.head()); // head() clones if necessary
0767: }
0768: }
0769:
0770: /*@
0771: @ public normal_behavior
0772: @ requires int_length() >= 1;
0773: @ {|
0774: @ requires itemAt((int)(int_length()-1)) != null;
0775: @ ensures \result == (itemAt((int)(int_length()-1)));
0776: @ also
0777: @ requires itemAt((int)(int_length()-1)) == null;
0778: @ ensures \result == null;
0779: @ |}
0780: @ also
0781: @ public exceptional_behavior
0782: @ requires int_length() == 0;
0783: @ signals (JMLSequenceException);
0784: @*/
0785: public Object last() throws JMLSequenceException {
0786: if (theSeq == null) {
0787: throw new JMLSequenceException(
0788: "Tried last() on empty sequence.");
0789: } else {
0790: return theSeq.last(); // last() clones if necessary
0791: }
0792: }
0793:
0794: /*@ public normal_behavior
0795: @ requires s2 != null;
0796: @ ensures \result <==>
0797: @ int_length() <= s2.int_length()
0798: @ && (\exists int i; 0 <= i && i < s2.int_length()-int_length()+1;
0799: @ isPrefix(s2.removePrefix(i)));
0800: @*/
0801: public boolean isSubsequence(/*@ non_null @*/JMLObjectSequence s2) {
0802: JMLListObjectNode walker = s2.theSeq;
0803: for (int walkerLen = s2.int_length(); int_length() <= walkerLen; walkerLen--) {
0804: if (theSeq == null || theSeq.isPrefixOf(walker)) {
0805: return true;
0806: }
0807: walker = walker.next;
0808: }
0809: return false;
0810: }
0811:
0812: /*@ public normal_behavior
0813: @ requires s2 != null;
0814: @ ensures \result <==>
0815: @ this.isSubsequence(s2) && !this.equals(s2);
0816: @*/
0817: public boolean isProperSubsequence(
0818: /*@ non_null @*/JMLObjectSequence s2) {
0819: return int_length() < s2.int_length() && isSubsequence(s2);
0820: }
0821:
0822: /*@ public normal_behavior
0823: @ requires s2 != null;
0824: @ ensures \result <==> s2.isSubsequence(this);
0825: @*/
0826: public boolean isSupersequence(/*@ non_null @*/JMLObjectSequence s2) {
0827: return s2.isSubsequence(this );
0828: }
0829:
0830: /*@ public normal_behavior
0831: @ requires s2 != null;
0832: @ ensures \result <==> s2.isProperSubsequence(this);
0833: @*/
0834: public boolean isProperSupersequence(
0835: /*@ non_null @*/JMLObjectSequence s2) {
0836: return s2.isProperSubsequence(this );
0837: }
0838:
0839: /*@ public normal_behavior
0840: @ requires s2 != null;
0841: @ ensures \result <==>
0842: @ (\exists int i; 0 <= i && i < int_length();
0843: @ itemAt(i) == elem
0844: @ && subsequence(0,i)
0845: @ .concat(subsequence((int)(i+1),int_length()))
0846: @ .equals(s2));
0847: @ ensures_redundantly \result ==> this.int_length() == s2.int_length()+1;
0848: @ ensures_redundantly \result ==> has(elem);
0849: @ ensures_redundantly \result <==> s2.isDeletionFrom(this, elem);
0850: @*/
0851: public boolean isInsertionInto(
0852: /*@ non_null @*/JMLObjectSequence s2, Object elem) {
0853: if (int_length() != s2.int_length() + 1) {
0854: return false;
0855: }
0856: JMLListObjectNode walker = theSeq;
0857: JMLListObjectNode s2walker = s2.theSeq;
0858: int lenRemaining;
0859: /*@ maintaining subsequence(0, (int)(int_length()-lenRemaining))
0860: @ .equals(s2.subsequence(0, (int)(int_length()-lenRemaining)));
0861: @ decreasing int_length();
0862: @*/
0863: for (lenRemaining = int_length(); lenRemaining > 0; lenRemaining--) {
0864: if (walker.headEquals(elem)) {
0865: if ((walker.next == null && s2walker == null)
0866: || (walker.next != null && walker.next
0867: .equals(s2walker))) {
0868: return true;
0869: }
0870: }
0871: if (s2walker == null || !s2walker.headEquals(walker.head())) {
0872: return false;
0873: }
0874: walker = walker.next;
0875: s2walker = s2walker.next;
0876: }
0877: return false;
0878: }
0879:
0880: /*@ public normal_behavior
0881: @ requires s2 != null;
0882: @ ensures \result <==>
0883: @ (\exists int i; 0 <= i && i < s2.int_length();
0884: @ s2.itemAt(i) == elem
0885: @ && this.equals(s2.removeItemAt(i)));
0886: @ ensures_redundantly \result ==> this.int_length()+1 == s2.int_length();
0887: @ ensures_redundantly \result ==> s2.has(elem);
0888: @ ensures_redundantly \result <==> s2.isInsertionInto(this, elem);
0889: @*/
0890: public boolean isDeletionFrom(
0891: /*@ non_null @*/JMLObjectSequence s2, Object elem) {
0892: return s2.isInsertionInto(this , elem);
0893: }
0894:
0895: // *************** building new JMLObjectSequences **********************
0896:
0897: /** Return a clone of this object. This method does not clone the
0898: * elements of the sequence.
0899: */
0900: /*@ also
0901: @ public normal_behavior
0902: @ ensures \result != null
0903: @ && \result instanceof JMLObjectSequence
0904: @ && ((JMLObjectSequence)\result).equals(this);
0905: @*/
0906: public Object clone() {
0907: return this ;
0908: }
0909:
0910: /** Return a sequence containing the first n elements in this sequence.
0911: * @param n the number of elements in the result.
0912: * @exception JMLSequenceException if n is negative or greater than
0913: * the length of the sequence.
0914: * @see #trailer
0915: * @see #removePrefix
0916: * @see #subsequence
0917: */
0918: /*@ public normal_behavior
0919: @ requires 0 <= n && n <= length;
0920: @ ensures \result.length == n
0921: @ && (\forall \bigint i; 0 <= i && i < n;
0922: @ (\result.itemAt(i) != null
0923: @ ==> \result.itemAt(i) == (itemAt(i)))
0924: @ || (\result.itemAt(i) == null
0925: @ ==> itemAt(i) == null) );
0926: @ also
0927: @ public exceptional_behavior
0928: @ requires !(0 <= n && n <= length);
0929: @ signals (JMLSequenceException);
0930: @
0931: @ implies_that
0932: @ ensures !containsNull ==> !\result.containsNull;
0933: @
0934: model public JMLObjectSequence prefix(\bigint n) throws JMLSequenceException;
0935: @*/
0936:
0937: /*@ public normal_behavior
0938: @ requires 0 <= n && n <= length;
0939: @ ensures \result.length == n
0940: @ && (\forall int i; 0 <= i && i < n;
0941: @ (\result.itemAt(i) != null
0942: @ ==> \result.itemAt(i) == (itemAt(i)))
0943: @ || (\result.itemAt(i) == null
0944: @ ==> itemAt(i) == null) );
0945: @ also
0946: @ public exceptional_behavior
0947: @ requires !(0 <= n && n <= length);
0948: @ signals (JMLSequenceException);
0949: @
0950: @*/
0951: public/*@ non_null @*/JMLObjectSequence prefix(int n)
0952: throws JMLSequenceException {
0953: if (n < 0 || n > int_length()) {
0954: throw new JMLSequenceException(
0955: "Invalid parameter to prefix() with n = " + n
0956: + "\n" + " when sequence length = "
0957: + int_length());
0958: } else {
0959: if (n == 0) {
0960: return new JMLObjectSequence();
0961: } else {
0962: JMLListObjectNode pfx_list = theSeq.prefix(n);
0963: return new JMLObjectSequence(pfx_list, n);
0964: }
0965: }
0966: }
0967:
0968: /*@ public normal_behavior
0969: @ requires 0 <= n && n <= length;
0970: @ ensures \result.length == length - n
0971: @ && (\forall \bigint i; n <= i && i < length;
0972: @ (\result.itemAt(i-n) != null
0973: @ && \result.itemAt(i-n) == (itemAt(i)))
0974: @ || (\result.itemAt(i-n) == null
0975: @ && itemAt(i) == null) );
0976: @ also
0977: @ public exceptional_behavior
0978: @ requires !(0 <= n && n <= length);
0979: @ signals (JMLSequenceException);
0980: model public JMLObjectSequence removePrefix(\bigint n) throws JMLSequenceException ;
0981: @*/
0982:
0983: /*@ public normal_behavior
0984: @ requires 0 <= n && n <= length;
0985: @ ensures \result.length == length - n
0986: @ && (\forall \bigint i; n <= i && i < length;
0987: @ (\result.itemAt((int)(i-n)) != null
0988: @ && \result.itemAt((int)(i-n)) == (itemAt(i)))
0989: @ || (\result.itemAt((int)(i-n)) == null
0990: @ && itemAt(i) == null) );
0991: @ also
0992: @ public exceptional_behavior
0993: @ requires !(0 <= n && n <= length);
0994: @ signals (JMLSequenceException);
0995: @*/
0996: public/*@ non_null @*/JMLObjectSequence removePrefix(int n)
0997: throws JMLSequenceException {
0998: if (n < 0 || n > int_length()) {
0999: throw new JMLSequenceException(
1000: "Invalid parameter to removePrefix() "
1001: + "with n = " + n + "\n"
1002: + " when sequence length = "
1003: + int_length());
1004: } else {
1005: if (n == 0) {
1006: return this ;
1007: } else {
1008: JMLListObjectNode pfx_list = theSeq.removePrefix(n);
1009: return new JMLObjectSequence(pfx_list, int_length() - n);
1010: }
1011: }
1012: }
1013:
1014: /*@ public normal_behavior
1015: @ requires s2 != null;
1016: @ ensures \result.int_length() == int_length() + s2.int_length()
1017: @ && (\forall int i; 0 <= i && i < int_length();
1018: @ (\result.itemAt(i) != null
1019: @ && \result.itemAt(i) == (itemAt(i)))
1020: @ || (\result.itemAt(i) == null
1021: @ && itemAt(i) == null) )
1022: @ && (\forall int i; 0 <= i && i < s2.int_length();
1023: @ (\result.itemAt((int)(int_length()+i)) != null
1024: @ && \result.itemAt((int)(int_length()+i)) == (s2.itemAt(i)))
1025: @ || (\result.itemAt((int)(int_length()+i)) == null
1026: @ && s2.itemAt(i) == null) );
1027: @*/
1028: public/*@ non_null @*/
1029: JMLObjectSequence concat(/*@ non_null @*/JMLObjectSequence s2) {
1030: if (theSeq == null) {
1031: return s2;
1032: } else if (s2.theSeq == null) {
1033: return this ;
1034: } else {
1035: JMLListObjectNode new_list = theSeq.concat(s2.theSeq);
1036: return new JMLObjectSequence(new_list, int_length()
1037: + s2.int_length());
1038: }
1039: }
1040:
1041: /*@ public normal_behavior
1042: @ old int len = int_length();
1043: @ ensures \result.int_length() == len
1044: @ && (\forall int i; 0 <= i && i < len;
1045: @ (\result.itemAt((int)(len-i-1)) != null
1046: @ && \result.itemAt((int)(len-i-1)) == (itemAt(i)))
1047: @ || (\result.itemAt((int)(len-i-1)) == null
1048: @ && itemAt(i) == null) );
1049: @*/
1050: public/*@ non_null @*/JMLObjectSequence reverse() {
1051: if (theSeq == null) {
1052: return this ;
1053: } else {
1054: JMLListObjectNode r = theSeq.reverse();
1055: return new JMLObjectSequence(r, int_length());
1056: }
1057: }
1058:
1059: /*@ public normal_behavior
1060: @ requires 0 <= index && index < length();
1061: @ ensures \result.equals(prefix(index).concat(removePrefix(index+1)));
1062: @ also
1063: @ public exceptional_behavior
1064: @ requires !(0 <= index && index < length());
1065: @ signals (JMLSequenceException);
1066: @
1067: model public non_null JMLObjectSequence removeItemAt(\bigint index)
1068: throws JMLSequenceException ;
1069: @*/
1070:
1071: /*@ public normal_behavior
1072: @ requires 0 <= index && index < int_length();
1073: @ ensures \result.equals(prefix(index).concat(removePrefix((int)(index+1))));
1074: @ also
1075: @ public exceptional_behavior
1076: @ requires !(0 <= index && index < int_length());
1077: @ signals (JMLSequenceException);
1078: @
1079: @*/
1080: public/*@ non_null @*/JMLObjectSequence removeItemAt(int index)
1081: throws JMLSequenceException {
1082: if (0 <= index && index < int_length()) {
1083: JMLListObjectNode new_list = theSeq.removeItemAt(index);
1084: return new JMLObjectSequence(new_list, int_length() - 1);
1085: } else {
1086: throw new JMLSequenceException(
1087: "Invalid parameter to removeItemAt() "
1088: + "with index = " + index + "\n"
1089: + " when sequence length = "
1090: + int_length());
1091: }
1092: }
1093:
1094: /*@ public normal_behavior
1095: @ requires 0 <= index && index < length();
1096: @ ensures \result.equals(removeItemAt(index).insertBeforeIndex(index,
1097: @ item));
1098: @ also
1099: @ public exceptional_behavior
1100: @ requires !(0 <= index && index < length());
1101: @ signals (JMLSequenceException);
1102: model public non_null JMLObjectSequence replaceItemAt(\bigint index, Object item) throws JMLSequenceException;
1103: @*/
1104:
1105: /*@ public normal_behavior
1106: @ requires 0 <= index && index < int_length();
1107: @ ensures \result.equals(removeItemAt(index).insertBeforeIndex(index,
1108: @ item));
1109: @ ensures_redundantly
1110: @ (* \result is the same as this,
1111: @ but with item replacing the one at position index *);
1112: @ also
1113: @ public exceptional_behavior
1114: @ requires !(0 <= index && index < int_length());
1115: @ signals (JMLSequenceException);
1116: @*/
1117: public/*@ non_null @*/JMLObjectSequence replaceItemAt(int index,
1118: Object item) throws JMLSequenceException {
1119: if (0 <= index && index < int_length()) {
1120: JMLListObjectNode new_list = theSeq.replaceItemAt(index,
1121: item);
1122: return new JMLObjectSequence(new_list, int_length());
1123: } else {
1124: throw new JMLSequenceException(
1125: "Invalid parameter to replaceItemAt() "
1126: + "with index = " + index + "\n"
1127: + " when sequence length = "
1128: + int_length());
1129: }
1130: }
1131:
1132: /*@ public normal_behavior
1133: @ requires int_length() >= 1;
1134: @ ensures \result.equals(removeItemAt((int)(int_length()-1)));
1135: @ ensures_redundantly \result.int_length() == int_length() - 1
1136: @ && (* \result is like this, but without the last item *);
1137: @ also
1138: @ public exceptional_behavior
1139: @ requires int_length() == 0;
1140: @ signals (JMLSequenceException);
1141: @
1142: @*/
1143: public/*@ non_null @*/JMLObjectSequence header()
1144: throws JMLSequenceException {
1145: if (theSeq == null) {
1146: throw new JMLSequenceException(
1147: "Tried header() on empty sequence.");
1148: } else {
1149: JMLListObjectNode new_list = theSeq.removeLast();
1150: return new JMLObjectSequence(new_list, int_length() - 1);
1151: }
1152: }
1153:
1154: /*@ public normal_behavior
1155: @ requires int_length() >= 1;
1156: @ ensures \result.equals(removePrefix(1));
1157: @ ensures_redundantly \result.int_length() == int_length() - 1
1158: @ && (* \result is like this, but without the first item *);
1159: @ also
1160: @ public exceptional_behavior
1161: @ requires int_length() == 0;
1162: @ signals (JMLSequenceException);
1163: @
1164: @*/
1165: public/*@ pure @*//*@ non_null @*/JMLObjectSequence trailer()
1166: throws JMLSequenceException {
1167: if (theSeq == null) {
1168: throw new JMLSequenceException(
1169: "Tried trailer() on empty sequence.");
1170: } else {
1171: JMLListObjectNode new_list = theSeq.next;
1172: return new JMLObjectSequence(new_list, int_length() - 1);
1173: }
1174: }
1175:
1176: /*@ //FIXME, _ alsoIfValue _
1177: @ public normal_behavior
1178: @ requires -1 <= afterThisOne && afterThisOne < length;
1179: @ requires length < Integer.MAX_VALUE;
1180: @ ensures \result.equals(insertBeforeIndex((int)(afterThisOne + 1), item));
1181: @ ensures_redundantly
1182: @ (* \result is the same sequence as this,
1183: @ but with item inserted after the index "afterThisOne" *);
1184: @ also
1185: @ public exceptional_behavior
1186: @ requires !(-1 <= afterThisOne && afterThisOne < length);
1187: @ signals (JMLSequenceException);
1188: model public JMLObjectSequence insertAfterIndex(\bigint afterThisOne, Object item) throws JMLSequenceException, IllegalStateException;
1189: @*/
1190:
1191: /*@
1192: @ public normal_behavior
1193: @ requires -1 <= afterThisOne && afterThisOne < length;
1194: @ requires length < Integer.MAX_VALUE;
1195: @ ensures \result.equals(insertBeforeIndex((int)(afterThisOne + 1), item));
1196: @ also
1197: @ public exceptional_behavior
1198: @ requires !(-1 <= afterThisOne && afterThisOne < length);
1199: @ signals (JMLSequenceException);
1200: @*/
1201: public/*@ non_null @*/JMLObjectSequence insertAfterIndex(
1202: int afterThisOne, Object item) throws JMLSequenceException,
1203: IllegalStateException {
1204: if (afterThisOne < -1 || afterThisOne >= int_length()) {
1205: throw new JMLSequenceException("Invalid parameter to "
1206: + "insertAfterIndex() " + "with afterThisOne = "
1207: + afterThisOne + "\n"
1208: + " when sequence length = " + int_length());
1209: } else if (int_length() < Integer.MAX_VALUE) {
1210: return insertBeforeIndex(afterThisOne + 1, item);
1211: } else {
1212: throw new IllegalStateException(TOO_BIG_TO_INSERT);
1213: }
1214: }
1215:
1216: private static final String TOO_BIG_TO_INSERT = "Cannot insert into a sequence with Integer.MAX_VALUE elements.";
1217:
1218: /*@
1219: @ public normal_behavior
1220: @ requires 0 <= beforeThisOne && beforeThisOne <= length;
1221: @ requires length < Integer.MAX_VALUE;
1222: @ ensures \result.equals(
1223: @ prefix(beforeThisOne).
1224: @ concat(new JMLObjectSequence(item)).
1225: @ concat(removePrefix(beforeThisOne))
1226: @ );
1227: @ also
1228: @ public exceptional_behavior
1229: @ requires !(0 <= beforeThisOne && beforeThisOne <= length);
1230: @ signals (JMLSequenceException);
1231: model public
1232: JMLObjectSequence insertBeforeIndex(\bigint beforeThisOne, Object item)
1233: throws JMLSequenceException, IllegalStateException;
1234: @*/
1235:
1236: /*@
1237: @ public normal_behavior
1238: @ requires 0 <= beforeThisOne && beforeThisOne <= length;
1239: @ requires length < Integer.MAX_VALUE;
1240: @ ensures \result.equals(
1241: @ prefix(beforeThisOne).
1242: @ concat(new JMLObjectSequence(item)).
1243: @ concat(removePrefix(beforeThisOne))
1244: @ );
1245: @ also
1246: @ public exceptional_behavior
1247: @ requires !(0 <= beforeThisOne && beforeThisOne <= length);
1248: @ signals (JMLSequenceException);
1249: @*/
1250: public/*@ non_null @*/
1251: JMLObjectSequence insertBeforeIndex(int beforeThisOne, Object item)
1252: throws JMLSequenceException, IllegalStateException {
1253: if (beforeThisOne < 0 || beforeThisOne > int_length()) {
1254: throw new JMLSequenceException(
1255: "Invalid parameter to insertBeforeIndex()"
1256: + " with beforeThisOne = " + beforeThisOne
1257: + "\n" + " when sequence length = "
1258: + int_length());
1259: } else if (int_length() < Integer.MAX_VALUE) {
1260: if (theSeq == null) {
1261: return new JMLObjectSequence(item);
1262: } else {
1263: // insertBefore() clones item, if necessary
1264: JMLListObjectNode new_list = theSeq.insertBefore(
1265: beforeThisOne, item);
1266: return new JMLObjectSequence(new_list, int_length() + 1);
1267: }
1268: } else {
1269: throw new IllegalStateException(TOO_BIG_TO_INSERT);
1270: }
1271: }
1272:
1273: /*@
1274: @ public normal_behavior
1275: @ requires int_length() < Integer.MAX_VALUE;
1276: @ ensures \result.equals(insertBeforeIndex(int_length(), item));
1277: @ ensures_redundantly
1278: @ \result.int_length() == int_length() + 1
1279: @ && isProperPrefix(\result);
1280: @*/
1281: public/*@ non_null @*/JMLObjectSequence insertBack(Object item)
1282: throws IllegalStateException {
1283: if (theSeq == null) {
1284: return new JMLObjectSequence(item);
1285: } else if (int_length() < Integer.MAX_VALUE) {
1286: return new JMLObjectSequence(theSeq.append(item),
1287: int_length() + 1);
1288: } else {
1289: throw new IllegalStateException(TOO_BIG_TO_INSERT);
1290: }
1291: }
1292:
1293: /*@
1294: @ public normal_behavior
1295: @ requires int_length() < Integer.MAX_VALUE;
1296: @ ensures \result.equals(insertBeforeIndex(0, item));
1297: @ ensures_redundantly
1298: @ \result.int_length() == int_length() + 1
1299: @ && \result.trailer().equals(this);
1300: @ for_example
1301: @ public normal_example
1302: @ requires (* this is <a,b,c> and item is d *);
1303: @ ensures (* \result is <d,a,b,c> *);
1304: @*/
1305: public/*@ pure @*//*@ non_null @*/JMLObjectSequence insertFront(
1306: Object item) throws IllegalStateException {
1307: if (theSeq == null) {
1308: return new JMLObjectSequence(item);
1309: } else if (int_length() < Integer.MAX_VALUE) {
1310: return new JMLObjectSequence(
1311: // cons() clones item, if necessary
1312: JMLListObjectNode.cons(item, theSeq),
1313: int_length() + 1);
1314: } else {
1315: throw new IllegalStateException(TOO_BIG_TO_INSERT);
1316: }
1317: }
1318:
1319: /*@ public normal_behavior
1320: @ requires 0 <= from && from <= to && to <= length();
1321: @ ensures \result.equals(removePrefix(from).prefix((int)(to - from)));
1322: @ ensures_redundantly
1323: @ (* \result contains the elements of this beginning with
1324: @ index from (inclusive) and ending
1325: @ with index to (exclusive) *)
1326: @ && \result.length() == to - from;
1327: @ also
1328: @ public exceptional_behavior
1329: @ requires !(0 <= from && from <= to && to <= length());
1330: @ signals (JMLSequenceException);
1331: @
1332: model public non_null JMLObjectSequence subsequence(\bigint from, \bigint to) throws JMLSequenceException ;
1333: @*/
1334:
1335: /*@ public normal_behavior
1336: @ requires 0 <= from && from <= to && to <= int_length();
1337: @ ensures \result.equals(removePrefix(from).prefix((int)(to - from)));
1338: @ ensures_redundantly
1339: @ (* \result contains the elements of this beginning with
1340: @ index from (inclusive) and ending
1341: @ with index to (exclusive) *)
1342: @ && \result.int_length() == to - from;
1343: @ also
1344: @ public exceptional_behavior
1345: @ requires !(0 <= from && from <= to && to <= int_length());
1346: @ signals (JMLSequenceException);
1347: @
1348: @*/
1349: public/*@ non_null @*/JMLObjectSequence subsequence(int from,
1350: int to) throws JMLSequenceException {
1351: if (from < 0 || from > to || to > int_length()) {
1352: throw new JMLSequenceException("Invalid parameters to "
1353: + "subsequence() with from = " + from
1354: + " and to = " + to + "\n" + " "
1355: + "when sequence length = " + int_length());
1356: } else {
1357: if (theSeq == null) {
1358: return this ;
1359: } else {
1360: JMLListObjectNode removedPrefix = theSeq
1361: .removePrefix(from);
1362: if (removedPrefix == null) {
1363: return new JMLObjectSequence();
1364: } else {
1365: JMLListObjectNode new_list = removedPrefix
1366: .prefix(to - from);
1367: return new JMLObjectSequence(new_list, to - from);
1368: }
1369: }
1370: }
1371: }
1372:
1373: /*@ public normal_behavior
1374: @ ensures \result != null
1375: @ && (\forall int i; 0 <= i && i < int_length();
1376: @ \result.count(this.itemAt(i))
1377: @ == this.count(this.itemAt(i)));
1378: @*/
1379: public /*@ non_null @*/ JMLObjectBag toBag() {
1380: JMLObjectBag ret = new JMLObjectBag();
1381: JMLObjectSequenceEnumerator enum = elements();
1382: while (enum.hasMoreElements()) {
1383: Object o = enum.nextElement();
1384: Object e = (o == null ? null : o);
1385: ret = ret.insert(e);
1386: }
1387: return ret;
1388: }
1389: /*@ public normal_behavior
1390: @ ensures \result != null
1391: @ && (\forall Object o;; \result.has(o) == this.has(o));
1392: @*/
1393: public /*@ non_null @*/ JMLObjectSet toSet() {
1394: JMLObjectSet ret = new JMLObjectSet();
1395: JMLObjectSequenceEnumerator enum = elements();
1396: while (enum.hasMoreElements()) {
1397: Object o = enum.nextElement();
1398: Object e = (o == null ? null : o);
1399: ret = ret.insert(e);
1400: }
1401: return ret;
1402: }
1403: /*@ public normal_behavior
1404: @ ensures \result != null && \result.length == int_length()
1405: @ && (\forall int i; 0 <= i && i < int_length();
1406: @ (\result[i] == null ==> this.itemAt(i) == null)
1407: @ && (\result[i] != null ==>
1408: @ \result[i] == (this.itemAt(i))));
1409: @*/
1410: public /*@ non_null @*/ Object[] toArray() {
1411: Object[] ret = new Object[int_length()];
1412: JMLObjectSequenceEnumerator enum = elements();
1413: int i = 0;
1414: //@ loop_invariant 0 <= i && i <= ret.length;
1415: while (enum.hasMoreElements()) {
1416: Object o = enum.nextElement();
1417: if (o == null) {
1418: ret[i] = null;
1419: } else {
1420: Object e = o;
1421: ret[i] = e ;
1422: }
1423: i++;
1424: }
1425: return ret;
1426: }
1427:
1428: /*@ public normal_behavior
1429: @ ensures \fresh(\result);
1430: @*/
1431: public/*@ non_null @*/JMLObjectSequenceEnumerator elements() {
1432: JMLObjectSequenceEnumerator retValue = new JMLObjectSequenceEnumerator(
1433: this );
1434: return retValue;
1435: }
1436:
1437: /*@ also
1438: @ public normal_behavior
1439: @ ensures \fresh(\result)
1440: @ && \result.equals(new JMLEnumerationToIterator(elements()));
1441: @*/
1442: public JMLIterator iterator() {
1443: return new JMLEnumerationToIterator(elements());
1444: }
1445:
1446: public String toString() {
1447: String newStr = "(<";
1448: JMLListObjectNode seqWalker = theSeq;
1449: boolean first = true;
1450: while (seqWalker != null) {
1451: if (!first) {
1452: newStr = newStr + ", ";
1453: }
1454: newStr = newStr + seqWalker.val;
1455: first = false;
1456: seqWalker = seqWalker.next;
1457: }
1458: return (newStr + ">)");
1459: }
1460:
1461: }
|