001: // @(#)$Id: JMLValueBagSpecs.java 1.1 Mon, 02 May 2005 14:31:03 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999, 2002 Iowa State University
004:
005: // This file is part of JML
006:
007: // JML is free software; you can redistribute it and/or modify
008: // it under the terms of the GNU General Public License as published by
009: // the Free Software Foundation; either version 2, or (at your option)
010: // any later version.
011:
012: // JML is distributed in the hope that it will be useful,
013: // but WITHOUT ANY WARRANTY; without even the implied warranty of
014: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
015: // GNU General Public License for more details.
016:
017: // You should have received a copy of the GNU General Public License
018: // along with JML; see the file COPYING. If not, write to
019: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
020:
021: package org.jmlspecs.models;
022:
023: /** Special behavior for JMLValueBag not shared by JMLObjectBag.
024: *
025: * @version $Revision: 1.1 $
026: * @author Gary T. Leavens, with help from Clyde Ruby, and others.
027: * @see JMLValueType
028: * @see JMLValueBag
029: */
030: //-@ immutable
031: public/*@ pure @*/abstract class JMLValueBagSpecs implements
032: JMLValueType {
033:
034: /** Is the argument ".equals" to one of the values in this bag.
035: * @see #has(Object)
036: * @see #count(JMLType)
037: */
038: /*@ public normal_behavior
039: @ ensures \result <==> count(elem) > 0;
040: @*/
041: public abstract boolean has(JMLType elem);
042:
043: /** Is the argument ".equals" to one of the values in this bag.
044: * @see #has(JMLType)
045: * @see #count(Object)
046: */
047: /*@ public normal_behavior
048: @ requires elem != null;
049: @ ensures \result
050: @ <==> elem instanceof JMLType && has((JMLType)elem);
051: @ also
052: @ public normal_behavior
053: @ requires elem == null;
054: @ ensures \result == has(null);
055: @*/
056: public boolean has(Object elem) {
057: if (elem == null) {
058: return has(null);
059: } else {
060: return elem instanceof JMLType && has((JMLType) elem);
061: }
062: }
063:
064: /** Tell many times the argument occurs ".equals" to one of the
065: * values in this bag.
066: * @see #count(Object)
067: * @see #has(JMLType)
068: */
069: /*@ public normal_behavior
070: @ ensures \result >= 0;
071: @*/
072: public abstract int count(JMLType elem);
073:
074: /** Tell many times the argument occurs ".equals" to one of the
075: * values in this bag.
076: * @see #count(JMLType)
077: * @see #has(Object)
078: */
079: /*@ public normal_behavior
080: @ requires elem != null;
081: @ ensures \result
082: @ == (elem instanceof JMLType ? count((JMLType)elem) : 0);
083: @ also
084: @ public normal_behavior
085: @ requires elem == null;
086: @ ensures \result == count(null);
087: @*/
088: public int count(Object elem) {
089: if (elem == null) {
090: return count(null);
091: } else {
092: return (elem instanceof JMLType ? count((JMLType) elem) : 0);
093: }
094: }
095:
096: /** Tells the number of elements in the bag.
097: */
098: /*@ public normal_behavior
099: @ ensures \result >= 0;
100: @*/
101: public abstract int int_size();
102:
103: // Specification inherited from JMLValueType.
104: // Note: not requiring the \result contain "clones" of the elements of
105: // this, allows the implementer latitude to take advantage of the
106: // nature of immutable types.
107: public abstract Object clone();
108:
109: /*@ public normal_behavior
110: @ requires true;
111: @ public model int countObject(JMLType elem);
112: @*/
113:
114: public abstract/*@ non_null @*/JMLValueBag insert(JMLType elem);
115:
116: /*@
117: @ signals (IllegalArgumentException) cnt < 0;
118: @*/
119: public abstract/*@ non_null @*/JMLValueBag insert(JMLType elem,
120: int cnt) throws IllegalArgumentException;
121:
122: }
|