01: // Copyright (C) 2002 Iowa State University
02:
03: // This file is part of JML
04:
05: // JML is free software; you can redistribute it and/or modify
06: // it under the terms of the GNU General Public License as published by
07: // the Free Software Foundation; either version 2, or (at your option)
08: // any later version.
09:
10: // JML is distributed in the hope that it will be useful,
11: // but WITHOUT ANY WARRANTY; without even the implied warranty of
12: // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13: // GNU General Public License for more details.
14:
15: // You should have received a copy of the GNU General Public License
16: // along with GNU Emacs; see the file COPYING. If not, write to
17: // the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
18:
19: package org.jmlspecs.models;
20:
21: /** A class with static methods that safely work with null objects.
22: *
23: * @version $Revision: 1.1 $
24: * @author Katie Becker and Gary T. Leavens
25: */
26: //-@ immutable
27: public class JMLNullSafe {
28:
29: /** No instances of this class can be created. */
30: private JMLNullSafe() {
31: }
32:
33: /** Test for equality of o1 and o2, allowing either to be null. */
34: //@ ensures \result <==> (o1 == null ? o2 == null : o1.equals(o2));
35: public static/*@ pure @*/boolean equals(Object o1, Object o2) {
36: return o1 == null ? o2 == null : o1.equals(o2);
37: }
38:
39: /** Return a string representation for the argument, which may be null. */
40: /*@ public normal_behavior
41: @ requires o == null;
42: @ assignable \nothing;
43: @ ensures \result != null && \result.equals("null");
44: @ also
45: @ requires o != null;
46: @ ensures \result != null;
47: @*/
48: public static String toString(Object o) {
49: return o == null ? "null" : o.toString();
50: }
51:
52: /** Return a hash code for the argument, which may be null. */
53: /*@ public normal_behavior
54: @ requires o == null;
55: @ assignable \nothing;
56: @ ensures \result == 0;
57: @*/
58: public static int hashCode(Object o) {
59: return o == null ? 0 : o.hashCode();
60: }
61: }
|