01: // @(#)$Id: JMLDataGroup.java 1.2 Tue, 17 May 2005 14:57:40 +0200 engelc $
02:
03: // Copyright (C) 1998, 1999 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.lang;
22:
23: /** A type with one element, for use in declaring "data groups".
24: * Note that there is only one equivalence class of objects of this type;
25: * that is, all objects of this type are considered .equal to each other.
26: *
27: * @version $Revision: 1.2 $
28: * @author Gary T. Leavens, based on an idea of Rustan Leino
29: */
30: public/*@ pure @*/final class JMLDataGroup {
31:
32: /** Initialize this object.
33: * @see #IT
34: */
35: /*@ private normal_behavior
36: @ assignable owner;
37: @ ensures owner == null;
38: @*/
39: private JMLDataGroup() {
40: }
41:
42: /** The only object of this type.
43: */
44: public static final/*@ non_null @*/JMLDataGroup IT = new JMLDataGroup();
45:
46: /** Return this object.
47: */
48: public Object clone() {
49: return this ;
50: }
51:
52: /** Test whether the given argument is a non-null object of type
53: * JMLDataGroup.
54: */
55: /*@ also
56: @ public normal_behavior
57: @ ensures \result <==> oth != null && oth instanceof JMLDataGroup;
58: @*/
59: public/*@ pure @*/boolean equals(Object oth) {
60: return oth != null && oth instanceof JMLDataGroup;
61: }
62:
63: /** Return a hash code for this object.
64: */
65: public/*@ pure @*/int hashCode() {
66: return 0;
67: }
68:
69: /** Return a string representation of this object.
70: */
71: /*@ also
72: @ public normal_behavior
73: @ ensures \result != null
74: @ && (* result is a string representation of this *);
75: @*/
76: public String toString() {
77: return "JMLDataGroup.IT";
78: }
79:
80: }
|