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