001: // @(#)$Id: JMLString.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 reflection of {@link java.lang.String} that implements {@link JMLType}.
024: *
025: * @version $Revision: 1.2 $
026: * @author Gary T. Leavens
027: * @see java.lang.String
028: * @see JMLType
029: */
030: //-@ immutable
031: public/*@ pure @*/class JMLString implements JMLComparable {
032:
033: /** The contents of this object.
034: */
035: //@ public model String theString;
036: //@ public invariant theString != null;
037: protected String str_;
038:
039: //@ in theString;
040: //@ protected represents theString <- str_;
041:
042: //@ protected invariant str_ != null;
043:
044: //@ public invariant owner == null;
045:
046: /** Initialize the contents of this object to be the empty string.
047: * @see #EMPTY
048: */
049: /*@ public normal_behavior
050: @ assignable theString, owner;
051: @ ensures theString.equals("");
052: @*/
053: public JMLString() {
054: str_ = "";
055: }
056:
057: /** Initialize the contents of this object to be the given string.
058: */
059: /*@ public normal_behavior
060: @ requires s != null;
061: @ assignable theString, owner;
062: @ ensures theString.equals(s);
063: @*/
064: public JMLString(/*@ non_null @*/String s)
065: throws IllegalArgumentException {
066: if (s != null) {
067: str_ = s;
068: } else {
069: throw new IllegalArgumentException();
070: }
071: }
072:
073: /** The empty JMLString.
074: * @see #JMLString()
075: */
076: public static final JMLString EMPTY = new JMLString();
077:
078: /** Return a clone of this string.
079: */
080: /*@ also
081: @ public normal_behavior
082: @ ensures \result == this;
083: @*/
084: public Object clone() {
085: return this ;
086: }
087:
088: /** Compare this to op2, returning a comparison code.
089: * @param op2 the object this is compared to.
090: * @exception ClassCastException when o is not a JMLString.
091: * @exception NullPointerException when o is null.
092: * @see #equals(Object)
093: * @see #compareTo(JMLString)
094: */
095: /*@ also
096: @ public normal_behavior
097: @ requires op2 instanceof JMLString;
098: @ ensures \result == theString.compareTo(((JMLString)op2).theString);
099: @ also
100: @ public exceptional_behavior
101: @ requires !(op2 instanceof JMLString);
102: @ signals (ClassCastException);
103: @*/
104: public int compareTo(Object op2) throws ClassCastException {
105: return str_.compareTo(((JMLString) op2).str_); //@ nowarn Cast;
106: }
107:
108: /** Compares this to another.
109: * @see #equals(Object)
110: * @see #compareTo(Object)
111: */
112: /*@ public normal_behavior
113: @ requires another != null;
114: @ ensures \result == theString.compareTo(another.theString);
115: @*/
116: public int compareTo(/*@ non_null @*/JMLString another) {
117: return str_.compareTo(another.str_);
118: }
119:
120: /** Tell if these two strings are equal.
121: * @see #equalsIgnoreCase(String)
122: * @see #equalsIgnoreCase(JMLString)
123: * @see #compareTo(Object)
124: * @see #compareTo(JMLString)
125: */
126: /*@ also
127: @ public normal_behavior
128: @ {|
129: @ requires s != null && s instanceof JMLString;
130: @ ensures \result == ((JMLString) s).theString.equals(theString);
131: @ also
132: @ requires s == null || !(s instanceof JMLString);
133: @ ensures !\result;
134: @ |}
135: @*/
136: public boolean equals(Object s) {
137: if (s != null && s instanceof JMLString) {
138: return (str_.equals(((JMLString) s).str_));
139: } else {
140: return (false);
141: }
142: }
143:
144: /** Are these strings equal, except for case?
145: * @see #equals
146: * @see #equalsIgnoreCase(String)
147: * @see #compareTo(Object)
148: * @see #compareTo(JMLString)
149: */
150: /*@ public normal_behavior
151: @ requires another != null;
152: @ ensures \result == theString.equalsIgnoreCase(another.theString);
153: @*/
154: public boolean equalsIgnoreCase(/*@ non_null @*/JMLString another) {
155: return str_.equalsIgnoreCase(another.str_);
156: }
157:
158: /** Are these strings equal, except for case?
159: * @see #equals
160: * @see #equalsIgnoreCase(JMLString)
161: * @see #compareTo(Object)
162: * @see #compareTo(JMLString)
163: */
164: /*@ public normal_behavior
165: @ requires another != null;
166: @ ensures \result == theString.equalsIgnoreCase(another);
167: @*/
168: public boolean equalsIgnoreCase(/*@ non_null @*/String another) {
169: return str_.equalsIgnoreCase(another);
170: }
171:
172: /** Return a hash code for this object.
173: */
174: // specification is inherited
175: public int hashCode() {
176: return (str_.hashCode());
177: }
178:
179: /** Return theString.
180: */
181: /*@ also
182: @ public normal_behavior
183: @ ensures \result.equals(theString);
184: @*/
185: public String toString() {
186: return (str_);
187: }
188:
189: /** Produce a new JMLString that is the concatentation of two JMLStrings.
190: */
191: public JMLString concat(JMLString s) {
192: return new JMLString(str_ + s.str_);
193: }
194:
195: /** Produce a new JMLString that is the concatentation of the JMLString
196: and a String.
197: */
198: public JMLString concat(String s) {
199: return new JMLString(str_ + s);
200: }
201:
202: /** Produce a new JMLString that is the concatentation of the JMLString
203: and a char.
204: */
205: public JMLString concat(char c) {
206: return new JMLString(str_ + c);
207: }
208: }
|