001: // @(#)$Id: JMLArrayOps.java 1.1 Mon, 02 May 2005 14:31:03 +0200 engelc $
002:
003: // Adapted in part from Compaq SRC's specification for ESC/Java
004:
005: // Copyright (C) 2000, 2002 Iowa State University
006:
007: // This file is part of JML
008:
009: // JML is free software; you can redistribute it and/or modify
010: // it under the terms of the GNU General Public License as published by
011: // the Free Software Foundation; either version 2, or (at your option)
012: // any later version.
013:
014: // JML is distributed in the hope that it will be useful,
015: // but WITHOUT ANY WARRANTY; without even the implied warranty of
016: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
017: // GNU General Public License for more details.
018:
019: // You should have received a copy of the GNU General Public License
020: // along with JML; see the file COPYING. If not, write to
021: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
022:
023: package org.jmlspecs.models;
024:
025: /** Array Operations that are useful for specifications.
026: *
027: * @version $Revision: 1.1 $
028: * @author Brandon Shilling
029: * @author Gary T. Leavens
030: * @see java.util.Arrays
031: * @see JMLObjectSequence
032: * @see JMLValueSequence
033: */
034: public class JMLArrayOps {
035:
036: /** Search the array for the given element and return how many
037: * times that element's object identity occurs in the array.
038: * @see #objectIdentityCount(Object[], Object, int)
039: * @see #hasObjectIdentity(Object[], Object)
040: * @see #valueEqualsCount(Object[], Object)
041: */
042: /*@ public normal_behavior
043: @ requires array != null;
044: @ ensures \result == (\num_of int i; 0 <= i && i < array.length;
045: @ array[i] == element);
046: @*/
047: public static/*@ pure @*/int objectIdentityCount(
048: /*@ non_null @*/Object[] array, Object element) {
049: return objectIdentityCount(array, element, array.length);
050: }
051:
052: /** Search the array for the given element and return how many
053: * times that element's object identity occurs in the array from
054: * 0 the given length-1.
055: * @see #objectIdentityCount(Object[], Object)
056: * @see #hasObjectIdentity(Object[], Object, int)
057: * @see #valueEqualsCount(Object[], Object, int)
058: */
059: /*@ public normal_behavior
060: @ requires array != null;
061: @ requires 0 <= length && length <= array.length;
062: @ ensures \result == (\num_of int i; 0 <= i && i < length;
063: @ array[i] == element);
064: @ implies_that
065: @ requires 0 <= length && length <= array.length;
066: @*/
067: public static/*@ pure @*/int objectIdentityCount(
068: /*@ non_null @*/Object[] array, Object element, int length) {
069: int elementCount = 0;
070: for (int i = 0; i < length; i++) {
071: if (element == array[i]) {
072: elementCount++;
073: }
074: }
075: return elementCount;
076: }
077:
078: /** Search the array for the given element and return how many
079: * times an object with value "equals" to the given element occurs
080: * in the array.
081: * @see #valueEqualsCount(Object[], Object, int)
082: * @see #hasValueEquals(Object[], Object)
083: * @see #objectIdentityCount(Object[], Object)
084: */
085: /*@ public normal_behavior
086: @ requires array != null;
087: @ ensures \result
088: @ == (\num_of int i; 0 <= i && i < array.length;
089: @ (array[i] == null ==> element == null)
090: @ && (array[i] != null
091: @ ==> (* array[i].equals(element) *) ));
092: @*/
093: public static/*@ pure @*/int valueEqualsCount(
094: /*@ non_null @*/Object[] array, Object element) {
095: return valueEqualsCount(array, element, array.length);
096: }
097:
098: /** Search the array for the given element and return how many
099: * times an object with value "equals" to the given element occurs
100: * in the array from 0 the given length-1.
101: * @see #valueEqualsCount(Object[], Object)
102: * @see #hasValueEquals(Object[], Object, int)
103: * @see #objectIdentityCount(Object[], Object, int)
104: */
105: /*@ public normal_behavior
106: @ requires array != null;
107: @ requires 0 <= length && length <= array.length;
108: @ ensures \result
109: @ == (\num_of int i; 0 <= i && i < length;
110: @ (array[i] == null ==> element == null)
111: @ && (array[i] != null
112: @ ==> (* array[i].equals(element) *) ));
113: @ implies_that
114: @ requires 0 <= length && length <= array.length;
115: @*/
116: public static/*@ pure @*/int valueEqualsCount(
117: /*@ non_null @*/Object[] array, Object element, int length) {
118: int valueEqCount = 0;
119: for (int i = 0; i < length; i++) {
120: if (element == null) {
121: if (array[i] == null) {
122: valueEqCount++;
123: }
124: } else if (element.equals(array[i])) {
125: valueEqCount++;
126: }
127: }
128: return valueEqCount;
129: }
130:
131: /** Search the array for the given element and tell if
132: * that element's object identity occurs in the array.
133: * @see #hasObjectIdentity(Object[], Object, int)
134: * @see #objectIdentityCount(Object[], Object)
135: * @see #hasValueEquals(Object[], Object)
136: */
137: /*@ public normal_behavior
138: @ requires array != null;
139: @ ensures \result == (\exists int i; 0 <= i && i < array.length;
140: @ array[i] == element);
141: @*/
142: public static/*@ pure @*/boolean hasObjectIdentity(
143: /*@ non_null @*/Object[] array, Object element) {
144: return hasObjectIdentity(array, element, array.length);
145: }
146:
147: /** Search the array for the given element and tell if that
148: * element's object identity occurs in the array from 0 the given
149: * length-1.
150: * @see #hasObjectIdentity(Object[], Object)
151: * @see #objectIdentityCount(Object[], Object)
152: * @see #hasValueEquals(Object[], Object)
153: */
154: /*@ public normal_behavior
155: @ requires array != null;
156: @ requires 0 <= length && length <= array.length;
157: @ ensures \result == (\exists int i; 0 <= i && i < length;
158: @ array[i] == element);
159: @ implies_that
160: @ requires 0 <= length && length <= array.length;
161: @*/
162: public static/*@ pure @*/boolean hasObjectIdentity(
163: /*@ non_null @*/Object[] array, Object element, int length) {
164: for (int i = 0; i < length; i++) {
165: if (element == array[i]) {
166: return true;
167: }
168: }
169: return false;
170: }
171:
172: /** Search the array for the given element and tell if an object
173: * with value "equals" to the given element occurs in the array.
174: * @see #hasValueEquals(Object[], Object, int)
175: * @see #valueEqualsCount(Object[], Object)
176: * @see #hasObjectIdentity(Object[], Object)
177: */
178: /*@ public normal_behavior
179: @ requires array != null;
180: @ ensures \result
181: @ == (\exists int i; 0 <= i && i < array.length;
182: @ (array[i] == null ==> element == null)
183: @ && (array[i] != null
184: @ ==> (* array[i].equals(element) *) ));
185: @*/
186: public static/*@ pure @*/boolean hasValueEquals(
187: /*@ non_null @*/Object[] array, Object element) {
188: return hasValueEquals(array, element, array.length);
189: }
190:
191: /** Search the array for the given element and tell if an object
192: * with value "equals" to the given element occurs in the array
193: * from 0 the given length-1.
194: * @see #hasValueEquals(Object[], Object)
195: * @see #valueEqualsCount(Object[], Object, int)
196: * @see #hasObjectIdentity(Object[], Object, int)
197: */
198: /*@ public normal_behavior
199: @ requires array != null;
200: @ requires 0 <= length && length <= array.length;
201: @ ensures \result
202: @ == (\exists int i; 0 <= i && i < length;
203: @ (array[i] == null ==> element == null)
204: @ && (array[i] != null
205: @ ==> (* array[i].equals(element) *) ));
206: @ implies_that
207: @ requires 0 <= length && length <= array.length;
208: @*/
209: public static/*@ pure @*/boolean hasValueEquals(
210: /*@ non_null @*/Object[] array, Object element, int length) {
211: for (int i = 0; i < length; i++) {
212: if (element == null) {
213: if (array[i] == null) {
214: return true;
215: }
216: } else if (element.equals(array[i])) {
217: return true;
218: }
219: }
220: return false;
221: }
222:
223: }
|