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