01: // @(#)$Id: JMLCollection.java 1.1.1.1 Mon, 09 May 2005 15:27:50 +0200 engelc $
02:
03: // Copyright (C) 1998, 1999, 2002 Iowa State University
04:
05: // This file is part of JML
06:
07: // JML is free software; you can redistribute it and/or modify
08: // it under the terms of the GNU General Public License as published by
09: // the Free Software Foundation; either version 2, or (at your option)
10: // any later version.
11:
12: // JML is distributed in the hope that it will be useful,
13: // but WITHOUT ANY WARRANTY; without even the implied warranty of
14: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15: // GNU General Public License for more details.
16:
17: // You should have received a copy of the GNU General Public License
18: // along with JML; see the file COPYING. If not, write to
19: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
20:
21: package org.jmlspecs.models;
22:
23: /** Common protocol of the JML model collection types.
24: *
25: * The use of elementType and containsNull in this specification
26: * follows the ESC/Java specification of {@link java.util.Collection}.
27: * That is, these ghost fields are used by the user of the object to
28: * state what types of objects are allowed to be added to the collection,
29: * and hence what is guaranteed to be retrieved from the collection. They
30: * are not adjusted by methods based on the content of the collection.
31: *
32: * @version $Revision: 1.1.1.1 $
33: * @author Gary T. Leavens
34: * @author Yoonsik Cheon
35: * @see JMLEnumeration
36: * @see JMLIterator
37: */
38: //-@ immutable
39: public interface JMLCollection extends JMLType {
40:
41: /** The type of the elements in this collection.
42: */
43: //@ instance ghost public Object elementType;
44: //@ public instance constraint elementType == \old(elementType);
45: /** Whether this collection can contain null elements;
46: * think of it as "is allowed to contain null".
47: */
48: //@ instance ghost public boolean containsNull;
49: //@ public instance constraint containsNull == \old(containsNull);
50:
51: /** Returns an Iterator over this object.
52: */
53: /*@ public normal_behavior
54: @ ensures \fresh(\result) && \result.elementType == this.elementType;
55: @ ensures !containsNull ==> !\result.returnsNull;
56: @*/
57: /*@ pure @*//*@ non_null @*/JMLIterator iterator();
58:
59: /** Tell whether the argument is equal to one of the elements in
60: * this collection, using the notion of element equality
61: * appropriate for the collection.
62: */
63: /*@ public normal_behavior
64: @ ensures_redundantly !containsNull && elem == null ==> !\result;
65: @ ensures_redundantly
66: @ elem != null && !(\typeof(elem) <: elementType) ==> !\result;
67: @*/
68: /*@ pure @*/boolean has(Object elem);
69:
70: /** Tell the number of elements in this collection.
71: */
72: /*@ public normal_behavior
73: @ ensures \result >= 0;
74: @
75: @ model pure public int size();
76: @*/
77:
78: /*@ public normal_behavior
79: @ requires size() <= Integer.MAX_VALUE;
80: @ ensures \result == size();
81: @*/
82: /*@ pure @*/public int int_size();
83:
84: }
|