0001: // @(#)$Id: JMLEqualsSequence.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: public/*@ pure @*/class JMLEqualsSequence implements JMLCollection {
0026:
0027: //*********************** equational theory ***********************
0028:
0029: /*@ public invariant (\forall JMLEqualsSequence s2;
0030: @ (\forall Object e1, e2;
0031: @ (\forall \bigint n;
0032: @ equational_theory(this, s2, e1, e2, n) )));
0033: @*/
0034:
0035: /** An equational specification of the properties of sequences.
0036: */
0037: /*@ public normal_behavior
0038: @ {|
0039: @ // The following are defined by observations (itemAt) and induction.
0040: @
0041: @ ensures \result <==> !(new JMLEqualsSequence()).has(e1);
0042: @ also
0043: @ ensures \result <==> (new JMLEqualsSequence()).size() == 0;
0044: @ also
0045: @ ensures \result <==> (new JMLEqualsSequence(e1)).size() == 1;
0046: @ also
0047: @ ensures \result <==>
0048: @ e1 != null ==>
0049: @ (new JMLEqualsSequence(e1)).itemAt(0) .equals(e1);
0050: @ also
0051: @ ensures \result <==>
0052: @ e1 != null ==>
0053: @ s.insertFront(e1).first() .equals(e1);
0054: @ also
0055: @ ensures \result <==>
0056: @ e1 != null ==>
0057: @ s.insertBack(e1).last() .equals(e1);
0058: @ also
0059: @ ensures \result <==>
0060: @ e1 != null ==>
0061: @ s.insertFront(e1).itemAt(0) .equals(e1);
0062: @ also
0063: @ ensures \result <==>
0064: @ s.insertFront(e1).size() == s.size() + 1;
0065: @ also
0066: @ ensures \result <==>
0067: @ e1 != null ==>
0068: @ s.insertBack(e1).itemAt(s.size()) .equals(e1);
0069: @ also
0070: @ ensures \result <==>
0071: @ s.insertBack(e1).size() == s.size() + 1;
0072: @ also
0073: @ ensures \result <==>
0074: @ // !FIXME! The following may be inconsistent: argument to itemAt might
0075: @ // be equal to size, but it is required to be less than size.
0076: @ -1 <= n && n < s.size() && e1 != null
0077: @ ==> s.insertAfterIndex(n, e1).itemAt(n+1) .equals(e1);
0078: @ also
0079: @ ensures \result <==>
0080: @ -1 <= n && n < s.size()
0081: @ ==> s.insertAfterIndex(n, e1).size() == s.size() + 1;
0082: @ also
0083: @ ensures \result <==>
0084: @ 0 <= n && n <= s.size() && e1 != null
0085: @ ==> s.insertBeforeIndex(n, e1).itemAt(n) .equals(e1);
0086: @ also
0087: @ ensures \result <==>
0088: @ 0 <= n && n <= s.size()
0089: @ ==> s.insertBeforeIndex(n, e1).size() == s.size() + 1;
0090: @ also
0091: @ ensures \result <==>
0092: @ s.isPrefix(s2)
0093: @ == (\forall int i; 0 <= i && i < s.int_length();
0094: @ (s2.itemAt(i) != null
0095: @ && s2.itemAt(i) .equals(s.itemAt(i)))
0096: @ || (s2.itemAt(i) == null && s.itemAt(i) == null) );
0097: @ also
0098: @ ensures \result <==>
0099: @ s.isSubsequence(s2)
0100: @ == s.int_length() <= s2.int_length()
0101: @ && (s.isPrefix(s2) || s.isSubsequence(s2.trailer()) );
0102: @
0103: @ // The following are all defined as abbreviations.
0104: @
0105: @ also
0106: @ ensures \result <==>
0107: @ s.isEmpty() == (s.size() == 0);
0108: @ also
0109: @ ensures \result <==>
0110: @ s.isEmpty() == (s.length == 0);
0111: @ also
0112: @ ensures \result <==>
0113: @ (new JMLEqualsSequence(e1)).equals(
0114: @ new JMLEqualsSequence().insertFront(e1));
0115: @ also
0116: @ ensures \result <==>
0117: @ (new JMLEqualsSequence(e1)).equals(
0118: @ new JMLEqualsSequence().insertBack(e1));
0119: @ also
0120: @ ensures \result <==>
0121: @ (new JMLEqualsSequence(e1)).equals(
0122: @ new JMLEqualsSequence().insertAfterIndex(-1, e1));
0123: @ also
0124: @ ensures \result <==>
0125: @ (new JMLEqualsSequence(e1)).equals(
0126: @ new JMLEqualsSequence().insertBeforeIndex(0, e1));
0127: @ also
0128: @ ensures \result <==>
0129: @ (s.size() >= 1 ==> s.equals(s.trailer().insertFront(s.first())));
0130: @ also
0131: @ ensures \result <==>
0132: @ (s.size() >= 1 ==> s.equals(s.header().insertBack(s.last())));
0133: @ also
0134: @ ensures \result <==>
0135: @ s.isProperSubsequence(s2)
0136: @ == ( s.isSubsequence(s2) && !s.equals(s2));
0137: @ also
0138: @ ensures \result <==>
0139: @ s.isSupersequence(s2) == s2.isSubsequence(s);
0140: @ also
0141: @ ensures \result <==>
0142: @ s.isProperSupersequence(s2) == s2.isProperSubsequence(s);
0143: @ |}
0144: public pure model boolean equational_theory(JMLEqualsSequence s,
0145: JMLEqualsSequence s2,
0146: Object e1,
0147: Object e2, \bigint n);
0148: @*/
0149:
0150: //exchange a value of a \bigint to BigInteger
0151: /*@
0152: @ public normal_behavior
0153: @ ensures true;
0154: @ public static model pure BigInteger bigintToBigInteger(\bigint biValue);
0155: @*/
0156:
0157: //exchange a value of a BigInteger to \bigint
0158: /*@ public normal_behavior
0159: requires oBi.equals(BigInteger.ZERO);
0160: ensures \result == (\bigint)0;
0161: @ public static model pure \bigint bigIntegerToBigint(BigInteger oBi);
0162: @*/
0163:
0164: //@ public invariant elementType <: \type(Object);
0165: /*@ public invariant
0166: @ (\forall Object o; o != null && has(o);
0167: @ \typeof(o) <: elementType);
0168: @*/
0169:
0170: //@ public invariant_redundantly isEmpty() ==> !containsNull;
0171: /** The list representing this sequence's elements, in order.
0172: */
0173: protected final JMLListEqualsNode theSeq;
0174: //@ in objectState;
0175: //@ invariant theSeq != null ==> theSeq.owner == this;
0176:
0177: /** This sequence's length.
0178: */
0179: protected final BigInteger _length;
0180:
0181: // in objectState;
0182: //@ public model \bigint length;
0183: //@ protected represents length <- bigIntegerToBigint(_length);
0184:
0185: //@ protected invariant theSeq == null <==> length == 0;
0186: //@ protected invariant length >= 0;
0187:
0188: /*@ protected invariant theSeq != null ==> length == theSeq.length();
0189: @ protected invariant length == length();
0190: @*/
0191:
0192: //@ public invariant owner == null;
0193: //************************* Constructors ********************************
0194: /** Initialize this to be the empty sequence.
0195: * @see #EMPTY
0196: */
0197: /*@ public normal_behavior
0198: @ assignable objectState, elementType, containsNull, owner;
0199: @ ensures isEmpty();
0200: @ ensures_redundantly size() == 0;
0201: @*/
0202: public JMLEqualsSequence() {
0203: theSeq = null;
0204: _length = BigInteger.ZERO;
0205: }
0206:
0207: /** Initialize this to be the sequence containing just the given element.
0208: * @param e the element that is the first element in this sequence.
0209: * @see #singleton
0210: */
0211: public JMLEqualsSequence(Object e)
0212: /*@ public normal_behavior
0213: @ assignable objectState, elementType, containsNull, owner;
0214: @ ensures int_length() == 1;
0215: @ ensures (e == null ==> itemAt(0) == null)
0216: @ && (e != null ==> itemAt(0) .equals(e));
0217: @*/
0218: {
0219: theSeq = JMLListEqualsNode.cons(e, null); // cons() clones e, if needed
0220: _length = BigInteger.ONE;
0221: }
0222:
0223: /** Initialize this sequence based on the given representation.
0224: */
0225: /*@ requires ls == null <==> len == 0;
0226: @ requires len >= 0;
0227: @ assignable objectState, elementType, containsNull, owner;
0228: @ ensures ls != null ==> elementType == ls.elementType;
0229: @ ensures ls != null ==> containsNull == ls.containsNull;
0230: @ ensures ls == null ==> elementType <: \type(Object);
0231: @ ensures ls == null ==> !containsNull;
0232:
0233: model protected JMLEqualsSequence (JMLListEqualsNode ls, \bigint len);
0234: @*/
0235:
0236: /** Initialize this sequence based on the given representation.
0237: */
0238: /*@ requires ls == null <==> len == 0;
0239: @ requires len >= 0;
0240: @ assignable objectState, elementType, containsNull, owner;
0241: @ ensures ls != null ==> elementType == ls.elementType;
0242: @ ensures ls != null ==> containsNull == ls.containsNull;
0243: @ ensures ls == null ==> elementType <: \type(Object);
0244: @ ensures ls == null ==> !containsNull;
0245: @*/
0246: protected JMLEqualsSequence(JMLListEqualsNode ls, int len) {
0247: theSeq = ls;
0248: _length = BigInteger.valueOf(len);
0249: }
0250:
0251: //**************************** Static methods ****************************
0252:
0253: /** The empty JMLEqualsSequence.
0254: * @see #JMLEqualsSequence()
0255: */
0256: public static final/*@ non_null @*/JMLEqualsSequence EMPTY = new JMLEqualsSequence();
0257:
0258: /** Return the singleton sequence containing the given element.
0259: * @see #JMLEqualsSequence(Object)
0260: */
0261: /*@ public normal_behavior
0262: @ assignable \nothing;
0263: @ ensures \result != null && \result.equals(new JMLEqualsSequence(e));
0264: @*/
0265: public static/*@ pure @*//*@ non_null @*/
0266: JMLEqualsSequence singleton(Object e) {
0267: return new JMLEqualsSequence(e);
0268: }
0269:
0270: /** Return the sequence containing all the elements in the given
0271: * array in the same order as the elements appear in the array.
0272: */
0273: /*@ public normal_behavior
0274: @ requires a != null;
0275: @ assignable \nothing;
0276: @ ensures \result != null && \result.size() == a.length
0277: @ && (\forall int i; 0 <= i && i < a.length;
0278: @ (\result.itemAt(i) == null
0279: @ ? a[i] == null
0280: @ : \result.itemAt(i) .equals(a[i])));
0281: @*/
0282: public static/*@ pure @*//*@ non_null @*/
0283: JMLEqualsSequence convertFrom(/*@ non_null @*/Object[] a) {
0284: /*@ non_null @*/JMLEqualsSequence ret = EMPTY;
0285: for (int i = a.length - 1; 0 <= i; i--) {
0286: ret = ret.insertFront(a[i]);
0287: }
0288: return ret;
0289: }
0290:
0291: /** Return the sequence containing the first 'size' elements in the given
0292: * array in the same order as the elements appear in the array.
0293: */
0294: /*@ public normal_behavior
0295: @ requires a != null && 0 <= size && size < a.length;
0296: @ assignable \nothing;
0297: @ ensures \result != null && \result.size() == size
0298: @ && (\forall int i; 0 <= i && i < size;
0299: @ (\result.itemAt(i) == null
0300: @ ? a[i] == null
0301: @ : \result.itemAt(i) .equals(a[i])));
0302: @
0303: @*/
0304: public static/*@ pure @*//*@ non_null @*/
0305: JMLEqualsSequence convertFrom(/*@ non_null @*/Object[] a, int size) {
0306: /*@ non_null @*/JMLEqualsSequence ret = EMPTY;
0307: for (int i = size - 1; 0 <= i; i--) {
0308: ret = ret.insertFront(a[i]);
0309: }
0310: return ret;
0311: }
0312:
0313: /** Return the sequence containing all the object in the
0314: * given collection in the same order as the elements appear in the
0315: * collection.
0316: *
0317: * @throws ClassCastException if some element in c is not an instance of
0318: * Object.
0319: * @see #containsAll(java.util.Collection)
0320: */
0321: /*@ public normal_behavior
0322: @ requires c != null
0323: @ && c.elementType <: \type(Object);
0324: @ requires c.size() < Integer.MAX_VALUE;
0325: @ assignable \nothing;
0326: @ ensures \result != null && \result.size() == c.size()
0327: @ && (\forall Object x; c.contains(x) <==> \result.has(x));
0328: @ also
0329: @ public exceptional_behavior
0330: @ requires c != null && (\exists Object o; c.contains(o);
0331: @ !(o instanceof Object));
0332: @ assignable \nothing;
0333: @ signals (ClassCastException);
0334: @*/
0335: public static/*@ pure @*//*@ non_null @*/
0336: JMLEqualsSequence convertFrom(
0337: /*@ non_null @*/java.util.Collection c)
0338: throws ClassCastException {
0339: /*@ non_null @*/JMLEqualsSequence ret = EMPTY;
0340: java.util.Iterator celems = c.iterator();
0341: while (celems.hasNext()) {
0342: Object o = celems.next();
0343: if (o == null) {
0344: ret = ret.insertBack(null);
0345: } else {
0346: ret = ret.insertBack(o);
0347: }
0348: }
0349: return ret;
0350: }
0351:
0352: /** Return the sequence containing all the object in the
0353: * given JMLCollection in the same order as the elements appear in the
0354: * collection.
0355: *
0356: * @throws ClassCastException if some element in c is not an instance of
0357: * Object.
0358: */
0359: /*@ public normal_behavior
0360: @ requires c != null
0361: @ && c.elementType <: \type(Object);
0362: @ requires c.size() < Integer.MAX_VALUE;
0363: @ assignable \nothing;
0364: @ ensures \result != null
0365: @ && (\forall Object x; c.has(x) <==> \result.has(x));
0366: @ ensures_redundantly \result.size() == c.size();
0367: @ also
0368: @ public exceptional_behavior
0369: @ requires c != null && (\exists Object o; c.has(o);
0370: @ !(o instanceof Object));
0371: @ assignable \nothing;
0372: @ signals (ClassCastException);
0373: @*/
0374: public static/*@ pure @*//*@ non_null @*/
0375: JMLEqualsSequence convertFrom(/*@ non_null @*/JMLCollection c)
0376: throws ClassCastException {
0377: /*@ non_null @*/JMLEqualsSequence ret = EMPTY;
0378: JMLIterator celems = c.iterator();
0379: while (celems.hasNext()) {
0380: Object o = celems.next();
0381: if (o == null) {
0382: ret = ret.insertBack(null);
0383: } else {
0384: ret = ret.insertBack(o);
0385: }
0386: }
0387: return ret;
0388: }
0389:
0390: //**************************** Observers **********************************
0391:
0392: /** Return the element at the given zero-based index.
0393: * @param i the zero-based index into the sequence.
0394: * @exception JMLSequenceException if the index oBiI is out of range.
0395: * @see #get(int)
0396: * @see #has(Object)
0397: * @see #count(Object)
0398: */
0399: /*@
0400: @ public normal_behavior
0401: @ requires 0 <= i && i < length;
0402: @ ensures \result != null ==> \typeof(\result) <: elementType;
0403: @ ensures !containsNull ==> \result != null;
0404: @ also
0405: @ public exceptional_behavior
0406: @ requires !(0 <= i && i < length);
0407: @ signals (JMLSequenceException);
0408: model public Object itemAt(\bigint i) throws JMLSequenceException {
0409: if (i < 0 || i >= this.length) {
0410: throw new JMLSequenceException("Index out of range.");
0411: } else {
0412: JMLListEqualsNode thisWalker = theSeq;
0413:
0414: \bigint k = 0;
0415: loop_invariant 0 <= k && k <= i && thisWalker != null;
0416: for (; k < i; k=k+1) {
0417: assume thisWalker.next != null;
0418: thisWalker = thisWalker.next;
0419: }
0420: return (thisWalker.head()); // head() clones if necessary
0421: }
0422: }
0423: @*/
0424:
0425: /** Return the element at the given zero-based index.
0426: * @param i the zero-based index into the sequence.
0427: * @exception JMLSequenceException if the index i is out of range.
0428: * @see #get(int)
0429: * @see #has(Object)
0430: * @see #count(Object)
0431: * @see #itemAt(\bigint)
0432: */
0433: /*@
0434: @ public normal_behavior
0435: @ requires 0 <= i && i < int_size();
0436: @ ensures \result != null ==> \typeof(\result) <: elementType;
0437: @ ensures !containsNull ==> \result != null;
0438: @ also
0439: @ public exceptional_behavior
0440: @ requires !(0 <= i && i < int_size());
0441: @ signals (JMLSequenceException);
0442: @*/
0443: public Object itemAt(int i) throws JMLSequenceException {
0444: if (i < 0 || i >= int_length()) {
0445: throw new JMLSequenceException("Index out of range.");
0446: } else {
0447: JMLListEqualsNode this Walker = theSeq;
0448:
0449: int k = 0;
0450: //@ loop_invariant 0 <= k && k <= i && thisWalker != null;
0451: for (; k < i; k++) {
0452: this Walker = this Walker.next;
0453: }
0454: return (this Walker.head()); // head() clones if necessary
0455: }
0456: }
0457:
0458: /** Return the element at the given zero-based index; a synonym
0459: * for {@link #itemAt}.
0460: * @param i the zero-based index into the sequence.
0461: * @exception IndexOutOfBoundsException if the index i is out of range.
0462: * @see #itemAt(\bigint)
0463: */
0464: /*@ public normal_behavior
0465: @ requires 0 <= i && i < length; //FIXME, might use size();
0466: @ also
0467: @ public exceptional_behavior
0468: @ requires !(0 <= i && i < length); //FIXME, might use size());
0469: @ signals (IndexOutOfBoundsException);
0470: @
0471: model public Object get(\bigint i) throws IndexOutOfBoundsException;
0472: @*/
0473:
0474: /** Return the element at the given zero-based index; a synonym
0475: * for {@link #itemAt}.
0476: * @param i the zero-based index into the sequence.
0477: * @exception IndexOutOfBoundsException if the index i is out of range.
0478: * @see #itemAt(int)
0479: */
0480: /*@ public normal_behavior
0481: @ requires 0 <= i && i < length;
0482: @ also
0483: @ public exceptional_behavior
0484: @ requires !(0 <= i && i < length);
0485: @ signals (IndexOutOfBoundsException);
0486: @
0487: @*/
0488: public Object get(int i) throws IndexOutOfBoundsException {
0489: try {
0490: Object ret = itemAt(i);
0491: return ret;
0492: } catch (JMLSequenceException e) {
0493: IndexOutOfBoundsException e2 = new IndexOutOfBoundsException();
0494: e2.initCause(e);
0495: throw e2;
0496: }
0497: }
0498:
0499: /** Tells the number of elements in the sequence; a synonym for
0500: * {@link #length}.
0501: * @see #length()
0502: * @see #isEmpty()
0503: */
0504: /*@
0505: @ public normal_behavior
0506: @ ensures \result == length;
0507: @ public model pure \bigint size() {
0508: @ return length;
0509: @ }
0510: @*/
0511:
0512: /** Tells the number of elements in the sequence; a synonym for
0513: * {@link #length}.
0514: * @see #size()
0515: * @see #isEmpty()
0516: */
0517: /*@
0518: @ public normal_behavior
0519: @ ensures \result == length;
0520: @ public model pure \bigint length();
0521: @*/
0522:
0523: /** Tells the number of elements in the sequence; a synonym for
0524: * {@link #length}.
0525: * @see #length()
0526: * @see #isEmpty()
0527: */
0528: /*@ also
0529: @ protected normal_behavior
0530: @ requires size() <= Integer.MAX_VALUE;
0531: @ ensures \result == size();
0532: @
0533: @*/
0534: public int int_size() {
0535: return _length.intValue();
0536: }
0537:
0538: /** Tells the number of elements in the sequence; a synonym for
0539: * {@link #size}.
0540: * @see #int_size()
0541: */
0542: /*@
0543: @ public normal_behavior
0544: @ requires size() <= Integer.MAX_VALUE;
0545: @ ensures \result == size();
0546: @*/
0547: public int int_length() {
0548: return _length.intValue();
0549: }
0550:
0551: /** Tells the number of times a given element occurs in the sequence.
0552: * @see #has(Object)
0553: * @see #itemAt(int)
0554: */
0555: /*@ // //FIXME, remove // later
0556: @ public normal_behavior
0557: @ requires item != null;
0558: @ ensures \result
0559: @ == (\num_of \bigint i; 0 <= i && i < length();
0560: @ itemAt(i) != null
0561: @ && itemAt(i) .equals(item));
0562: @ also
0563: @ public normal_behavior
0564: @ requires item == null;
0565: @ ensures \result == (\num_of \bigint i; 0 <= i && i < length();
0566: @ itemAt(i) == null);
0567: model public \bigint bi_count(Object item);
0568: @*/
0569:
0570: /** Tells the number of times a given element occurs in the sequence.
0571: * @see #has(Object)
0572: * @see #itemAt(int)
0573: */
0574: /*@
0575: @ public normal_behavior
0576: @ requires item != null;
0577: @ ensures \result
0578: @ == (\num_of int i; 0 <= i && i < int_length();
0579: @ itemAt(i) != null
0580: @ && itemAt(i) .equals(item));
0581: @ also
0582: @ public normal_behavior
0583: @ requires item == null;
0584: @ ensures \result == (\num_of int i; 0 <= i && i < int_length();
0585: @ itemAt(i) == null);
0586: @*/
0587: public int count(Object item) {
0588: JMLListEqualsNode ptr = this .theSeq;
0589: int cnt = 0;
0590: while (ptr != null) {
0591: if (ptr.headEquals(item)) {
0592: cnt++;
0593: }
0594: ptr = ptr.next;
0595: }
0596: return cnt;
0597: }
0598:
0599: /** Tells whether the given element is ".equals" to an
0600: * element in the sequence.
0601: * @see #count(Object)
0602: */
0603: /*@ also
0604: @ public normal_behavior
0605: @ {|
0606: @ requires elem != null;
0607: @ ensures \result <==>
0608: @ (\exists int i; 0 <= i && i < int_length();
0609: @ itemAt(i) .equals(elem));
0610: @ also
0611: @ requires elem == null;
0612: @ ensures \result <==>
0613: @ (\exists int i; 0 <= i && i < int_length();
0614: @ itemAt(i) == null);
0615: @ |}
0616: @*/
0617: public boolean has(Object elem) {
0618: return theSeq != null && theSeq.has(elem);
0619: }
0620:
0621: /** Tell whether, for each element in the given collection, there is a
0622: * ".equals" element in this sequence.
0623: * @param c the collection whose elements are sought.
0624: */
0625: /*@ public normal_behavior
0626: @ requires c != null;
0627: @ ensures \result <==> (\forall Object o; c.contains(o); this.has(o));
0628: @*/
0629: public boolean containsAll(/*@ non_null @*/java.util.Collection c) {
0630: java.util.Iterator celems = c.iterator();
0631: while (celems.hasNext()) {
0632: Object o = celems.next();
0633: if (!has(o)) {
0634: return false;
0635: }
0636: }
0637: return true;
0638: }
0639:
0640: /** Tells whether the elements of the this sequence occur, in
0641: * order, at the beginning of the given sequence, using
0642: * ".equals" for comparisons.
0643: * @see #isProperPrefix
0644: * @see #isSuffix
0645: */
0646: /*@ public normal_behavior
0647: @ requires s2 != null;
0648: @ ensures \result <==>
0649: @ int_length() <= s2.int_length()
0650: @ && (\forall int i; 0 <= i && i < int_length();
0651: @ (s2.itemAt(i) != null
0652: @ && s2.itemAt(i) .equals(itemAt(i)))
0653: @ || (s2.itemAt(i) == null && itemAt(i) == null) );
0654: @*/
0655: public boolean isPrefix(/*@ non_null @*/JMLEqualsSequence s2) {
0656: return int_length() <= s2.int_length()
0657: && (theSeq == null || theSeq.isPrefixOf(s2.theSeq));
0658: }
0659:
0660: /** Tells whether this sequence is shorter than the given
0661: * sequence, and also if the elements of this sequence occur, in
0662: * order, at the beginning of the given sequence, using
0663: * ".equals" for comparisons.
0664: * @see #isPrefix
0665: * @see #isProperSuffix
0666: */
0667: /*@ public normal_behavior
0668: @ requires s2 != null;
0669: @ ensures \result <==> this.isPrefix(s2) && !this.equals(s2);
0670: @*/
0671: public boolean isProperPrefix(/*@ non_null @*/JMLEqualsSequence s2) {
0672: return int_length() != s2.int_length() && isPrefix(s2);
0673: }
0674:
0675: /** Tells whether the elements of this sequence occur, in order,
0676: * at the end of the given sequence, using ".equals" for
0677: * comparisons.
0678: * @see #isProperSuffix
0679: * @see #isPrefix
0680: */
0681: /*@ public normal_behavior
0682: @ requires s2 != null;
0683: @ ensures \result <==>
0684: @ int_length() <= s2.int_length()
0685: @ && this.equals(s2.removePrefix(s2.int_length() - int_length()));
0686: @*/
0687: public boolean isSuffix(/*@ non_null @*/JMLEqualsSequence s2) {
0688: if (int_length() > s2.int_length()) {
0689: return false;
0690: } else if (int_length() == 0) {
0691: return true;
0692: }
0693: JMLListEqualsNode suffix = s2.theSeq.removePrefix(s2
0694: .int_length()
0695: - int_length());
0696: return theSeq.equals(suffix);
0697: }
0698:
0699: /** Tells whether the this sequence is shorter than the given
0700: * object, and also if the elements of this sequence occur, in
0701: * order, at the end of the given sequence, using
0702: * ".equals" for comparisons.
0703: * @see #isSuffix
0704: * @see #isProperPrefix
0705: */
0706: /*@ public normal_behavior
0707: @ requires s2 != null;
0708: @ ensures \result <==> this.isSuffix(s2) && !this.equals(s2);
0709: @*/
0710: public boolean isProperSuffix(/*@ non_null @*/JMLEqualsSequence s2) {
0711: return int_length() != s2.int_length() && isSuffix(s2);
0712: }
0713:
0714: /** Test whether this object's value is equal to the given argument.
0715: * @see #isSuffix
0716: * @see #int_size()
0717: */
0718: /*@ also
0719: @ public normal_behavior
0720: @ requires obj != null && obj instanceof JMLEqualsSequence;
0721: @ ensures \result <==>
0722: @ isPrefix((JMLEqualsSequence)obj)
0723: @ && ((JMLEqualsSequence)obj).isPrefix(this);
0724: @ ensures_redundantly \result ==>
0725: @ containsNull == ((JMLEqualsSequence)obj).containsNull;
0726: @ also
0727: @ public normal_behavior
0728: @ requires obj == null || !(obj instanceof JMLEqualsSequence);
0729: @ ensures !\result;
0730: @*/
0731: public/*@ pure @*/boolean equals(Object obj) {
0732: return (obj != null && obj instanceof JMLEqualsSequence)
0733: && (int_length() == ((JMLEqualsSequence) obj)
0734: .int_length())
0735: && isPrefix((JMLEqualsSequence) obj);
0736: }
0737:
0738: /** Return a hash code for this object.
0739: */
0740: public int hashCode() {
0741: return (theSeq == null ? 0 : theSeq.hashCode());
0742: }
0743:
0744: /** Tells whether this sequence is empty.
0745: * @see #int_size()
0746: * @see #int_length()
0747: */
0748: /*@ public normal_behavior
0749: @ ensures \result == (int_length() == 0);
0750: @*/
0751: public/*@ pure @*/boolean isEmpty() {
0752: return theSeq == null;
0753: }
0754:
0755: /** Return the zero-based index of the first occurrence of the given
0756: * element in the sequence, if there is one
0757: * @param item the Object sought in this.
0758: * @return the first index at which item occurs.
0759: * @exception JMLSequenceException if item is not a member of the sequence.
0760: * @see #itemAt(int)
0761: */
0762: /*@ public normal_behavior
0763: @ requires has(item);
0764: @ {|
0765: @ requires item != null;
0766: @ ensures itemAt(\result) .equals(item)
0767: @ && (\forall \bigint i; 0 <= i && i < \result;
0768: @ !(itemAt(i) .equals(item)));
0769: @ also
0770: @ requires item == null;
0771: @ ensures itemAt(\result) == null
0772: @ && (\forall \bigint i; 0 <= i && i < \result;
0773: @ itemAt(i) != null);
0774: @ |}
0775: @ also
0776: @ public exceptional_behavior
0777: @ requires !has(item);
0778: @ signals (JMLSequenceException);
0779: @
0780: model public \bigint bi_indexOf(Object item) throws JMLSequenceException ;
0781: @*/
0782:
0783: /** Return the zero-based index of the first occurrence of the given
0784: * element in the sequence, if there is one
0785: * @param item the Object sought in this.
0786: * @return the first index at which item occurs.
0787: * @exception JMLSequenceException if item is not a member of the sequence.
0788: * @see #itemAt(int)
0789: */
0790: /*@ public normal_behavior
0791: @ requires has(item);
0792: @ {|
0793: @ requires item != null;
0794: @ ensures itemAt(\result) .equals(item)
0795: @ && (\forall int i; 0 <= i && i < \result;
0796: @ !(itemAt(i) .equals(item)));
0797: @ also
0798: @ requires item == null;
0799: @ ensures itemAt(\result) == null
0800: @ && (\forall int i; 0 <= i && i < \result;
0801: @ itemAt(i) != null);
0802: @ |}
0803: @ also
0804: @ public exceptional_behavior
0805: @ requires !has(item);
0806: @ signals (JMLSequenceException);
0807: @*/
0808: public int indexOf(Object item) throws JMLSequenceException {
0809: if (theSeq == null) {
0810: throw new JMLSequenceException(ITEM_PREFIX + item
0811: + IS_NOT_FOUND);
0812: }
0813: int idx = theSeq.indexOf(item);
0814: if (idx == -1) {
0815: throw new JMLSequenceException(ITEM_PREFIX + item
0816: + IS_NOT_FOUND);
0817: } else {
0818: return idx;
0819: }
0820: }
0821:
0822: private static final String ITEM_PREFIX = "item ";
0823: private static final String IS_NOT_FOUND = " is not in this sequence.";
0824:
0825: /** Return the first element in this sequence.
0826: * @exception JMLSequenceException if the sequence is empty.
0827: * @see #itemAt(int)
0828: * @see #last
0829: * @see #trailer
0830: * @see #header
0831: */
0832: /*@
0833: @ public normal_behavior
0834: @ requires int_length() > 0;
0835: @ {|
0836: @ requires itemAt(0) != null;
0837: @ ensures \result .equals(itemAt(0));
0838: @ also
0839: @ requires itemAt(0) == null;
0840: @ ensures \result == null;
0841: @ |}
0842: @ also
0843: @ public exceptional_behavior
0844: @ requires int_length() == 0;
0845: @ signals (JMLSequenceException);
0846: @*/
0847: public/*@ pure @*/Object first() throws JMLSequenceException {
0848: if (theSeq == null) {
0849: throw new JMLSequenceException(
0850: "Tried first() on empty sequence.");
0851: } else {
0852: return (theSeq.head()); // head() clones if necessary
0853: }
0854: }
0855:
0856: /** Return the last element in this sequence.
0857: * @exception JMLSequenceException if the sequence is empty.
0858: * @see #itemAt(int)
0859: * @see #first
0860: * @see #header
0861: * @see #trailer
0862: */
0863: /*@
0864: @ public normal_behavior
0865: @ requires int_length() >= 1;
0866: @ {|
0867: @ requires itemAt((int)(int_length()-1)) != null;
0868: @ ensures \result .equals(itemAt((int)(int_length()-1)));
0869: @ also
0870: @ requires itemAt((int)(int_length()-1)) == null;
0871: @ ensures \result == null;
0872: @ |}
0873: @ also
0874: @ public exceptional_behavior
0875: @ requires int_length() == 0;
0876: @ signals (JMLSequenceException);
0877: @*/
0878: public Object last() throws JMLSequenceException {
0879: if (theSeq == null) {
0880: throw new JMLSequenceException(
0881: "Tried last() on empty sequence.");
0882: } else {
0883: return theSeq.last(); // last() clones if necessary
0884: }
0885: }
0886:
0887: /** Tells whether this sequence is a subsequence of the given sequence.
0888: * @param s2 the sequence to search for within this sequence.
0889: * @return whether the elements of this occur (in order) within s2.
0890: * @see #isProperSubsequence
0891: * @see #isSupersequence
0892: */
0893: /*@ public normal_behavior
0894: @ requires s2 != null;
0895: @ ensures \result <==>
0896: @ int_length() <= s2.int_length()
0897: @ && (\exists int i; 0 <= i && i < s2.int_length()-int_length()+1;
0898: @ isPrefix(s2.removePrefix(i)));
0899: @*/
0900: public boolean isSubsequence(/*@ non_null @*/JMLEqualsSequence s2) {
0901: JMLListEqualsNode walker = s2.theSeq;
0902: for (int walkerLen = s2.int_length(); int_length() <= walkerLen; walkerLen--) {
0903: if (theSeq == null || theSeq.isPrefixOf(walker)) {
0904: return true;
0905: }
0906: walker = walker.next;
0907: }
0908: return false;
0909: }
0910:
0911: /** Tells whether this sequence is strictly shorter than the given
0912: * sequence and a subsequence of it.
0913: * @param s2 the sequence to search for within this sequence.
0914: * @return whether the elements of s2 occur (in order) within this.
0915: * @see #isSubsequence
0916: * @see #isProperSupersequence
0917: */
0918: /*@ public normal_behavior
0919: @ requires s2 != null;
0920: @ ensures \result <==>
0921: @ this.isSubsequence(s2) && !this.equals(s2);
0922: @*/
0923: public boolean isProperSubsequence(
0924: /*@ non_null @*/JMLEqualsSequence s2) {
0925: return int_length() < s2.int_length() && isSubsequence(s2);
0926: }
0927:
0928: /** Tells whether the given sequence is a supersequence of this sequence.
0929: * @param s2 the sequence to search within for this sequence.
0930: * @return whether the elements of this occur (in order) within s2.
0931: * @see #isProperSubsequence
0932: * @see #isSubsequence
0933: */
0934: /*@ public normal_behavior
0935: @ requires s2 != null;
0936: @ ensures \result <==> s2.isSubsequence(this);
0937: @*/
0938: public boolean isSupersequence(/*@ non_null @*/JMLEqualsSequence s2) {
0939: return s2.isSubsequence(this );
0940: }
0941:
0942: /** Tells whether the given sequence is both longer than and a
0943: * supersequence of this sequence.
0944: * @param s2 the sequence to search within for this sequence.
0945: * @return whether the elements of this occur (in order) within s2.
0946: * @see #isSupersequence
0947: * @see #isProperSubsequence
0948: */
0949: /*@ public normal_behavior
0950: @ requires s2 != null;
0951: @ ensures \result <==> s2.isProperSubsequence(this);
0952: @*/
0953: public boolean isProperSupersequence(
0954: /*@ non_null @*/JMLEqualsSequence s2) {
0955: return s2.isProperSubsequence(this );
0956: }
0957:
0958: /** Tells whether this sequence is the result of inserting the
0959: * given element once into the given sequence. That is, this
0960: * sequence is exactly one element longer than the given
0961: * sequence, and its elements are in the same order, except for
0962: * the insertion of the given element.
0963: * @param s2 the shorter sequence, which we see if the elem is
0964: * inserted into
0965: * @param elem the given element
0966: * @return whether the elements of s2 occur in order in this
0967: * sequence, with the insertion of elem somewhere.
0968: * @see #isDeletionFrom
0969: * @see #isProperSupersequence
0970: * @see #isProperSubsequence
0971: * @see #subsequence
0972: */
0973: /*@ public normal_behavior
0974: @ requires s2 != null;
0975: @ ensures \result <==>
0976: @ (\exists int i; 0 <= i && i < int_length();
0977: @ itemAt(i) .equals(elem)
0978: @ && subsequence(0,i)
0979: @ .concat(subsequence((int)(i+1),int_length()))
0980: @ .equals(s2));
0981: @ ensures_redundantly \result ==> this.int_length() == s2.int_length()+1;
0982: @ ensures_redundantly \result ==> has(elem);
0983: @ ensures_redundantly \result <==> s2.isDeletionFrom(this, elem);
0984: @*/
0985: public boolean isInsertionInto(
0986: /*@ non_null @*/JMLEqualsSequence s2, Object elem) {
0987: if (int_length() != s2.int_length() + 1) {
0988: return false;
0989: }
0990: JMLListEqualsNode walker = theSeq;
0991: JMLListEqualsNode s2walker = s2.theSeq;
0992: /*@ maintaining subsequence(0, (int)(int_length()-lenRemaining))
0993: @ .equals(s2.subsequence(0, (int)(int_length()-lenRemaining)));
0994: @ decreasing int_length();
0995: @*/
0996: for (int lenRemaining = int_length(); lenRemaining > 0; lenRemaining--) {
0997: if (walker.headEquals(elem)) {
0998: if ((walker.next == null && s2walker == null)
0999: || (walker.next != null && walker.next
1000: .equals(s2walker))) {
1001: return true;
1002: }
1003: }
1004: if (s2walker == null || !s2walker.headEquals(walker.head())) {
1005: return false;
1006: }
1007: walker = walker.next;
1008: s2walker = s2walker.next;
1009: }
1010: return false;
1011: }
1012:
1013: /** Tells whether this sequence is the result of deleting the
1014: * given element once from the given sequence. That is, this
1015: * sequence is exactly one element shorter than the given
1016: * sequence, and its elements are in the same order, except for
1017: * the deletion of the given element from the given sequence.
1018: * @param s2 the longer sequence, in which we see if the elem is
1019: * deleted from
1020: * @param elem the given element
1021: * @return whether the elements of s2 occur in order in this
1022: * sequence, with the deletion of elem somewhere.
1023: * @see #isInsertionInto
1024: * @see #isProperSupersequence
1025: * @see #isProperSubsequence
1026: * @see #subsequence
1027: */
1028: /*@ public normal_behavior
1029: @ requires s2 != null;
1030: @ ensures \result <==>
1031: @ (\exists int i; 0 <= i && i < s2.int_length();
1032: @ s2.itemAt(i) .equals(elem)
1033: @ && this.equals(s2.removeItemAt(i)));
1034: @ ensures_redundantly \result ==> this.int_length()+1 == s2.int_length();
1035: @ ensures_redundantly \result ==> s2.has(elem);
1036: @ ensures_redundantly \result <==> s2.isInsertionInto(this, elem);
1037: @*/
1038: public boolean isDeletionFrom(
1039: /*@ non_null @*/JMLEqualsSequence s2, Object elem) {
1040: return s2.isInsertionInto(this , elem);
1041: }
1042:
1043: // *************** building new JMLEqualsSequences **********************
1044:
1045: /** Return a clone of this object. This method does not clone the
1046: * elements of the sequence.
1047: */
1048: /*@ also
1049: @ public normal_behavior
1050: @ ensures \result != null
1051: @ && \result instanceof JMLEqualsSequence
1052: @ && ((JMLEqualsSequence)\result).equals(this);
1053: @*/
1054: public Object clone() {
1055: return this ;
1056: }
1057:
1058: /** Return a sequence containing the first n elements in this sequence.
1059: * @param n the number of elements in the result.
1060: * @exception JMLSequenceException if n is negative or greater than
1061: * the length of the sequence.
1062: * @see #trailer
1063: * @see #removePrefix
1064: * @see #subsequence
1065: */
1066: /*@ public normal_behavior
1067: @ requires 0 <= n && n <= length;
1068: @ ensures \result.length == n
1069: @ && (\forall \bigint i; 0 <= i && i < n;
1070: @ (\result.itemAt(i) != null
1071: @ ==> \result.itemAt(i) .equals(itemAt(i)))
1072: @ || (\result.itemAt(i) == null
1073: @ ==> itemAt(i) == null) );
1074: @ also
1075: @ public exceptional_behavior
1076: @ requires !(0 <= n && n <= length);
1077: @ signals (JMLSequenceException);
1078: @
1079: @
1080: @ model public JMLEqualsSequence prefix(\bigint n);
1081: @*/
1082:
1083: /** Return a sequence containing the first n elements in this sequence.
1084: * @param n the number of elements in the result.
1085: * @exception JMLSequenceException if n is negative or greater than
1086: * the length of the sequence.
1087: * @see #trailer
1088: * @see #removePrefix
1089: * @see #subsequence
1090: */
1091: /*@ public normal_behavior
1092: @ requires 0 <= n && n <= length;
1093: @ ensures \result.length == n
1094: @ && (\forall int i; 0 <= i && i < n;
1095: @ (\result.itemAt(i) != null
1096: @ ==> \result.itemAt(i) .equals(itemAt(i)))
1097: @ || (\result.itemAt(i) == null
1098: @ ==> itemAt(i) == null) );
1099: @ also
1100: @ public exceptional_behavior
1101: @ requires !(0 <= n && n <= length);
1102: @ signals (JMLSequenceException);
1103: @ also
1104: @ public behavior
1105: @ ensures !containsNull ==> !\result.containsNull;
1106: @
1107: @*/
1108: public/*@ non_null @*/JMLEqualsSequence prefix(int n)
1109: throws JMLSequenceException {
1110: if (n < 0 || n > int_length()) {
1111: throw new JMLSequenceException(
1112: "Invalid parameter to prefix() with n = " + n
1113: + "\n" + " when sequence length = "
1114: + int_length());
1115: } else {
1116: if (n == 0) {
1117: return new JMLEqualsSequence();
1118: } else {
1119: JMLListEqualsNode pfx_list = theSeq.prefix(n);
1120: return new JMLEqualsSequence(pfx_list, n);
1121: }
1122: }
1123: }
1124:
1125: /** Return a sequence containing all but the first n elements in this.
1126: * @param n the number of elements to remove
1127: * @exception JMLSequenceException if n is negative or greater than
1128: * the length of the sequence.
1129: * @see #header
1130: * @see #prefix
1131: * @see #subsequence
1132: */
1133: /*@ public normal_behavior
1134: @ requires 0 <= n && n <= length;
1135: @ ensures \result.length == length - n
1136: @ && (\forall \bigint i; n <= i && i < length;
1137: @ (\result.itemAt(i-n) != null
1138: @ && \result.itemAt(i-n) .equals(itemAt(i)))
1139: @ || (\result.itemAt(i-n) == null
1140: @ && itemAt(i) == null) );
1141: @ also
1142: @ public exceptional_behavior
1143: @ requires !(0 <= n && n <= length);
1144: @ signals (JMLSequenceException);
1145: @
1146: model public JMLEqualsSequence removePrefix(\bigint n);
1147: @*/
1148:
1149: /** Return a sequence containing all but the first n elements in this.
1150: * @param n the number of elements to remove
1151: * @exception JMLSequenceException if n is negative or greater than
1152: * the length of the sequence.
1153: * @see #header
1154: * @see #prefix
1155: * @see #subsequence
1156: */
1157: /*@ public normal_behavior
1158: @ requires 0 <= n && n <= length;
1159: @ ensures \result.length == length - n
1160: @ && (\forall \bigint i; n <= i && i < length;
1161: @ (\result.itemAt((int)(i-n)) != null
1162: @ && \result.itemAt((int)(i-n)) .equals(itemAt(i)))
1163: @ || (\result.itemAt((int)(i-n)) == null
1164: @ && itemAt(i) == null) );
1165: @ also
1166: @ public exceptional_behavior
1167: @ requires !(0 <= n && n <= length);
1168: @ signals (JMLSequenceException);
1169: @*/
1170: public/*@ non_null @*/JMLEqualsSequence removePrefix(int n)
1171: throws JMLSequenceException {
1172: if (n < 0 || n > int_length()) {
1173: throw new JMLSequenceException(
1174: "Invalid parameter to removePrefix() "
1175: + "with n = " + n + "\n"
1176: + " when sequence length = "
1177: + int_length());
1178: } else {
1179: if (n == 0) {
1180: return this ;
1181: } else {
1182: JMLListEqualsNode pfx_list = theSeq.removePrefix(n);
1183: return new JMLEqualsSequence(pfx_list, int_length() - n);
1184: }
1185: }
1186: }
1187:
1188: /** Return a sequence that is the concatenation of this with
1189: * the given sequence.
1190: * @param s2 the sequence to place at the end of this sequence in
1191: * the result.
1192: * @return the concatenation of this sequence and s2.
1193: */
1194: /*@ public normal_behavior
1195: @ requires s2 != null;
1196: @ ensures \result.int_length() == int_length() + s2.int_length()
1197: @ && (\forall int i; 0 <= i && i < int_length();
1198: @ (\result.itemAt(i) != null
1199: @ && \result.itemAt(i) .equals(itemAt(i)))
1200: @ || (\result.itemAt(i) == null
1201: @ && itemAt(i) == null) )
1202: @ && (\forall int i; 0 <= i && i < s2.int_length();
1203: @ (\result.itemAt((int)(int_length()+i)) != null
1204: @ && \result.itemAt((int)(int_length()+i)) .equals(s2.itemAt(i)))
1205: @ || (\result.itemAt((int)(int_length()+i)) == null
1206: @ && s2.itemAt(i) == null) );
1207: @*/
1208: public/*@ non_null @*/
1209: JMLEqualsSequence concat(/*@ non_null @*/JMLEqualsSequence s2) {
1210: if (theSeq == null) {
1211: return s2;
1212: } else if (s2.theSeq == null) {
1213: return this ;
1214: } else {
1215: JMLListEqualsNode new_list = theSeq.concat(s2.theSeq);
1216: return new JMLEqualsSequence(new_list, int_length()
1217: + s2.int_length());
1218: }
1219: }
1220:
1221: /** Return a sequence that is the reverse of this sequence.
1222: * @return the reverse of this sequence.
1223: */
1224: /*@ public normal_behavior
1225: @ old int len = int_length();
1226: @ ensures \result.int_length() == len
1227: @ && (\forall int i; 0 <= i && i < len;
1228: @ (\result.itemAt((int)(len-i-1)) != null
1229: @ && \result.itemAt((int)(len-i-1)) .equals(itemAt(i)))
1230: @ || (\result.itemAt((int)(len-i-1)) == null
1231: @ && itemAt(i) == null) );
1232: @ also
1233: @ public behavior
1234: @ ensures elementType == \result.elementType;
1235: @ ensures containsNull <==> \result.containsNull;
1236: @*/
1237: public/*@ non_null @*/JMLEqualsSequence reverse() {
1238: if (theSeq == null) {
1239: return this ;
1240: } else {
1241: JMLListEqualsNode r = theSeq.reverse();
1242: return new JMLEqualsSequence(r, int_length());
1243: }
1244: }
1245:
1246: /** Return a sequence like this, but without the element at the
1247: * given zero-based index.
1248: * @param index the zero-based index into the sequence.
1249: * @exception JMLSequenceException if the index is out of range.
1250: * @see #itemAt(int)
1251: * @see #removeItemAt
1252: * @see #prefix
1253: * @see #removePrefix
1254: * @see #subsequence
1255: * @see #concat
1256: */
1257: /*@ public normal_behavior
1258: @ requires 0 <= index && index < length();
1259: @ ensures \result.equals(prefix(index).concat(removePrefix(index+1)));
1260: @ also
1261: @ public exceptional_behavior
1262: @ requires !(0 <= index && index < length());
1263: @ signals (JMLSequenceException);
1264: @
1265: @
1266: model public non_null JMLEqualsSequence removeItemAt(\bigint index)
1267: throws JMLSequenceException;
1268: @*/
1269:
1270: /** Return a sequence like this, but without the element at the
1271: * given zero-based index.
1272: * @param index the zero-based index into the sequence.
1273: * @exception JMLSequenceException if the index is out of range.
1274: * @see #itemAt(int)
1275: * @see #removeItemAt
1276: * @see #prefix
1277: * @see #removePrefix
1278: * @see #subsequence
1279: * @see #concat
1280: */
1281: /*@ public normal_behavior
1282: @ requires 0 <= index && index < int_length();
1283: @ ensures \result.equals(prefix(index).concat(removePrefix((int)(index+1))));
1284: @ also
1285: @ public exceptional_behavior
1286: @ requires !(0 <= index && index < int_length());
1287: @ signals (JMLSequenceException);
1288: @
1289: @*/
1290: public/*@ non_null @*/JMLEqualsSequence removeItemAt(int index)
1291: throws JMLSequenceException {
1292: if (0 <= index && index < int_length()) {
1293: JMLListEqualsNode new_list = theSeq.removeItemAt(index);
1294: return new JMLEqualsSequence(new_list, int_length() - 1);
1295: } else {
1296: throw new JMLSequenceException(
1297: "Invalid parameter to removeItemAt() "
1298: + "with index = " + index + "\n"
1299: + " when sequence length = "
1300: + int_length());
1301: }
1302: }
1303:
1304: /** Return a sequence like this, but with item replacing the element at the
1305: * given zero-based index.
1306: * @param index the zero-based index into the sequence.
1307: * @param item the item to put at index index
1308: * @exception JMLSequenceException if the index is out of range.
1309: * @see #itemAt(int)
1310: * @see #replaceItemAt
1311: */
1312: /*@ public normal_behavior
1313: @ requires 0 <= index && index < length();
1314: @ ensures \result.equals(removeItemAt(index).insertBeforeIndex(index,
1315: @ item));
1316: @ also
1317: @ public exceptional_behavior
1318: @ requires !(0 <= index && index < length());
1319: @ signals (JMLSequenceException);
1320: @
1321: model public non_null JMLEqualsSequence
1322: replaceItemAt(\bigint index, Object item)
1323: throws JMLSequenceException;
1324: @*/
1325:
1326: /** Return a sequence like this, but with item replacing the element at the
1327: * given zero-based index.
1328: * @param index the zero-based index into the sequence.
1329: * @param item the item to put at index index
1330: * @exception JMLSequenceException if the index is out of range.
1331: * @see #itemAt(int)
1332: * @see #replaceItemAt
1333: */
1334: /*@ public normal_behavior
1335: @ requires 0 <= index && index < int_length();
1336: @ ensures \result.equals(removeItemAt(index).insertBeforeIndex(index,
1337: @ item));
1338: @ also
1339: @ public exceptional_behavior
1340: @ requires !(0 <= index && index < int_length());
1341: @ signals (JMLSequenceException);
1342: @*/
1343: public/*@ non_null @*/JMLEqualsSequence replaceItemAt(int index,
1344: Object item) throws JMLSequenceException {
1345: if (0 <= index && index < int_length()) {
1346: // replaceItemAt() clones item, if necessary
1347: JMLListEqualsNode new_list = theSeq.replaceItemAt(index,
1348: item);
1349: return new JMLEqualsSequence(new_list, int_length());
1350: } else {
1351: throw new JMLSequenceException(
1352: "Invalid parameter to replaceItemAt() "
1353: + "with index = " + index + "\n"
1354: + " when sequence length = "
1355: + int_length());
1356: }
1357: }
1358:
1359: /** Return a sequence containing all but the last element in this.
1360: * @exception JMLSequenceException if this is empty.
1361: * @see #prefix
1362: * @see #first
1363: * @see #last
1364: * @see #trailer
1365: * @see #subsequence
1366: */
1367: /*@ public normal_behavior
1368: @ requires int_length() >= 1;
1369: @ ensures \result.equals(removeItemAt((int)(int_length()-1)));
1370: @ ensures_redundantly \result.int_length() == int_length() - 1;
1371: @ also
1372: @ public exceptional_behavior
1373: @ requires int_length() == 0;
1374: @ signals (JMLSequenceException);
1375: @
1376: @*/
1377: public/*@ non_null @*/JMLEqualsSequence header()
1378: throws JMLSequenceException {
1379: if (theSeq == null) {
1380: throw new JMLSequenceException(
1381: "Tried header() on empty sequence.");
1382: } else {
1383: JMLListEqualsNode new_list = theSeq.removeLast();
1384: return new JMLEqualsSequence(new_list, int_length() - 1);
1385: }
1386: }
1387:
1388: /** Return a sequence containing all but the first element in this.
1389: * @exception JMLSequenceException if this is empty.
1390: * @see #removePrefix
1391: * @see #last
1392: * @see #first
1393: * @see #header
1394: * @see #subsequence
1395: */
1396: /*@ public normal_behavior
1397: @ requires int_length() >= 1;
1398: @ ensures \result.equals(removePrefix(1));
1399: @ ensures_redundantly \result.int_length() == int_length() - 1;
1400: @ also
1401: @ public exceptional_behavior
1402: @ requires int_length() == 0;
1403: @ signals (JMLSequenceException);
1404: @*/
1405: public/*@ pure @*//*@ non_null @*/JMLEqualsSequence trailer()
1406: throws JMLSequenceException {
1407: if (theSeq == null) {
1408: throw new JMLSequenceException(
1409: "Tried trailer() on empty sequence.");
1410: } else {
1411: JMLListEqualsNode new_list = theSeq.next;
1412: return new JMLEqualsSequence(new_list, int_length() - 1);
1413: }
1414: }
1415:
1416: /** Return a sequence like this, but with item put immediately after
1417: * the given index.
1418: * @param afterThisOne a zero-based index into the sequence, or -1.
1419: * @param item the item to put after index afterThisOne
1420: * @return if the index is in range
1421: * @exception JMLSequenceException if the index is out of range.
1422: * @see #insertBeforeIndex
1423: * @see #insertFront
1424: * @see #insertBack
1425: * @see #removeItemAt
1426: */
1427: /*@ //FIXME, _ alsoIfValue _
1428: @ public normal_behavior
1429: @ requires -1 <= afterThisOne && afterThisOne < length;
1430: @ requires length < Integer.MAX_VALUE;
1431: @ ensures \result.equals(insertBeforeIndex((int)(afterThisOne + 1), item));
1432: @ also
1433: @ public exceptional_behavior
1434: @ requires !(-1 <= afterThisOne && afterThisOne < length);
1435: @ signals (JMLSequenceException);
1436: @
1437: model public JMLEqualsSequence insertAfterIndex(\bigint afterThisOne,
1438: Object item)
1439: throws JMLSequenceException, IllegalStateException;
1440: @*/
1441:
1442: /** Return a sequence like this, but with item put immediately after
1443: * the given index.
1444: * @param afterThisOne a zero-based index into the sequence, or -1.
1445: * @param item the item to put after index afterThisOne
1446: * @return if the index is in range
1447: * @exception JMLSequenceException if the index is out of range.
1448: * @see #insertBeforeIndex
1449: * @see #insertFront
1450: * @see #insertBack
1451: * @see #removeItemAt
1452: */
1453: /*@
1454: @ public normal_behavior
1455: @ requires -1 <= afterThisOne && afterThisOne < length;
1456: @ requires length < Integer.MAX_VALUE;
1457: @ ensures \result.equals(insertBeforeIndex((int)(afterThisOne + 1), item));
1458: @ also
1459: @ public exceptional_behavior
1460: @ requires !(-1 <= afterThisOne && afterThisOne < length);
1461: @ signals (JMLSequenceException);
1462: @*/
1463: public/*@ non_null @*/JMLEqualsSequence insertAfterIndex(
1464: int afterThisOne, Object item) throws JMLSequenceException,
1465: IllegalStateException {
1466: if (afterThisOne < -1 || afterThisOne >= int_length()) {
1467: throw new JMLSequenceException("Invalid parameter to "
1468: + "insertAfterIndex() " + "with afterThisOne = "
1469: + afterThisOne + "\n"
1470: + " when sequence length = " + int_length());
1471: } else if (int_length() < Integer.MAX_VALUE) {
1472: return insertBeforeIndex(afterThisOne + 1, item);
1473: } else {
1474: throw new IllegalStateException(TOO_BIG_TO_INSERT);
1475: }
1476: }
1477:
1478: private static final String TOO_BIG_TO_INSERT = "Cannot insert into a sequence with Integer.MAX_VALUE elements.";
1479:
1480: /** Return a sequence like this, but with item put immediately
1481: * before the given index.
1482: * @param beforeThisOne a zero-based index into the sequence,
1483: * or the length of this.
1484: * @param item the item to put before index beforeThisOne
1485: * @return if the index is in range
1486: * @exception JMLSequenceException if the index is out of range.
1487: * @see #insertAfterIndex
1488: * @see #insertFront
1489: * @see #insertBack
1490: * @see #removeItemAt
1491: */
1492: /*@ //FIXME, _ alsoIfValue _
1493: @ public normal_behavior
1494: @ requires 0 <= beforeThisOne && beforeThisOne <= length;
1495: @ requires length < Integer.MAX_VALUE;
1496: @ ensures \result.equals(
1497: @ prefix(beforeThisOne).
1498: @ concat(new JMLEqualsSequence(item)).
1499: @ concat(removePrefix(beforeThisOne))
1500: @ );
1501: @ also
1502: @ public exceptional_behavior
1503: @ requires !(0 <= beforeThisOne && beforeThisOne <= length);
1504: @ signals (JMLSequenceException);
1505: @
1506: model public
1507: JMLEqualsSequence insertBeforeIndex(\bigint beforeThisOne, Object item)
1508: throws JMLSequenceException, IllegalStateException ;
1509: @*/
1510:
1511: /** Return a sequence like this, but with item put immediately
1512: * before the given index.
1513: * @param beforeThisOne a zero-based index into the sequence,
1514: * or the length of this.
1515: * @param item the item to put before index beforeThisOne
1516: * @return if the index is in range
1517: * @exception JMLSequenceException if the index is out of range.
1518: * @see #insertAfterIndex
1519: * @see #insertFront
1520: * @see #insertBack
1521: * @see #removeItemAt
1522: */
1523: /*@
1524: @ public normal_behavior
1525: @ requires 0 <= beforeThisOne && beforeThisOne <= length;
1526: @ requires length < Integer.MAX_VALUE;
1527: @ ensures \result.equals(
1528: @ prefix(beforeThisOne).
1529: @ concat(new JMLEqualsSequence(item)).
1530: @ concat(removePrefix(beforeThisOne))
1531: @ );
1532: @ also
1533: @ public exceptional_behavior
1534: @ requires !(0 <= beforeThisOne && beforeThisOne <= length);
1535: @ signals (JMLSequenceException);
1536: @*/
1537: public/*@ non_null @*/
1538: JMLEqualsSequence insertBeforeIndex(int beforeThisOne, Object item)
1539: throws JMLSequenceException, IllegalStateException {
1540: if (beforeThisOne < 0 || beforeThisOne > int_length()) {
1541: throw new JMLSequenceException(
1542: "Invalid parameter to insertBeforeIndex()"
1543: + " with beforeThisOne = " + beforeThisOne
1544: + "\n" + " when sequence length = "
1545: + int_length());
1546: } else if (int_length() < Integer.MAX_VALUE) {
1547: if (theSeq == null) {
1548: return new JMLEqualsSequence(item);
1549: } else {
1550: // insertBefore() clones item, if necessary
1551: JMLListEqualsNode new_list = theSeq.insertBefore(
1552: beforeThisOne, item);
1553: return new JMLEqualsSequence(new_list, int_length() + 1);
1554: }
1555: } else {
1556: throw new IllegalStateException(TOO_BIG_TO_INSERT);
1557: }
1558: }
1559:
1560: /** Return a sequence like this, but with the given item put an the end.
1561: * @param item the item to put at the end of the result.
1562: * @return a sequence the elements of this sequence followed by item.
1563: * @see #insertAfterIndex
1564: * @see #insertBeforeIndex
1565: * @see #insertFront
1566: * @see #removeItemAt
1567: * @see #header
1568: * @see #last
1569: */
1570: /*@
1571: @ public normal_behavior
1572: @ requires int_length() < Integer.MAX_VALUE;
1573: @ ensures \result.equals(insertBeforeIndex(int_length(), item));
1574: @ ensures_redundantly
1575: @ \result.int_length() == int_length() + 1
1576: @ && isProperPrefix(\result);
1577: @*/
1578: public/*@ non_null @*/JMLEqualsSequence insertBack(Object item)
1579: throws IllegalStateException {
1580: if (theSeq == null) {
1581: return new JMLEqualsSequence(item);
1582: } else if (int_length() < Integer.MAX_VALUE) {
1583: // append() clones item, if necessary
1584: return new JMLEqualsSequence(theSeq.append(item),
1585: int_length() + 1);
1586: } else {
1587: throw new IllegalStateException(TOO_BIG_TO_INSERT);
1588: }
1589: }
1590:
1591: /** Return a sequence like this, but with the given item put an the front.
1592: * @param item the item to put at the front of the result.
1593: * @return a sequence with item followed by the elements of this sequence.
1594: * @see #insertAfterIndex
1595: * @see #insertBeforeIndex
1596: * @see #insertBack
1597: * @see #removeItemAt
1598: * @see #trailer
1599: * @see #first
1600: */
1601: /*@
1602: @ public normal_behavior
1603: @ requires int_length() < Integer.MAX_VALUE;
1604: @ ensures \result.equals(insertBeforeIndex(0, item));
1605: @ ensures_redundantly
1606: @ \result.int_length() == int_length() + 1
1607: @ && \result.trailer().equals(this);
1608: @*/
1609: public/*@ pure @*//*@ non_null @*/JMLEqualsSequence insertFront(
1610: Object item) throws IllegalStateException {
1611: if (theSeq == null) {
1612: return new JMLEqualsSequence(item);
1613: } else if (int_length() < Integer.MAX_VALUE) {
1614: return new JMLEqualsSequence(
1615: // cons() clones item, if necessary
1616: JMLListEqualsNode.cons(item, theSeq),
1617: int_length() + 1);
1618: } else {
1619: throw new IllegalStateException(TOO_BIG_TO_INSERT);
1620: }
1621: }
1622:
1623: /** Returns a subsequence of this containing the elements beginning
1624: * with index from (inclusive) and ending with index to (exclusive).
1625: * @param from the inclusive, zero-based element of the first
1626: * element in the subsequence.
1627: * @param to the zero-based element of the first element that
1628: * should not be in the subsequence.
1629: * @exception JMLSequenceException if (from < 0 or from > to
1630: * or to > length of this.
1631: * @see #prefix
1632: * @see #removePrefix
1633: * @see #header
1634: * @see #trailer
1635: * @see #concat
1636: */
1637: /*@ public normal_behavior
1638: @ requires 0 <= from && from <= to && to <= length();
1639: @ ensures \result.equals(removePrefix(from).prefix((int)(to - from)))
1640: @ && \result.length() == to - from;
1641: @ also
1642: @ public exceptional_behavior
1643: @ requires !(0 <= from && from <= to && to <= length());
1644: @ signals (JMLSequenceException);
1645: @ also
1646: @ public behavior
1647: @ ensures !\result.containsNull <== !containsNull;
1648: @
1649: model public non_null JMLEqualsSequence subsequence(\bigint from, \bigint to)
1650: throws JMLSequenceException ;
1651: @*/
1652:
1653: /** Returns a subsequence of this containing the elements beginning
1654: * with index from (inclusive) and ending with index to (exclusive).
1655: * @param from the inclusive, zero-based element of the first
1656: * element in the subsequence.
1657: * @param to the zero-based element of the first element that
1658: * should not be in the subsequence.
1659: * @exception JMLSequenceException if (from < 0 or from > to
1660: * or to > length of this.
1661: * @see #prefix
1662: * @see #removePrefix
1663: * @see #header
1664: * @see #trailer
1665: * @see #concat
1666: */
1667: /*@ public normal_behavior
1668: @ requires 0 <= from && from <= to && to <= int_length();
1669: @ ensures \result.equals(removePrefix(from).prefix((int)(to - from)))
1670: @ && \result.int_length() == to - from;
1671: @ also
1672: @ public exceptional_behavior
1673: @ requires !(0 <= from && from <= to && to <= int_length());
1674: @ signals (JMLSequenceException);
1675: @ also
1676: @ public behavior
1677: @ ensures !\result.containsNull <== !containsNull;
1678: @*/
1679: public/*@ non_null @*/JMLEqualsSequence subsequence(int from,
1680: int to) throws JMLSequenceException {
1681: if (from < 0 || from > to || to > int_length()) {
1682: throw new JMLSequenceException("Invalid parameters to "
1683: + "subsequence() with from = " + from
1684: + " and to = " + to + "\n" + " "
1685: + "when sequence length = " + int_length());
1686: } else {
1687: if (theSeq == null) {
1688: return this ; // i.e., from == to == int_length() == 0
1689: } else {
1690: JMLListEqualsNode removedPrefix = theSeq
1691: .removePrefix(from);
1692: if (removedPrefix == null) {
1693: return new JMLEqualsSequence();
1694: } else {
1695: JMLListEqualsNode new_list = removedPrefix
1696: .prefix(to - from);
1697: return new JMLEqualsSequence(new_list, to - from);
1698: }
1699: }
1700: }
1701: }
1702:
1703: /** Return a new JMLEqualsBag containing all the elements of this.
1704: * @see #toSet()
1705: * @see #toArray()
1706: */
1707: /*@ public normal_behavior
1708: @ ensures \result != null
1709: @ && (\forall int i; 0 <= i && i < int_length();
1710: @ \result.count(this.itemAt(i))
1711: @ == this.count(this.itemAt(i)));
1712: @*/
1713: public /*@ non_null @*/ JMLEqualsBag toBag() {
1714: JMLEqualsBag ret = new JMLEqualsBag();
1715: JMLEqualsSequenceEnumerator enum = elements();
1716: while (enum.hasMoreElements()) {
1717: Object o = enum.nextElement();
1718: Object e = (o == null ? null : o);
1719: ret = ret.insert(e);
1720: }
1721: return ret;
1722: }
1723: /** Return a new JMLEqualsSet containing all the elements of this.
1724: * @see #toBag()
1725: * @see #toArray()
1726: */
1727: /*@ public normal_behavior
1728: @ ensures \result != null
1729: @ && (\forall Object o;; \result.has(o) == this.has(o));
1730: @*/
1731: public /*@ non_null @*/ JMLEqualsSet toSet() {
1732: JMLEqualsSet ret = new JMLEqualsSet();
1733: JMLEqualsSequenceEnumerator enum = elements();
1734: while (enum.hasMoreElements()) {
1735: Object o = enum.nextElement();
1736: Object e = (o == null ? null : o);
1737: ret = ret.insert(e);
1738: }
1739: return ret;
1740: }
1741: /** Return a new array containing all the elements of this in order.
1742: * @see #toSet()
1743: * @see #toBag()
1744: */
1745: /*@ public normal_behavior
1746: @ ensures \result != null && \result.length == int_length()
1747: @ && (\forall int i; 0 <= i && i < int_length();
1748: @ (\result[i] == null ==> this.itemAt(i) == null)
1749: @ && (\result[i] != null ==>
1750: @ \result[i] .equals(this.itemAt(i))));
1751: @*/
1752: public /*@ non_null @*/ Object[] toArray() {
1753: Object[] ret = new Object[int_length()];
1754: JMLEqualsSequenceEnumerator enum = elements();
1755: int i = 0;
1756: //@ loop_invariant 0 <= i && i <= ret.length;
1757: while (enum.hasMoreElements()) {
1758: Object o = enum.nextElement();
1759: if (o == null) {
1760: ret[i] = null;
1761: } else {
1762: Object e = o;
1763: ret[i] = e ;
1764: }
1765: i++;
1766: }
1767: return ret;
1768: }
1769: //********************** Tools Methods *********************************
1770:
1771: // The enumerator method and toString are of no value for writing
1772: // assertions in JML. They are included for the use of developers
1773: // of CASE tools based on JML, e.g., type checkers, assertion
1774: // evaluators, prototype generators, test tools, ... . They can
1775: // also be used in model programs in specifications.
1776:
1777: /** Return a enumerator for this.
1778: * @see #iterator()
1779: * @see #itemAt()
1780: */
1781: /*@ public normal_behavior
1782: @ ensures \fresh(\result);
1783: @*/
1784: public/*@ non_null @*/JMLEqualsSequenceEnumerator elements() {
1785: JMLEqualsSequenceEnumerator retValue = new JMLEqualsSequenceEnumerator(
1786: this );
1787: return retValue;
1788: }
1789:
1790: /** Returns an iterator over this sequence.
1791: * @see #elements()
1792: */
1793: /*@ also
1794: @ public normal_behavior
1795: @ ensures \fresh(\result)
1796: @ && \result.equals(new JMLEnumerationToIterator(elements()));
1797: @*/
1798: public JMLIterator iterator() {
1799: return new JMLEnumerationToIterator(elements());
1800: }
1801:
1802: public String toString() {
1803: String newStr = "(<";
1804: JMLListEqualsNode seqWalker = theSeq;
1805: boolean first = true;
1806: while (seqWalker != null) {
1807: if (!first) {
1808: newStr = newStr + ", ";
1809: }
1810: newStr = newStr + seqWalker.val;
1811: first = false;
1812: seqWalker = seqWalker.next;
1813: }
1814: return (newStr + ">)");
1815: }
1816:
1817: }
|