001: // @(#)$Id: JMLModelObjectSet.java 1.2 Mon, 09 May 2005 15:27:50 +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: /** A collection of object sets for use in set comprehensions. All of
024: * the public methods are model methods, because there is no way to
025: * compute the set of all potential object identities of any given
026: * type.
027: *
028: * <p> This type is not that useful, as you can mostly just use
029: * quantification over the relevant type instead of one of these sets.
030: * Indeed the sets are defined by using universal quantifiers, and so their
031: * use is roughly equivalent.
032: *
033: * @version $Revision: 1.2 $
034: * @author Gary T. Leavens
035: */
036: //-@ immutable
037: public/*@ pure @*/class JMLModelObjectSet {
038:
039: /** The set of all (actual and potential) JMLByte objects.
040: */
041: /*@ public normal_behavior
042: @ assignable \nothing;
043: @ ensures (\forall JMLByte x; ; \result.has(x));
044: public static pure model non_null JMLObjectSet JMLBytes();
045: @*/
046:
047: /** The set of all (actual and potential) JMLChar objects.
048: */
049: /*@ public normal_behavior
050: @ assignable \nothing;
051: @ ensures (\forall JMLChar x; ; \result.has(x));
052: public static pure model non_null JMLObjectSet JMLChars();
053: @*/
054:
055: /** The set of all (actual and potential) JMLInteger objects.
056: */
057: /*@ public normal_behavior
058: @ assignable \nothing;
059: @ ensures (\forall JMLInteger x; ; \result.has(x));
060: public static pure model non_null JMLObjectSet JMLIntegers();
061: @*/
062:
063: /** The set of all (actual and potential) JMLLong objects.
064: */
065: /*@ public normal_behavior
066: @ assignable \nothing;
067: @ ensures (\forall JMLLong x; ; \result.has(x));
068: public static pure model non_null JMLObjectSet JMLLongs();
069: @*/
070:
071: /** The set of all (actual and potential) JMLShort objects.
072: */
073: /*@ public normal_behavior
074: @ assignable \nothing;
075: @ ensures (\forall JMLShort x; ; \result.has(x));
076: public static pure model non_null JMLObjectSet JMLShorts();
077: @*/
078:
079: /** The set of all (actual and potential) JMLString objects.
080: */
081: /*@ public normal_behavior
082: @ assignable \nothing;
083: @ ensures (\forall JMLString x; ; \result.has(x));
084: public static pure model non_null JMLObjectSet JMLStrings();
085: @*/
086:
087: /** The set of all (actual and potential) JMLFloat objects.
088: */
089: /*@ public normal_behavior
090: @ assignable \nothing;
091: @ ensures (\forall JMLFloat x; ; \result.has(x));
092: public static pure model non_null JMLObjectSet JMLFloats();
093: @*/
094:
095: /** The set of all (actual and potential) JMLDouble objects.
096: */
097: /*@ public normal_behavior
098: @ assignable \nothing;
099: @ ensures (\forall JMLDouble x; ; \result.has(x));
100: public static pure model non_null JMLObjectSet JMLDoubles();
101: @*/
102:
103: /** The set of all (actual and potential) Boolean objects.
104: */
105: /*@ public normal_behavior
106: @ assignable \nothing;
107: @ ensures (\forall Boolean x; ; \result.has(x));
108: public static pure model non_null JMLObjectSet Booleans();
109: @*/
110:
111: /** The set of all (actual and potential) Byte objects.
112: */
113: /*@ public normal_behavior
114: @ assignable \nothing;
115: @ ensures (\forall Byte x; ; \result.has(x));
116: public static pure model non_null JMLObjectSet Bytes();
117: @*/
118:
119: /** The set of all (actual and potential) Character objects.
120: */
121: /*@ public normal_behavior
122: @ assignable \nothing;
123: @ ensures (\forall Character x; ; \result.has(x));
124: public static pure model non_null JMLObjectSet Characters();
125: @*/
126:
127: /** The set of all (actual and potential) Integer objects.
128: */
129: /*@ public normal_behavior
130: @ assignable \nothing;
131: @ ensures (\forall Integer x; ; \result.has(x));
132: public static pure model non_null JMLObjectSet Integers();
133: @*/
134:
135: /** The set of all (actual and potential) Long objects.
136: */
137: /*@ public normal_behavior
138: @ assignable \nothing;
139: @ ensures (\forall Long x; ; \result.has(x));
140: public static pure model non_null JMLObjectSet Longs();
141: @*/
142:
143: /** The set of all (actual and potential) Short objects.
144: */
145: /*@ public normal_behavior
146: @ assignable \nothing;
147: @ ensures (\forall Short x; ; \result.has(x));
148: public static pure model non_null JMLObjectSet Shorts();
149: @*/
150:
151: /** The set of all (actual and potential) String objects.
152: */
153: /*@ public normal_behavior
154: @ assignable \nothing;
155: @ ensures (\forall String x; ; \result.has(x));
156: public static pure model non_null JMLObjectSet Strings();
157: @*/
158:
159: /** The set of all (actual and potential) Float objects.
160: */
161: /*@ public normal_behavior
162: @ assignable \nothing;
163: @ ensures (\forall Float x; ; \result.has(x));
164: public static pure model non_null JMLObjectSet Floats();
165: @*/
166:
167: /** The set of all (actual and potential) Double objects.
168: */
169: /*@ public normal_behavior
170: @ assignable \nothing;
171: @ ensures (\forall Double x; ; \result.has(x));
172: public static pure model non_null JMLObjectSet Doubles();
173: @*/
174:
175: /** This class has no instances.
176: */
177: private JMLModelObjectSet() {
178: }
179: }
|