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