001: // @(#)$Id: JMLValueSequenceSpecs.java 1.3 Tue, 17 May 2005 14:57:40 +0200 engelc $
002:
003: // Copyright (C) 1998, 1999 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: import java.math.BigInteger;
024:
025: /** Specical behavior for JMLValueSequence not shared by JMLObjectSequence.
026: *
027: * @version $Revision: 1.3 $
028: * @author Gary T. Leavens, with help from Clyde Ruby, and others.
029: * @see JMLValueType
030: * @see JMLValueBag
031: */
032: //-@ immutable
033: public/*@ pure @*/abstract class JMLValueSequenceSpecs implements
034: JMLValueType {
035:
036: /** Return the representative at the given index.
037: * @see #itemAt
038: */
039: /*@ public normal_behavior
040: @ requires 0 <= i && i < int_length(); //FIXME, change to _length later
041: @ ensures (* \result is the ith object of this *);
042: @ public model JMLType objectAt(\bigint i);
043: @*/
044:
045: // ********************** observers **************************
046: /** Is the argument ".equals" to one of the values in this sequence.
047: * @see #has(Object)
048: * @see #int_count(JMLType)
049: */
050: /*@ public normal_behavior
051: @ ensures \result <==>
052: @ (* elem is ".equals" to one of the objects in this sequence *);
053: @*/
054: public abstract boolean has(JMLType elem);
055:
056: /** Is the argument ".equals" to one of the values in this sequence.
057: * @see #has(JMLType)
058: * @see #count(Object)
059: */
060: /*@ public normal_behavior
061: @ requires elem != null;
062: @ ensures \result
063: @ <==> elem instanceof JMLType && has((JMLType)elem);
064: @ also
065: @ public normal_behavior
066: @ requires elem == null;
067: @ ensures \result == has(null);
068: @*/
069: public boolean has(Object elem) {
070: if (elem == null) {
071: return has(null);
072: } else {
073: return elem instanceof JMLType && has((JMLType) elem);
074: }
075: }
076:
077: /** Tell many times the argument occurs ".equals" to one of the
078: * values in this sequence.
079: * @see #count(Object)
080: * @see #has(JMLType)
081: */
082: /*@ public normal_behavior
083: @ ensures \result >= 0
084: @ && (* \result is the number of times elem tests
085: @ as ".equals" to one of the objects in this sequence *);
086: @*/
087: public abstract int count(JMLType elem);
088:
089: /** Tell many times the argument occurs ".equals" to one of the
090: * values in the bag.
091: * @see #count(JMLType)
092: * @see #has(Object)
093: */
094: /*@ public normal_behavior
095: @ requires elem != null;
096: @ ensures \result
097: @ == (elem instanceof JMLType ? count((JMLType)elem) : 0);
098: @ also
099: @ public normal_behavior
100: @ requires elem == null;
101: @ ensures \result == count(null);
102: @*/
103: public int count(Object elem) {
104: if (elem == null) {
105: return count(null);
106: } else {
107: return (elem instanceof JMLType ? count((JMLType) elem) : 0);
108: }
109: }
110:
111: /** This sequence's length.
112: */
113: /*@ public normal_behavior
114: @ ensures \result >= 0;
115: @*/
116: public abstract int int_length();
117:
118: /** Return a clone of the element at the given zero-based index.
119: * @param i the zero-based index into the sequence.
120: * @exception JMLSequenceException if the index i is out of range.
121: */
122: /*@
123: @ ensures \result == objectAt(i).clone();
124: @*/
125: public abstract JMLType itemAt(int i) throws JMLSequenceException;
126:
127: /** Return a clone of the first element in this sequence.
128: * @exception JMLSequenceException if the sequence is empty.
129: * @see #last
130: */
131: /*@
132: @ ensures \result == objectAt(0).clone();
133: @*/
134: public abstract JMLType first() throws JMLSequenceException;
135:
136: /** Return a clone of the last element in this sequence.
137: * @exception JMLSequenceException if the sequence is empty.
138: * @see #first
139: */
140: /*@
141: @ ensures \result == objectAt((int)(int_length()-1)).clone();
142: @*/
143: public abstract JMLType last() throws JMLSequenceException;
144:
145: // ********************** building new values *********
146:
147: /** Return a clone of this object, making clones of any contained
148: * objects in the sequence.
149: */
150: public abstract Object clone();
151:
152: /** Return a sequence like this, but with a clone ofitem put
153: * immediately after the given index.
154: * @param afterThisOne a zero-based index into the sequence, or -1.
155: * @param item the item to put after index afterThisOne
156: * @return if the index is in range
157: * @exception JMLSequenceException if the index is out of range.
158: * @see #insertBeforeIndex
159: * @see #insertBack
160: * @see #insertFront
161: */
162: public abstract/*@ non_null @*/JMLValueSequence insertAfterIndex(
163: int afterThisOne, JMLType item) throws JMLSequenceException;
164:
165: /** Return a sequence like this, but with a clone of item put immediately
166: * before the given index.
167: * @param beforeThisOne a zero-based index into the sequence,
168: * or the length of this.
169: * @param item the item to put before index beforeThisOne
170: * @return if the index is in range
171: * @exception JMLSequenceException if the index is out of range.
172: * @see #insertAfterIndex
173: * @see #insertBack
174: * @see #insertFront
175: */
176: public abstract/*@ non_null @*/JMLValueSequence insertBeforeIndex(
177: int beforeThisOne, JMLType item)
178: throws JMLSequenceException
179: /*@ public model_program {
180: @ assume item != null;
181: @ assume 0 <= beforeThisOne && beforeThisOne <= int_length();
182: @ JMLType copy = (JMLType)item.clone();
183: @
184: @ JMLValueSequence returnVal = null;
185: @ normal_behavior
186: @ assignable returnVal;
187: @ ensures (\forall int i; 0 <= i && i < beforeThisOne;
188: @ returnVal.objectAt(i)
189: @ == objectAt(i))
190: @ && (\forall int i;
191: @ beforeThisOne <= i && i < int_length();
192: @ returnVal.objectAt((int)(i+1)) == objectAt(i))
193: @ && returnVal.objectAt(beforeThisOne) == copy
194: @ && returnVal.int_length() == int_length() + 1;
195: @ return returnVal;
196: @ }
197: @*/
198: ;
199:
200: /** Return a sequence like this, but with a clone of the given
201: * item put an the end.
202: * @param item the item to put at the end of the result.
203: * @return a sequence the elements of this sequence followed by item.
204: * @see #insertAfterIndex
205: * @see #insertBeforeIndex
206: * @see #insertFront
207: */
208: public abstract/*@ non_null @*/JMLValueSequence insertBack(
209: JMLType item)
210: /*@ public model_program {
211: @ assume item != null && int_length() < Integer.MAX_VALUE;
212: @ JMLType copy = (JMLType)item.clone();
213: @
214: @ JMLValueSequence returnVal = null;
215: @ normal_behavior
216: @ assignable returnVal;
217: @ ensures (\forall int i; 0 <= i && i < int_length();
218: @ returnVal.objectAt(i) == objectAt(i))
219: @ && returnVal.objectAt(int_length()) == copy
220: @ && returnVal.int_length() == int_length() + 1;
221: @ return returnVal;
222: @ }
223: @*/
224: ;
225:
226: /** Return a sequence like this, but with the given item put an the front.
227: * @param item the item to put at the front of the result.
228: * @return a sequence with item followed by the elements of this sequence.
229: * @see #insertAfterIndex
230: * @see #insertBeforeIndex
231: * @see #insertBack
232: */
233: public abstract/*@ non_null @*/
234: JMLValueSequence insertFront(JMLType item)
235: /*@ public model_program {
236: @ assume item != null && int_length() < Integer.MAX_VALUE;
237: @ JMLType copy = (JMLType)item.clone();
238: @
239: @ JMLValueSequence returnVal = null;
240: @ normal_behavior
241: @ assignable returnVal;
242: @ ensures (\forall int i; 0 <= i && i < int_length();
243: @ returnVal.objectAt((int)(i+1)) == objectAt(i))
244: @ && returnVal.objectAt(0) == copy
245: @ && returnVal.int_length() == int_length() + 1;
246: @ return returnVal;
247: @ }
248: @*/
249: ;
250: }
|