001: // @(#)$Id: JMLModelValueSet.java 1.1 Mon, 02 May 2005 14:31:03 +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 value sets for use in set comprehensions. The
024: * normal (non-model) methods might potentially be useful in executing
025: * assertions, although the sets of all integers and longs can't
026: * realistically be used in a direct way. The model methods have no
027: * hope of being executed.
028: *
029: * @version $Revision: 1.1 $
030: * @author Gary T. Leavens
031: * @see JMLValueSet
032: */
033: //-@ immutable
034: public/*@ pure @*/class JMLModelValueSet {
035:
036: /** This class has no instances.
037: */
038: private JMLModelValueSet() {
039: }
040:
041: /** The set of all (actual and potential) JMLByte values.
042: */
043: /*@ public normal_behavior
044: @ assignable \nothing;
045: @ ensures (\forall byte i;
046: @ (\exists JMLByte j; \result.has(j) && j != null;
047: @ j.theByte == i ));
048: @*/
049: public static/*@ pure @*//*@ non_null @*/JMLValueSet JMLBytes() {
050: JMLValueSet ret = null;
051: if (ret == null) {
052: ret = new JMLValueSet(new JMLByte(Byte.MAX_VALUE));
053: for (byte i = Byte.MIN_VALUE; i < Byte.MAX_VALUE; i++) {
054: ret = ret.insert(new JMLByte(i));
055: }
056: }
057: return ret;
058: } //@ nowarn Exception;
059:
060: /** The set of all (actual and potential) JMLChar values.
061: */
062: /*@ public normal_behavior
063: @ assignable \nothing;
064: @ ensures (\forall char i;
065: @ (\exists JMLChar j; \result.has(j) && j != null;
066: @ j.theChar == i ));
067: @*/
068: public static/*@ pure @*//*@ non_null @*/JMLValueSet JMLChars() {
069: JMLValueSet ret = null;
070: if (ret == null) {
071: ret = new JMLValueSet(new JMLChar(Character.MAX_VALUE));
072: for (char i = Character.MIN_VALUE; i < Character.MAX_VALUE; i++) {
073: ret = ret.insert(new JMLChar(i));
074: }
075: }
076: return ret;
077: } //@ nowarn Exception;
078:
079: /** The set of all (actual and potential) JMLShort values.
080: */
081: /*@ public normal_behavior
082: @ assignable \nothing;
083: @ ensures (\forall short i;
084: @ (\exists JMLShort j; \result.has(j) && j != null;
085: @ j.theShort == i ));
086: @*/
087: public static/*@ pure @*//*@ non_null @*/JMLValueSet JMLShorts() {
088: JMLValueSet ret = null;
089: if (ret == null) {
090: ret = new JMLValueSet(new JMLShort(Short.MAX_VALUE));
091: for (short i = Short.MIN_VALUE; i < Short.MAX_VALUE; i++) {
092: ret = ret.insert(new JMLShort(i));
093: }
094: }
095: return ret;
096: } //@ nowarn Exception;
097:
098: /** The set of all (actual and potential) JMLInteger values.
099: */
100: /*@ public normal_behavior
101: @ assignable \nothing;
102: @ ensures (\forall int i;
103: @ (\exists JMLInteger j; \result.has(j) && j != null;
104: @ j.theInt == i ));
105: public static pure model non_null JMLValueSet JMLIntegers();
106: @*/
107:
108: // ********* The following aren't ever going to be executable. *******
109:
110: /** The set of all (actual and potential) JMLLong values.
111: */
112: /*@ public normal_behavior
113: @ assignable \nothing;
114: @ ensures (\forall long i;
115: @ (\exists JMLLong j; \result.has(j) && j != null;
116: @ j.theLong == i ));
117: public static pure model non_null JMLValueSet JMLLongs();
118: @*/
119:
120: /** The set of all (actual and potential) JMLString values.
121: */
122: /*@ public normal_behavior
123: @ assignable \nothing;
124: @ ensures (\forall String s; s != null;
125: @ (\exists JMLString js; \result.has(js) && js != null;
126: @ js.theString.equals(s) ));
127: public static pure model non_null JMLValueSet JMLStrings();
128: @*/
129:
130: /** The set of all (actual and potential) JMLFloat values.
131: */
132: /*@ public normal_behavior
133: @ assignable \nothing;
134: @ ensures (\forall float f;
135: @ (\exists JMLFloat jf; \result.has(jf) && jf != null;
136: @ (Float.isNaN(f) && jf.isNaN())
137: @ || jf.theFloat == f ));
138: public static pure model non_null JMLValueSet JMLFloats();
139: @*/
140:
141: /** The set of all (actual and potential) JMLDouble values.
142: */
143: /*@ public normal_behavior
144: @ assignable \nothing;
145: @ ensures (\forall double f;
146: @ (\exists JMLDouble jf; \result.has(jf) && jf != null;
147: @ (Double.isNaN(f) && jf.isNaN())
148: @ || jf.theDouble == f ));
149: public static pure model non_null JMLValueSet JMLDoubles();
150: @*/
151: }
|