0001: // @(#)$Id: JMLEqualsBag.java 1.4 Tue, 17 May 2005 14:57:40 +0200 engelc $
0002:
0003: // Copyright (C) 1998, 1999, 2002 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: /** Bags (i.e., multisets) of objects. This type uses
0024: * ".equals" to compare elements, and does not clone elements that
0025: * are passed into and returned from the bag's methods.
0026: *
0027: * @version $Revision: 1.4 $
0028: * @author Gary T. Leavens, with help from Albert Baker, Clyde Ruby,
0029: * and others.
0030: * @see JMLCollection
0031: * @see JMLType
0032: * @see JMLObjectBag
0033: * @see JMLValueBag
0034: * @see JMLEqualsBagEnumerator
0035: *
0036: * @see JMLObjectSet
0037: * @see JMLValueSet
0038: */
0039: //-@ immutable
0040: public/*@ pure @*/class JMLEqualsBag implements JMLCollection {
0041:
0042: /** The list representing the contents of this bag. Each element
0043: * of this list is of type JMLEqualsBagEntry.
0044: */
0045: protected final JMLEqualsBagEntryNode the_list;
0046: // in objectState;
0047:
0048: /** The size of this bag.
0049: */
0050: protected/*@ spec_public @*/final int size;
0051:
0052: // in objectState;
0053:
0054: //@ protected invariant the_list == null <==> size == 0;
0055: //@ public invariant size >= 0;
0056: /*@ protected invariant the_list != null ==>
0057: @ (\forall int i; 0 <= i && i < the_list.int_size();
0058: @ the_list.itemAt(i) instanceof JMLEqualsBagEntry);
0059: @*/
0060:
0061: //*********************** equational theory ***********************
0062: //@ public invariant (\forall Object e1; ; count(e1) >= 0);
0063: /*@ public invariant (\forall JMLEqualsBag s2; s2 != null;
0064: @ (\forall Object e1, e2; ;
0065: @ equational_theory(this, s2, e1, e2) ));
0066: @*/
0067:
0068: /** An equational specification of the properties of bags.
0069: */
0070: /*@ public normal_behavior
0071: @ {|
0072: @ // The following are defined by using has and induction.
0073: @
0074: @ ensures \result <==>
0075: @ (new JMLEqualsBag()).count(e1) == 0;
0076: @ also
0077: @ requires e1 != null;
0078: @ ensures \result <==>
0079: @ s.insert(e1).count(e2)
0080: @ == (e1.equals(e2)
0081: @ ? (s.count(e2) + 1) : s.count(e2));
0082: @ also
0083: @ ensures \result <==>
0084: @ s.insert(null).count(e2)
0085: @ == (e2 == null ? (s.count(e2) + 1) : s.count(e2));
0086: @ also
0087: @ ensures \result <==>
0088: @ (new JMLEqualsBag()).int_size() == 0;
0089: @ also
0090: @ ensures \result <==>
0091: @ s.insert(e1).int_size() == (s.int_size() + 1);
0092: @ also
0093: @ ensures \result <==>
0094: @ s.isSubbag(s2)
0095: @ == (\forall Object o; ; s.count(o) <= s2.count(o));
0096: @ also
0097: @ ensures \result <==>
0098: @ s.equals(s2) == ( s.isSubbag(s2) && s2.isSubbag(s));
0099: @ also
0100: @ ensures \result <==>
0101: @ (new JMLEqualsBag()).remove(e1).equals(new JMLEqualsBag());
0102: @ also
0103: @ ensures \result <==>
0104: @ s.insert(null).remove(e2)
0105: @ .equals
0106: @ (e2 == null ? s : s.remove(e2).insert(null));
0107: @ also
0108: @ requires e1 != null;
0109: @ ensures \result <==>
0110: @ s.insert(e1).remove(e2)
0111: @ .equals
0112: @ (e1.equals(e2)
0113: @ ? s : s.remove(e2).insert(e1));
0114: @
0115: @ // The following are all defined as abbreviations.
0116: @
0117: @ also
0118: @ ensures \result <==>
0119: @ s.isEmpty() == (s.int_size() == 0);
0120: @ also
0121: @ ensures \result <==>
0122: @ (new JMLEqualsBag()).has(e1);
0123: @ also
0124: @ ensures \result <==>
0125: @ (new JMLEqualsBag(e1)).equals(new JMLEqualsBag().insert(e1));
0126: @ also
0127: @ ensures \result <==>
0128: @ s.isProperSubbag(s2) == ( s.isSubbag(s2) && !s.equals(s2));
0129: @ also
0130: @ ensures \result <==>
0131: @ s.isSuperbag(s2) == s2.isSubbag(s);
0132: @ also
0133: @ ensures \result <==>
0134: @ s.isProperSuperbag(s2) == s2.isProperSubbag(s);
0135: @ |}
0136: @
0137: @ implies_that // other ways to specify some operations
0138: @
0139: @ ensures \result <==> (new JMLEqualsBag()).isEmpty();
0140: @
0141: @ ensures \result <==> !s.insert(e1).isEmpty();
0142: @
0143: @ ensures \result <==>
0144: @ (new JMLEqualsBag(null)).has(e2) == (e2 == null);
0145: @
0146: @ ensures \result <==>
0147: @ (e1 != null
0148: @ ==> new JMLEqualsBag(e1).has(e2)
0149: @ == (e1.equals(e2)));
0150: public pure model boolean equational_theory(JMLEqualsBag s,
0151: JMLEqualsBag s2,
0152: Object e1,
0153: Object e2);
0154: @*/// end of equational_theory
0155: //@ public invariant elementType <: \type(Object);
0156: /*@ public invariant
0157: @ (\forall Object o; o != null && has(o);
0158: @ \typeof(o) <: elementType);
0159: @*/
0160:
0161: //@ public invariant_redundantly isEmpty() ==> !containsNull;
0162: //@ public invariant owner == null;
0163: //************************* Constructors ********************************
0164: /** Initialize this bag to be empty.
0165: * @see #EMPTY
0166: */
0167: /*@ public normal_behavior
0168: @ assignable objectState, elementType, containsNull, owner;
0169: @ ensures this.isEmpty();
0170: @ ensures_redundantly (* this is an empty bag *);
0171: @
0172: @ implies_that
0173: @ ensures elementType <: \type(Object) && !containsNull;
0174: @*/
0175: public JMLEqualsBag() {
0176: the_list = null;
0177: size = 0;
0178: }
0179:
0180: /*@ public normal_behavior
0181: @ assignable objectState, elementType, containsNull, owner;
0182: @ ensures count(elem) == 1 && int_size() == 1;
0183: @ ensures_redundantly (* this is a singleton bag containing elem *);
0184: @
0185: @ implies_that
0186: @ ensures containsNull <==> elem == null;
0187: @ ensures elem != null ==> elementType == \typeof(elem);
0188: @ ensures elem == null ==> elementType <: \type(Object);
0189: @*/
0190: /** Initialize this bag to contain the given element.
0191: * @param elem the element that is the sole contents of this bag.
0192: * @see #singleton
0193: */
0194: public JMLEqualsBag(Object elem) {
0195: // cons() clones if necessary
0196: the_list = JMLEqualsBagEntryNode.cons(new JMLEqualsBagEntry(
0197: elem), null);
0198: size = 1;
0199: }
0200:
0201: /** Initialize this bag with the given representation.
0202: */
0203: /*@ requires ls == null <==> sz == 0;
0204: @ requires sz >= 0;
0205: @ assignable objectState, elementType, containsNull, owner;
0206: @ ensures elementType
0207: @ == (ls == null ? \type(Object) : ls.entryElementType);
0208: @ ensures containsNull
0209: @ == (ls == null ? false : ls.containsNullElements);
0210: @*/
0211: protected JMLEqualsBag(JMLEqualsBagEntryNode ls, int sz) {
0212: the_list = ls;
0213: size = sz;
0214: }
0215:
0216: //**************************** Static methods ****************************
0217:
0218: /** The empty JMLEqualsBag.
0219: * @see #JMLEqualsBag()
0220: */
0221: public static final/*@ non_null @*/JMLEqualsBag EMPTY = new JMLEqualsBag();
0222:
0223: /** Return the singleton bag containing the given element.
0224: * @see #JMLEqualsBag(Object)
0225: */
0226: /*@ public normal_behavior
0227: @ ensures \result != null && \result.equals(new JMLEqualsBag(e));
0228: @*/
0229: public static/*@ pure @*//*@ non_null @*/JMLEqualsBag singleton(
0230: Object e) {
0231: return new JMLEqualsBag(e);
0232: }
0233:
0234: /** Return the bag containing all the elements in the given array.
0235: */
0236: /*@ public normal_behavior
0237: @ requires a != null;
0238: @ ensures \result != null && \result.int_size() == a.length
0239: @ && (* \result contains each element in a *);
0240: @ ensures_redundantly \result != null && \result.int_size() == a.length
0241: @ && (\forall int i; 0 <= i && i < a.length; \result.has(a[i]));
0242: @*/
0243: public static/*@ pure @*//*@ non_null @*/
0244: JMLEqualsBag convertFrom(/*@ non_null @*/Object[] a) {
0245: /*@ non_null @*/JMLEqualsBag ret = EMPTY;
0246: for (int i = 0; i < a.length; i++) {
0247: ret = ret.insert(a[i]);
0248: }
0249: return ret;
0250: }
0251:
0252: /** Return the bag containing all the object in the
0253: * given collection.
0254: * @throws ClassCastException if some element in c is not an instance of
0255: * Object.
0256: * @see #containsAll(java.util.Collection)
0257: */
0258: /*@ public normal_behavior
0259: @ requires c != null
0260: @ && (c.elementType <: \type(Object));
0261: @ ensures \result != null && \result.int_size() == c.size()
0262: @ && (* \result contains each element in c *);
0263: @ ensures_redundantly \result != null && \result.int_size() == c.size()
0264: @ && (\forall Object x; c.contains(x) <==> \result.has(x));
0265: @ also
0266: @ public exceptional_behavior
0267: @ requires c != null && (\exists Object o; c.contains(o);
0268: @ !(o instanceof Object));
0269: @ signals (ClassCastException);
0270: @*/
0271: public static/*@ pure @*//*@ non_null @*/
0272: JMLEqualsBag convertFrom(/*@ non_null @*/java.util.Collection c)
0273: throws ClassCastException {
0274: /*@ non_null @*/JMLEqualsBag ret = EMPTY;
0275: java.util.Iterator celems = c.iterator();
0276: while (celems.hasNext()) {
0277: Object o = celems.next();
0278: if (o == null) {
0279: ret = ret.insert(null);
0280: } else {
0281: ret = ret.insert(o);
0282: }
0283: }
0284: return ret;
0285: }
0286:
0287: /** Return the bag containing all the object in the
0288: * given JMLCollection.
0289: * @throws ClassCastException if some element in c is not an instance of
0290: * Object.
0291: */
0292: /*@ public normal_behavior
0293: @ requires c != null
0294: @ && (c.elementType <: \type(Object));
0295: @ ensures \result != null
0296: @ && (\forall Object x; c.has(x) <==> \result.has(x));
0297: @ ensures_redundantly \result.int_size() == c.int_size();
0298: @ also
0299: @ public exceptional_behavior
0300: @ requires c != null && (\exists Object o; c.has(o);
0301: @ !(o instanceof Object));
0302: @ signals (ClassCastException);
0303: @*/
0304: public static/*@ pure @*//*@ non_null @*/
0305: JMLEqualsBag convertFrom(/*@ non_null @*/JMLCollection c)
0306: throws ClassCastException {
0307: /*@ non_null @*/JMLEqualsBag ret = EMPTY;
0308: JMLIterator celems = c.iterator();
0309: while (celems.hasNext()) {
0310: Object o = celems.next();
0311: if (o == null) {
0312: ret = ret.insert(null);
0313: } else {
0314: ret = ret.insert(o);
0315: }
0316: }
0317: return ret;
0318: }
0319:
0320: //**************************** Observers **********************************
0321:
0322: /** Tell how many times the given element occurs ".equals"
0323: * to an element in this bag.
0324: * @param elem the element sought.
0325: * @return the number of times elem occurs in this bag.
0326: * @see #has(Object)
0327: */
0328: /*@
0329: @ public normal_behavior
0330: @ ensures \result >= 0
0331: @ && (* \result is the number of times elem occurs in this *);
0332: @*/
0333: //@ implies_that
0334: //@ ensures \result >= 0;
0335: public int count(Object elem) {
0336: JMLEqualsBagEntry matchingEntry = getMatchingEntry(elem);
0337: if (matchingEntry != null) {
0338: return matchingEntry.count;
0339: } else {
0340: // there is no matching item in the list.
0341: return 0;
0342: }
0343: }
0344:
0345: /** Tell whether the given element occurs ".equals"
0346: * to an element in this bag.
0347: * @param elem the element sought.
0348: * @see #count(Object)
0349: */
0350: /*@ also
0351: @ public normal_behavior
0352: @ ensures \result <==> (count(elem) > 0);
0353: @*/
0354: public boolean has(Object elem) {
0355: return the_list != null
0356: && the_list.has(new JMLEqualsBagEntry(elem));
0357: }
0358:
0359: /** Tell whether, for each element in the given collection, there is a
0360: * ".equals" element in this bag.
0361: * @param c the collection whose elements are sought.
0362: * @see #isSuperbag(JMLEqualsSet)
0363: * @see #convertFrom(java.util.Collection)
0364: */
0365: /*@ public normal_behavior
0366: @ requires c != null;
0367: @ ensures \result <==> (\forall Object o; c.contains(o); this.has(o));
0368: @*/
0369: public boolean containsAll(/*@ non_null @*/java.util.Collection c) {
0370: java.util.Iterator celems = c.iterator();
0371: while (celems.hasNext()) {
0372: Object o = celems.next();
0373: if (!has(o)) {
0374: return false;
0375: }
0376: }
0377: return true;
0378: }
0379:
0380: /** Test whether this object's value is equal to the given argument.
0381: * This comparison uses ".equals" to compare elements.
0382: *
0383: * <p>Note that the <kbd>elementType</kbd>s may be different for
0384: * otherwise equal bags.
0385: */
0386: /*@ also
0387: @ public normal_behavior
0388: @ ensures \result <==>
0389: @ b2 != null && b2 instanceof JMLEqualsBag
0390: @ && (\forall Object e; ;
0391: @ this.count(e) == ((JMLEqualsBag)b2).count(e));
0392: @*/
0393: /*@ implies_that
0394: @ public normal_behavior
0395: @ requires b2 != null && b2 instanceof JMLEqualsBag;
0396: @ ensures \result ==>
0397: @ this.int_size() == ((JMLEqualsBag)b2).int_size()
0398: @ && containsNull == ((JMLEqualsBag)b2).containsNull;
0399: @*/
0400: public boolean equals(Object b2) {
0401: return b2 != null && b2 instanceof JMLEqualsBag
0402: && (size == ((JMLEqualsBag) b2).int_size())
0403: && isSubbag((JMLEqualsBag) b2);
0404: }
0405:
0406: /** Return a hash code for this object
0407: */
0408: public/*@ pure @*/int hashCode() {
0409: return the_list == null ? 0 : the_list.hashCode();
0410: }
0411:
0412: /** Tell whether this bag has no elements.
0413: * @see #int_size()
0414: * @see #has(Object)
0415: */
0416: /*@ public normal_behavior
0417: @ ensures \result == (\forall Object e; ; count(e) == 0);
0418: @*/
0419: public boolean isEmpty() {
0420: return the_list == null;
0421: }
0422:
0423: /** Tell the number of elements in this bag.
0424: */
0425: /*@ also
0426: @ public normal_behavior
0427: @ ensures \result >= 0 && (* \result is the size of this bag *);
0428: @*/
0429: public int int_size() {
0430: return size;
0431: }
0432:
0433: /** Tells whether every item in this bag is contained in the argument.
0434: * @see #isProperSubbag(JMLEqualsBag)
0435: * @see #isSuperbag(JMLEqualsBag)
0436: */
0437: /*@ public normal_behavior
0438: @ requires b2 != null;
0439: @ ensures \result <==>
0440: @ (\forall Object e; ; count(e) <= b2.count(e));
0441: @*/
0442: public boolean isSubbag(/*@ non_null @*/JMLEqualsBag b2) {
0443: if (size > b2.int_size()) {
0444: return false;
0445: } else {
0446: for (JMLListValueNode walker = the_list; walker != null; walker = walker.next) {
0447: JMLEqualsBagEntry entry = (JMLEqualsBagEntry) walker.val;
0448: if (entry.count > b2.count(entry.theElem)) {
0449: return false;
0450: }
0451: }
0452: return true;
0453: }
0454: }
0455:
0456: /** Tells whether every item in this bag is contained in the
0457: * argument, but the argument is strictly larger.
0458: * @see #isSubbag(JMLEqualsBag)
0459: * @see #isProperSuperbag(JMLEqualsBag)
0460: */
0461: /*@ public normal_behavior
0462: @ requires b2 != null;
0463: @ ensures \result <==>
0464: @ this.isSubbag(b2) && !this.equals(b2);
0465: @*/
0466: public boolean isProperSubbag(/*@ non_null @*/JMLEqualsBag b2) {
0467: return size < b2.int_size() && isSubbag(b2);
0468: }
0469:
0470: /** Tells whether every item in the argument is contained in this bag.
0471: * @see #isProperSuperbag(JMLEqualsBag)
0472: * @see #isSubbag(JMLEqualsBag)
0473: * @see #containsAll(java.util.Collection)
0474: */
0475: /*@ public normal_behavior
0476: @ requires b2 != null;
0477: @ ensures \result == b2.isSubbag(this);
0478: @*/
0479: public boolean isSuperbag(/*@ non_null @*/JMLEqualsBag b2) {
0480: return b2.isSubbag(this );
0481: }
0482:
0483: /** Tells whether every item in the argument is contained in this bag
0484: * argument, but this bag is strictly larger.
0485: * @see #isSuperbag(JMLEqualsBag)
0486: * @see #isProperSubbag(JMLEqualsBag)
0487: */
0488: /*@ public normal_behavior
0489: @ requires b2 != null;
0490: @ ensures \result == b2.isProperSubbag(this);
0491: @*/
0492: public boolean isProperSuperbag(/*@ non_null @*/JMLEqualsBag b2) {
0493: return b2.isProperSubbag(this );
0494: }
0495:
0496: /** Return an arbitrary element of this.
0497: * @exception JMLNoSuchElementException if this is empty.
0498: * @see #isEmpty()
0499: * @see #elements()
0500: */
0501: /*@ public normal_behavior
0502: @ requires !isEmpty();
0503: @ ensures (\exists Object e; this.has(e);
0504: @ \result.equals(e));
0505: @ also
0506: @ public exceptional_behavior
0507: @ requires isEmpty();
0508: @ signals (JMLNoSuchElementException);
0509: @
0510: @ implies_that
0511: @ ensures \result != null ==> \typeof(\result) <: elementType;
0512: @ ensures !containsNull ==> \result != null;
0513: @ signals (JMLNoSuchElementException) size == 0;
0514: @*/
0515: public Object choose() throws JMLNoSuchElementException {
0516: if (the_list != null) {
0517: JMLEqualsBagEntry entry = (JMLEqualsBagEntry) the_list.val;
0518: Object elt = entry.theElem;
0519: if (elt == null) {
0520: return null;
0521: } else {
0522: Object o = elt;
0523: return (Object) o;
0524: }
0525: } else {
0526: throw new JMLNoSuchElementException("Tried to .choose() "
0527: + "with JMLEqualsBag empty");
0528: }
0529: }
0530:
0531: // ******************** building new JMLEqualsBags **********************
0532:
0533: /** Return a clone of this object. This method does not clone the
0534: * elements of the bag.
0535: */
0536: /*@ also
0537: @ public normal_behavior
0538: @ ensures \result instanceof JMLEqualsBag && this.equals(\result);
0539: @ ensures_redundantly \result != null;
0540: @*/
0541: public Object clone() {
0542: return this ;
0543: }
0544:
0545: /** Find a JMLEqualsBagEntry that is for the same element, if possible.
0546: * @param item the item sought.
0547: * @return null if the item is not in the bag.
0548: */
0549: /*@ assignable \nothing;
0550: @ ensures the_list == null ==> \result == null;
0551: @ ensures_redundantly \result != null ==> the_list != null;
0552: @ ensures \result != null
0553: @ ==> 0 <= \result.count && \result.count <= size;
0554: @*/
0555: protected JMLEqualsBagEntry getMatchingEntry(Object item) {
0556: JMLEqualsBagEntry currEntry = null;
0557: JMLListValueNode ptr = this .the_list;
0558: //@ maintaining (* no earlier element matches item *);
0559: while (ptr != null) {
0560: currEntry = (JMLEqualsBagEntry) ptr.val;
0561: if (currEntry.equalElem(item)) {
0562: return currEntry;
0563: }
0564: ptr = ptr.next;
0565: }
0566: return null;
0567: }
0568:
0569: /** Return a bag containing the given item and the ones in
0570: * this bag.
0571: * @see #insert(Object, int)
0572: * @see #has(Object)
0573: * @see #remove(Object)
0574: */
0575: /*@
0576: @ public normal_behavior
0577: @ requires size < Integer.MAX_VALUE;
0578: @ {|
0579: @ requires elem != null;
0580: @ ensures \result != null
0581: @ && (\forall Object e; ;
0582: @ ( (e.equals(elem))
0583: @ ==> \result.count(e) == count(e) + 1 )
0584: @ && ( !(e.equals(elem))
0585: @ ==> \result.count(e) == count(e) ));
0586: @ also
0587: @ requires elem == null;
0588: @ ensures \result != null
0589: @ && (\forall Object e; ;
0590: @ ( e == null
0591: @ ==> \result.count(e) == count(e) + 1 )
0592: @ && (e != null
0593: @ ==> \result.count(e) == count(e) ));
0594: @ |}
0595: @*/
0596: public/*@ non_null @*/JMLEqualsBag insert(Object elem)
0597: throws IllegalStateException {
0598: return insert(elem, 1);
0599: }
0600:
0601: /** Return a bag containing the given item the given number of
0602: * times, in addition to the ones in this bag.
0603: * @see #insert(Object)
0604: * @see #has(Object)
0605: * @see #remove(Object, int)
0606: */
0607: /*@
0608: @ public normal_behavior
0609: @ requires cnt > 0;
0610: @ requires size <= Integer.MAX_VALUE - cnt;
0611: @ {|
0612: @ requires elem != null;
0613: @ ensures \result != null
0614: @ && (\forall Object e; ;
0615: @ ( (e != null && e.equals(elem))
0616: @ ==> \result.count(e) == count(e) + cnt )
0617: @ && ( e == null || !(e.equals(elem))
0618: @ ==> \result.count(e) == count(e) ));
0619: @ also
0620: @ requires elem == null;
0621: @ ensures \result != null
0622: @ && (\forall Object e; ;
0623: @ ( e == null ==> \result.count(e) == count(e) + cnt )
0624: @ && ( e != null ==> \result.count(e) == count(e) ));
0625: @ |}
0626: @ also
0627: @ public normal_behavior
0628: @ requires cnt == 0;
0629: @ ensures \result != null && \result.equals(this);
0630: @ also
0631: @ signals (IllegalArgumentException) cnt < 0;
0632: @*/
0633: public/*@ non_null @*/JMLEqualsBag insert(Object elem, int cnt)
0634: throws IllegalArgumentException, IllegalStateException {
0635: if (cnt < 0) {
0636: throw new IllegalArgumentException(
0637: "insert called with negative count");
0638: }
0639: if (cnt == 0) {
0640: return this ;
0641: }
0642: if (!(size <= Integer.MAX_VALUE - cnt)) {
0643: throw new IllegalStateException(
0644: "Bag too big to insert into");
0645: }
0646:
0647: JMLEqualsBagEntry entry = null;
0648: JMLEqualsBagEntryNode new_list = the_list;
0649: JMLEqualsBagEntry matchingEntry = getMatchingEntry(elem);
0650: if (matchingEntry != null) {
0651: entry = new JMLEqualsBagEntry(matchingEntry.theElem,
0652: matchingEntry.count + cnt);
0653: JMLListValueNode nl = the_list.removeBE(matchingEntry);
0654: if (nl == null) {
0655: new_list = null;
0656: } else {
0657: new_list = (JMLEqualsBagEntryNode) nl;
0658: }
0659: } else {
0660: // there is no matching item in the list.
0661: entry = new JMLEqualsBagEntry(elem, cnt);
0662: }
0663: // cons() clones if necessary
0664: return new JMLEqualsBag(JMLEqualsBagEntryNode.cons(entry,
0665: new_list), size + cnt);
0666: }
0667:
0668: /** Return a bag containing the items in this bag except for
0669: * one of the given element.
0670: * @see #remove(Object, int)
0671: * @see #insert(Object)
0672: */
0673: /*@ public normal_behavior
0674: @ {|
0675: @ requires elem != null;
0676: @ ensures \result != null
0677: @ && (\forall Object e; ;
0678: @ ( (e.equals(elem) && has(e))
0679: @ ==> \result.count(e) == count(e) - 1 )
0680: @ && ( !(e.equals(elem))
0681: @ ==> \result.count(e) == count(e) ));
0682: @ also
0683: @ requires elem == null;
0684: @ ensures \result != null
0685: @ && (\forall Object e; ;
0686: @ ( e == null
0687: @ ==> \result.count(e) == count(e) - 1 )
0688: @ && (e != null
0689: @ ==> \result.count(e) == count(e) ));
0690: @ |}
0691: @*/
0692: public/*@ non_null @*/JMLEqualsBag remove(Object elem) {
0693: return remove(elem, 1);
0694: }
0695:
0696: /** Return a bag containing the items in this bag, except for
0697: * the given number of the given element.
0698: * @see #remove(Object)
0699: * @see #insert(Object, int)
0700: */
0701: /*@ public normal_behavior
0702: @ requires cnt > 0;
0703: @ {|
0704: @ requires elem != null;
0705: @ ensures \result != null
0706: @ && (\forall Object e; ;
0707: @ ( (e.equals(elem) && has(e))
0708: @ ==> \result.count(e) == JMLMath.max(0, count(e) - cnt) )
0709: @ && ( !(e.equals(elem))
0710: @ ==> \result.count(e) == count(e) ));
0711: @ also
0712: @ requires elem == null;
0713: @ ensures \result != null
0714: @ && (\forall Object e; ;
0715: @ ( e == null
0716: @ ==> \result.count(e) == JMLMath.max(0, count(e) - cnt) )
0717: @ && (e != null
0718: @ ==> \result.count(e) == count(e) ));
0719: @ |}
0720: @ also
0721: @ public normal_behavior
0722: @ requires cnt == 0;
0723: @ ensures \result != null && \result.equals(this);
0724: @ also
0725: @ signals (IllegalArgumentException) cnt < 0;
0726: @ implies_that
0727: @ requires 0 <= cnt;
0728: @*/
0729: public/*@ non_null @*/JMLEqualsBag remove(Object elem, int cnt)
0730: throws IllegalArgumentException {
0731: if (cnt < 0) {
0732: throw new IllegalArgumentException(
0733: "remove called with negative count");
0734: }
0735: if (cnt == 0) {
0736: return this ;
0737: }
0738:
0739: JMLEqualsBagEntry entry = null;
0740: JMLEqualsBagEntryNode new_list = the_list;
0741: JMLEqualsBagEntry matchingEntry = getMatchingEntry(elem);
0742: if (matchingEntry != null) {
0743: JMLListValueNode nl = the_list.removeBE(matchingEntry);
0744: if (nl == null) {
0745: new_list = null;
0746: } else {
0747: new_list = (JMLEqualsBagEntryNode) nl;
0748: }
0749: if ((matchingEntry.count - cnt) > 0) {
0750: entry = new JMLEqualsBagEntry(matchingEntry.theElem,
0751: matchingEntry.count - cnt);
0752: // cons() clones if necessary
0753: return new JMLEqualsBag(JMLEqualsBagEntryNode.cons(
0754: entry, new_list), size - cnt);
0755: } else {
0756: return new JMLEqualsBag(new_list, size
0757: - matchingEntry.count);
0758: }
0759: } else {
0760: // there is no matching item in the list.
0761: return this ;
0762: }
0763: }
0764:
0765: /** Return a bag containing the items in this bag, except for
0766: * all items that are ".equals" to the given item.
0767: * @see #remove(Object)
0768: * @see #remove(Object, int)
0769: */
0770: /*@ public normal_behavior
0771: @ requires elem != null;
0772: @ ensures \result != null
0773: @ && (\forall Object e; ;
0774: @ ( (e.equals(elem) && has(e))
0775: @ ==> \result.count(e) == 0 )
0776: @ && ( !(e.equals(elem))
0777: @ ==> \result.count(e) == count(e) ));
0778: @ also
0779: @ public normal_behavior
0780: @ requires elem == null;
0781: @ ensures \result != null
0782: @ && (\forall Object e; ;
0783: @ ( e == null
0784: @ ==> \result.count(e) == 0 )
0785: @ && (e != null
0786: @ ==> \result.count(e) == count(e) ));
0787: @*/
0788: public/*@ non_null @*/JMLEqualsBag removeAll(Object elem) {
0789: JMLEqualsBagEntry matchingEntry = getMatchingEntry(elem);
0790: if (matchingEntry != null) {
0791: JMLListValueNode nl = the_list.removeBE(matchingEntry);
0792: JMLEqualsBagEntryNode new_list;
0793: if (nl == null) {
0794: new_list = null;
0795: } else {
0796: new_list = (JMLEqualsBagEntryNode) nl;
0797: }
0798: return new JMLEqualsBag(new_list, size
0799: - matchingEntry.count);
0800: } else {
0801: // there is no matching item in the list.
0802: return this ;
0803: }
0804: }
0805:
0806: /** Return a bag containing the items in both this bag and the
0807: * given bag. Note that items occur the minimum number of times they
0808: * occur in both bags.
0809: * @see #union(JMLEqualsBag)
0810: * @see #difference(JMLEqualsBag)
0811: */
0812: /*@ public normal_behavior
0813: @ requires b2 != null;
0814: @ ensures \result != null
0815: @ && (\forall Object e; ;
0816: @ \result.count(e) == Math.min(count(e), b2.count(e)));
0817: @*/
0818: public/*@ non_null @*/
0819: JMLEqualsBag intersection(/*@ non_null @*/JMLEqualsBag b2) {
0820: JMLEqualsBagEntryNode newList = null;
0821: JMLEqualsBagEntry newEntry;
0822: int othCount, newCount;
0823: int newSize = 0;
0824: JMLListValueNode this Walker = the_list;
0825: while (this Walker != null) {
0826: JMLEqualsBagEntry currEntry = (JMLEqualsBagEntry) this Walker.val;
0827: othCount = b2.count(currEntry.theElem);
0828: newCount = Math.min(othCount, currEntry.count);
0829: if (newCount >= 1) {
0830: newEntry = new JMLEqualsBagEntry(currEntry.theElem,
0831: newCount);
0832: newList = new JMLEqualsBagEntryNode(newEntry, newList);
0833: newSize += newCount;
0834: }
0835: this Walker = this Walker.next;
0836: }
0837: return new JMLEqualsBag(newList, newSize);
0838: }
0839:
0840: /** Return a bag containing the items in either this bag or the
0841: * given bag. Note that items occur the sum of times they
0842: * occur in both bags.
0843: * @see #intersection(JMLEqualsBag)
0844: * @see #difference(JMLEqualsBag)
0845: */
0846: /*@ public normal_behavior
0847: @ requires size < Integer.MAX_VALUE - b2.size;
0848: @ requires b2 != null;
0849: @ ensures \result != null
0850: @ && (\forall Object e; ;
0851: @ \result.count(e) == (count(e) + b2.count(e)));
0852: @*/
0853: public/*@ non_null @*/
0854: JMLEqualsBag union(/*@ non_null @*/JMLEqualsBag b2) {
0855: JMLEqualsBagEntryNode newList = null;
0856: JMLEqualsBagEntry newEntry;
0857: int othCount, newCount;
0858: JMLListValueNode this Walker = the_list;
0859: while (this Walker != null) {
0860: JMLEqualsBagEntry currEntry = (JMLEqualsBagEntry) this Walker.val;
0861: othCount = b2.count(currEntry.theElem);
0862: newCount = currEntry.count + othCount;
0863: newEntry = new JMLEqualsBagEntry(currEntry.theElem,
0864: newCount);
0865: newList = new JMLEqualsBagEntryNode(newEntry, newList);
0866: this Walker = this Walker.next;
0867: }
0868: JMLListValueNode othWalker = b2.the_list;
0869: while (othWalker != null) {
0870: JMLEqualsBagEntry currEntry = (JMLEqualsBagEntry) othWalker.val;
0871: if (the_list == null || !the_list.has(currEntry)) {
0872: newList = new JMLEqualsBagEntryNode(currEntry, newList);
0873: }
0874: othWalker = othWalker.next;
0875: }
0876: return new JMLEqualsBag(newList, size + b2.size);
0877: }
0878:
0879: /** Return a bag containing the items in this bag minus the
0880: * items in the given bag. If an item occurs in this bag N times,
0881: * and M times in the given bag, then it occurs N-M times in the result.
0882: * @see #union(JMLEqualsBag)
0883: * @see #difference(JMLEqualsBag)
0884: */
0885: /*@ public normal_behavior
0886: @ requires b2 != null;
0887: @ ensures \result != null
0888: @ && (\forall Object e; ;
0889: @ \result.count(e) == JMLMath.max(0, count(e) - b2.count(e)));
0890: @*/
0891: public/*@ non_null @*/JMLEqualsBag difference(
0892: /*@ non_null @*/JMLEqualsBag b2) {
0893: JMLEqualsBagEntryNode newList = null;
0894: JMLEqualsBagEntry newEntry;
0895: int othCount, newCount;
0896: int newSize = 0;
0897: JMLListValueNode this Walker = the_list;
0898: while (this Walker != null) {
0899: JMLEqualsBagEntry currEntry = (JMLEqualsBagEntry) this Walker.val;
0900: othCount = b2.count(currEntry.theElem);
0901: newCount = Math.max(0, currEntry.count - othCount);
0902: if (newCount >= 1) {
0903: newEntry = new JMLEqualsBagEntry(currEntry.theElem,
0904: newCount);
0905: newList = new JMLEqualsBagEntryNode(newEntry, newList);
0906: newSize += newCount;
0907: }
0908: this Walker = this Walker.next;
0909: }
0910: return new JMLEqualsBag(newList, newSize);
0911: }
0912:
0913: /** Return a new JMLEqualsSequence containing all the elements of this.
0914: * @see #toArray()
0915: * @see #toSet()
0916: */
0917: /*@ public normal_behavior
0918: @ ensures \result != null
0919: @ && (\forall Object o;; \result.count(o) == this.count(o));
0920: @*/
0921: public /*@ non_null @*/ JMLEqualsSequence toSequence() {
0922: JMLEqualsSequence ret = new JMLEqualsSequence();
0923: JMLEqualsBagEnumerator enum = elements();
0924: while (enum.hasMoreElements()) {
0925: Object o = enum.nextElement();
0926: Object e = (o == null ? null : o);
0927: ret = ret.insertFront(e);
0928: }
0929: return ret;
0930: }
0931:
0932: /** Return a new JMLEqualsSet containing all the elements of this.
0933: * @see #toSequence()
0934: */
0935: /*@ public normal_behavior
0936: @ ensures \result != null
0937: @ && (\forall Object o;; \result.has(o) == this.has(o));
0938: @*/
0939: public /*@ non_null @*/ JMLEqualsSet toSet() {
0940: JMLEqualsSet ret = new JMLEqualsSet();
0941: JMLEqualsBagEnumerator enum = elements();
0942: while (enum.hasMoreElements()) {
0943: Object o = enum.nextElement();
0944: Object e = (o == null ? null : o);
0945: ret = ret.insert(e);
0946: }
0947: return ret;
0948: }
0949: /** Return a new array containing all the elements of this.
0950: * @see #toSequence()
0951: */
0952: /*@ public normal_behavior
0953: @ ensures \result != null && \result.length == int_size()
0954: @ && (\forall Object o;;
0955: @ JMLArrayOps.valueEqualsCount(\result, o) == count(o));
0956: @ ensures_redundantly \result != null && \result.length == int_size()
0957: @ && (\forall int i; 0 <= i && i < \result.length;
0958: @ JMLArrayOps.valueEqualsCount(\result, \result[i])
0959: @ == count(\result[i]));
0960: @*/
0961: public /*@ non_null @*/ Object[] toArray() {
0962: Object[] ret = new Object[int_size()];
0963: JMLEqualsBagEnumerator enum = elements();
0964: int i = 0;
0965: //@ loop_invariant 0 <= i && i <= ret.length;
0966: while (enum.hasMoreElements()) {
0967: Object o = enum.nextElement();
0968: if (o == null) {
0969: ret[i] = null;
0970: } else {
0971: Object e = o;
0972: ret[i] = e;
0973: }
0974: i++;
0975: }
0976: return ret;
0977: }
0978:
0979: // ********************* Tools Methods *********************************
0980: // The enumerator method and toString are of no value for writing
0981: // assertions in JML. They are included for the use of developers
0982: // of CASE tools based on JML, e.g., type checkers, assertion
0983: // evaluators, prototype generators, test tools, ... . They can
0984: // also be used in model programs in specifications.
0985:
0986: /** Returns an Enumeration over this bag.
0987: * @see #iterator()
0988: */
0989: /*@ public normal_behavior
0990: @ ensures \fresh(\result) && this.equals(\result.uniteratedElems);
0991: @*/
0992: public/*@ non_null @*/JMLEqualsBagEnumerator elements() {
0993: return new JMLEqualsBagEnumerator(this );
0994: }
0995:
0996: /** Returns an iterator over this bag.
0997: * @see #elements()
0998: */
0999: /*@ also
1000: @ public normal_behavior
1001: @ ensures \fresh(\result)
1002: @ && \result.equals(new JMLEnumerationToIterator(elements()));
1003: @*/
1004: public JMLIterator iterator() {
1005: return new JMLEnumerationToIterator(elements());
1006: }
1007:
1008: /** Return a string representation of this object.
1009: */
1010: /*@ also
1011: @ public normal_behavior
1012: @ ensures (* \result is a string representation of this *);
1013: @*/
1014: public String toString() {
1015: String newStr = new String("{");
1016: JMLListValueNode bagWalker = the_list;
1017:
1018: if (bagWalker != null) {
1019: newStr = newStr + bagWalker.val;
1020: bagWalker = bagWalker.next;
1021: }
1022: while (bagWalker != null) {
1023: newStr = newStr + ", " + bagWalker.val;
1024: bagWalker = bagWalker.next;
1025: }
1026: newStr = newStr + "}";
1027: return newStr;
1028: }
1029:
1030: } // end of class JMLEqualsBag
1031:
1032: /** Internal class used in the implementation of JMLEqualsBag.
1033: *
1034: * @author Gary T. Leavens
1035: * @see JMLEqualsBag
1036: * @see JMLEqualsBagEntryNode
1037: */
1038: /*@ pure spec_public @*/class JMLEqualsBagEntry implements JMLType {
1039:
1040: /** The element in this bag entry.
1041: */
1042: public final Object theElem;
1043:
1044: /** The number of times the element occurs.
1045: */
1046: public final int count;
1047:
1048: //@ public invariant count > 0;
1049:
1050: /** The type of the element in this entry. This is Object if
1051: * the element is null.
1052: */
1053: //@ ghost public Object elementType;
1054: //@ public invariant elementType <: \type(Object);
1055: /*@ public
1056: @ invariant (theElem == null ==> elementType == \type(Object))
1057: @ && (theElem != null ==> elementType == \typeof(theElem));
1058: @*/
1059:
1060: //@ public invariant owner == null;
1061: /** Initialize this object to be a singleton entry.
1062: */
1063: /*@ public normal_behavior
1064: @ assignable theElem, count, elementType, owner;
1065: @ ensures theElem == e && count == 1;
1066: @*/
1067: public JMLEqualsBagEntry(Object e) {
1068: theElem = e;
1069: count = 1;
1070: }
1071:
1072: /** Initialize this object to be for the given element with the
1073: * given number of repetitions.
1074: */
1075: /*@ public normal_behavior
1076: @ requires cnt > 0;
1077: @ assignable theElem, count, elementType, owner;
1078: @ ensures count == cnt && (e == null ==> theElem == null);
1079: @ ensures (e != null ==> e.equals(theElem));
1080: @*/
1081: public JMLEqualsBagEntry(Object e, int cnt) {
1082: theElem = e;
1083: count = cnt;
1084: }
1085:
1086: /** Make a clone of the given entry.
1087: */
1088: public Object clone() {
1089: return this ;
1090: }
1091:
1092: /** Are these elements equal? */
1093: /*@ public normal_behavior
1094: @ ensures \result <==>
1095: @ (othElem == null && theElem == null)
1096: @ || (othElem != null && othElem.equals(theElem));
1097: @*/
1098: public boolean equalElem(Object othElem) {
1099: return (othElem == null && theElem == null)
1100: || (othElem != null && othElem.equals(theElem));
1101: }
1102:
1103: /** Test whether this object's value is equal to the given argument.
1104: */
1105: public boolean equals(Object obj) {
1106: if (obj != null && obj instanceof JMLEqualsBagEntry) {
1107: JMLEqualsBagEntry oth = (JMLEqualsBagEntry) obj;
1108: return equalElem(oth.theElem);
1109: } else {
1110: return (false);
1111: }
1112: }
1113:
1114: /** Return a hash code for this object.
1115: */
1116: public int hashCode() {
1117: return theElem == null ? 0 : theElem.hashCode();
1118: }
1119:
1120: /** Return a new bag entry with the same element as this but with
1121: * the given number of repetitions added to the element's current
1122: * count.
1123: */
1124: /*@ public normal_behavior
1125: @ requires numInserted > 0;
1126: @ ensures \result != null && \result.count == count + numInserted;
1127: @ ensures \result != null && \result.theElem.equals(theElem);
1128: @*/
1129: public JMLEqualsBagEntry insert(int numInserted) {
1130: return new JMLEqualsBagEntry(theElem, count + numInserted);
1131: }
1132:
1133: /** Return a string representation of this object.
1134: */
1135: public String toString() {
1136: if (count == 1) {
1137: return theElem + "";
1138: } else {
1139: return count + " copies of " + theElem;
1140: }
1141: }
1142:
1143: }
1144:
1145: /** Internal class used in the implementation of JMLEqualsBag.
1146: *
1147: * @author Gary T. Leavens
1148: * @see JMLEqualsBag
1149: * @see JMLEqualsBagEntry
1150: * @see JMLListValueNode
1151: */
1152: /*@ pure spec_public @*/class JMLEqualsBagEntryNode extends
1153: JMLListValueNode {
1154:
1155: //@ public invariant elementType == \type(JMLEqualsBagEntry) && !containsNull;
1156:
1157: //@ public invariant val != null && val instanceof JMLEqualsBagEntry;
1158:
1159: //@ public invariant next != null ==> next instanceof JMLEqualsBagEntryNode;
1160:
1161: /** The type of the elements contained in the entries in this list.
1162: */
1163: //@ ghost public Object entryElementType;
1164: //@ public constraint entryElementType == \old(entryElementType);
1165: //@ public invariant entryElementType <: \type(Object);
1166: /*@ public invariant
1167: @ val != null && val instanceof JMLEqualsBagEntry
1168: @ && ((JMLEqualsBagEntry)val).elementType <: entryElementType;
1169: @ public invariant
1170: @ (next != null
1171: @ ==> ((JMLEqualsBagEntryNode)next).entryElementType
1172: @ <: entryElementType);
1173: @ public invariant
1174: @ containsNullElements ==> entryElementType == \type(Object);
1175: @*/
1176:
1177: /** Whether this list can contain null elements in its bag entries;
1178: */
1179: //@ ghost public boolean containsNullElements;
1180: //@ public constraint containsNullElements == \old(containsNullElements);
1181: /*@ protected
1182: @ invariant containsNullElements <==>
1183: @ ((JMLEqualsBagEntry)val).theElem == null
1184: @ || (next != null
1185: @ && ((JMLEqualsBagEntryNode)next).containsNullElements);
1186: @*/
1187:
1188: /** Initialize this list to have the given bag entry as its first
1189: * element followed by the given list.
1190: * This does not do any cloning.
1191: *
1192: * @param entry the JMLEqualsBagEntry to place at the head of this list.
1193: * @param nxt the JMLEqualsBagEntryNode to make the tail of this list.
1194: * @see #cons
1195: */
1196: /*@ public normal_behavior
1197: @ requires entry != null;
1198: @ assignable val, next, elementType, containsNull, owner;
1199: @ assignable entryElementType, containsNullElements;
1200: @ ensures val.equals(entry);
1201: @*/
1202: /*@ ensures next == nxt;
1203: @ ensures entryElementType
1204: @ == (nxt == null ? entry.elementType
1205: @ : (nxt.entryElementType <: entry.elementType
1206: @ ? entry.elementType
1207: @ : ((entry.elementType <: nxt.entryElementType)
1208: @ ? nxt.entryElementType
1209: @ : \type(Object))));
1210: @ ensures containsNullElements
1211: @ == (((JMLEqualsBagEntry)val).theElem == null
1212: @ || (next != null
1213: @ && ((JMLEqualsBagEntryNode)next)
1214: @ .containsNullElements));
1215: @*/
1216: public JMLEqualsBagEntryNode(
1217: /*@ non_null @*/JMLEqualsBagEntry entry,
1218: JMLEqualsBagEntryNode nxt) {
1219: super (entry, nxt);
1220: }
1221:
1222: /** Return a JMLEqualsBagEntryNode containing the given entry
1223: * followed by the given list.
1224: *
1225: * This method handles any necessary cloning for value lists
1226: * and it handles inserting null elements.
1227: *
1228: * @param hd the JMLEqualsBagEntry to place at the head of the result.
1229: * @param tl the JMLEqualsBagEntryNode to make the tail of the result.
1230: * @see #JMLEqualsBagEntryNode
1231: */
1232: /*@ public normal_behavior
1233: @ requires hd != null;
1234: @ ensures \result != null
1235: @ && \result.headEquals(hd) && \result.next == tl;
1236: @ ensures \result.equals(new JMLEqualsBagEntryNode(hd, tl));
1237: @ implies_that
1238: @ requires hd != null;
1239: @ ensures tl == null <==> \result.next == null;
1240: @ ensures \result != null && \result.val instanceof JMLEqualsBagEntry
1241: @ && \result.entryElementType
1242: @ == (\result.next == null
1243: @ ? ((JMLEqualsBagEntry)\result.val).elementType
1244: @ : (((JMLEqualsBagEntryNode)\result.next)
1245: @ .entryElementType
1246: @ <: ((JMLEqualsBagEntry)\result.val).elementType
1247: @ ? ((JMLEqualsBagEntry)\result.val).elementType
1248: @ : ((((JMLEqualsBagEntry)\result.val).elementType
1249: @ <: ((JMLEqualsBagEntryNode)\result.next)
1250: @ .entryElementType)
1251: @ ? ((JMLEqualsBagEntryNode)\result.next)
1252: @ .entryElementType
1253: @ : \type(Object))));
1254: @ ensures \result != null
1255: @ && \result.containsNullElements
1256: @ == (((JMLEqualsBagEntry)\result.val).theElem == null
1257: @ || (\result.next != null
1258: @ && ((JMLEqualsBagEntryNode)\result.next)
1259: @ .containsNullElements));
1260: @*/
1261: public static/*@ pure @*//*@ non_null @*/
1262: JMLEqualsBagEntryNode cons(/*@ non_null @*/JMLEqualsBagEntry hd,
1263: JMLEqualsBagEntryNode tl) {
1264: return new JMLEqualsBagEntryNode(
1265: (JMLEqualsBagEntry) hd.clone(), tl);
1266: }
1267:
1268: /** Return a clone of this object.
1269: */
1270: /*@ also
1271: @ public normal_behavior
1272: @ ensures \result != null
1273: @ && \result instanceof JMLEqualsBagEntryNode
1274: @ && ((JMLEqualsBagEntryNode)\result).equals(this);
1275: @*/
1276: public Object clone() {
1277: // Recall that cons() handles cloning.
1278: return cons(val, (next == null ? null
1279: : (JMLEqualsBagEntryNode) next.clone()));
1280: }
1281:
1282: /** Return a list that is like this list but without the first
1283: * occurrence of the given bag entry.
1284: */
1285: /*@ public normal_behavior
1286: @ requires !has(entry);
1287: @ ensures this.equals(\result);
1288: @ also
1289: @ public normal_behavior
1290: @ old int index = indexOf(entry);
1291: @ requires has(entry);
1292: @ ensures \result == null <==> \old(int_size() == 1);
1293: @ ensures \result != null && index == 0
1294: @ ==> \result.equals(removePrefix(1));
1295: @ ensures \result != null && index > 0
1296: @ ==> \result.equals(prefix(index).concat(removePrefix((int)(index+1))));
1297: @*/
1298: public JMLEqualsBagEntryNode removeBE(
1299: /*@ non_null @*/JMLEqualsBagEntry entry) {
1300: if (entry.equals(val)) {
1301: if (next == null) {
1302: return null;
1303: } else {
1304: return (JMLEqualsBagEntryNode) next;
1305: }
1306: } else {
1307: JMLEqualsBagEntryNode rest = (next == null ? null
1308: : ((JMLEqualsBagEntryNode) next).removeBE(entry));
1309: return new JMLEqualsBagEntryNode((JMLEqualsBagEntry) val,
1310: rest);
1311: }
1312: }
1313:
1314: }
|