01: // @(#)$Id: JMLValueSetSpecs.java 1.3 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: /** Special behavior for JMLValueSet not shared by JMLObjectSet.
24: *
25: * @version $Revision: 1.3 $
26: * @author Gary T. Leavens, with help from Clyde Ruby, and others.
27: * @see JMLValueType
28: * @see JMLValueSet
29: */
30: //-@ immutable
31: public/*@ pure @*/abstract class JMLValueSetSpecs implements
32: JMLValueType {
33:
34: /** Is the argument ".equals" to one of the values in the set.
35: * @see #has(Object)
36: */
37: public abstract boolean has(JMLType elem);
38:
39: /** Is the argument ".equals" to one of the values in theSet.
40: * @see #has(JMLType)
41: */
42: /*@ public normal_behavior
43: @ requires elem != null;
44: @ ensures \result
45: @ <==> elem instanceof JMLType && has((JMLType)elem);
46: @ also
47: @ public normal_behavior
48: @ requires elem == null;
49: @ ensures \result == has(null);
50: @*/
51: public boolean has(Object elem) {
52: if (elem == null) {
53: return has(null);
54: } else {
55: return elem instanceof JMLType && has((JMLType) elem);
56: }
57: }
58:
59: /** Tells the number of elements in the set.
60: */
61: /*@ public normal_behavior
62: @ ensures \result >= 0
63: @ && (* \result is the number of elements in the set *);
64: @*/
65: public abstract int int_size();
66:
67: // Specification inherited from JMLValueType.
68: // Note: not requiring the \result contain "clones" of the elements of
69: // this, allows the implementer latitude to take advantage of the
70: // nature of immutable types.
71: public abstract Object clone();
72:
73: /** Is the argument one of the objects representing values in the set?
74: * @see #has(Object)
75: */
76: /*@ public normal_behavior
77: ensures true;
78: public model boolean hasObject(JMLType elem);
79: @*/
80: /** Returns a new set that contains all the elements of this and
81: * also the given argument.
82: */
83: public abstract/*@ non_null @*/JMLValueSet insert(JMLType elem);
84:
85: }
|