Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

java.lang
Class String

java.lang.Object
  extended byjava.lang.String
All Implemented Interfaces:
CharSequence, Comparable, Serializable
public final class String
extends Object
implements Serializable, Comparable, CharSequence

JML's specification of java.lang.String.

Version:
$Revision: 1.44 $
Author:
Gary T. Leavens

Class Specifications
axiom ( \forall char[] s1, s2; s1 != null&&s2 != null; !equal(s1,s2) ==> (lessThan(s1,s2) <=!=> lessThan(s2,s1)));
public invariant this.stringSeq != null;
public invariant ( \forall int i; 0 <= i&&i < this.stringSeq.int_length(); this.stringSeq.itemAt(i) instanceof org.jmlspecs.models.JMLChar);
initially !this.isInterned;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Specifications inherited from interface Comparable
instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0);
instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x)));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

Specifications inherited from interface CharSequence
axiom ( \forall char[] a; ; equal(a,a));
axiom ( \forall char[] a, b; ; equal(a,b) <==> equal(b,a));
axiom ( \forall char[] a, b, c; ; (equal(a,b)&&equal(b,c)) ==> equal(a,c));
public invariant this.charArray != null;
public invariant this.charArray.owner == this;

Model Field Summary
 boolean isInterned
           
 JMLValueSequence stringSeq
           
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Model fields inherited from interface java.lang.CharSequence
charArray
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
static Comparator CASE_INSENSITIVE_ORDER
           
 
Model Constructor Summary
protected String(JMLValueSequence seq)
           
 
Constructor Summary
  String()
           
  String(non_null byte[] bytes)
           
  String(non_null byte[] ascii, int hibyte)
          Deprecated. as of 1.1
  String(non_null byte[] bytes, int offset, int length)
           
  String(non_null byte[] ascii, int hibyte, int offset, int count)
          Deprecated. as of 1.1
  String(non_null byte[] bytes, int offset, int length, non_null String charsetName)
           
  String(non_null byte[] bytes, non_null String charsetName)
           
  String(non_null char[] value)
           
  String(non_null char[] value, int offset, int count)
           
(package private) String(int offset, int count, char[] value)
           
  String(String original)
           
  String(non_null StringBuffer buffer)
           
 
Model Method Summary
 boolean byteArraysEqual(byte[] a, byte[] b)
           
 char byteToChar(int hibyte, byte ascii)
           
static boolean charEqualsIgnoreCase(char c1, char c2)
           
static boolean lessThan(char[] s1, char[] s2)
           
static boolean lessThan(JMLValueSequence s1, JMLValueSequence s2)
           
static boolean lessThanIgnoreCase(JMLValueSequence s1, JMLValueSequence s2)
           
 
Model methods inherited from class java.lang.Object
hashValue
 
Model methods inherited from interface java.lang.Comparable
definedComparison, sgn
 
Model methods inherited from interface java.lang.CharSequence
equal, equal
 
Method Summary
 char charAt(int index)
           
 int compareTo(non_null Object o)
           
 int compareTo(non_null String anotherString)
           
 int compareToIgnoreCase(nullable String str)
           
 String concat(non_null String str)
           
 boolean contentEquals(StringBuffer sb)
           
static String copyValueOf(non_null char[] data)
           
static String copyValueOf(non_null char[] data, int offset, int count)
           
 boolean endsWith(String suffix)
           
 boolean equals(nullable Object anObject)
          According to the javadocs, the equals method should not be called.
 boolean equalsIgnoreCase(String anotherString)
           
 byte[] getBytes()
           
 void getBytes(int srcBegin, int srcEnd, byte[] dst, int dstBegin)
          Deprecated. as of 1.1, use getBytes()
 byte[] getBytes(String charsetName)
           
 void getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin)
           
 int hashCode()
          According to the javadocs, the hashCode method should not be called.
(package private) static int indexOf(char[] source, int sourceOffset, int sourceCount, char[] target, int targetOffset, int targetCount, int fromIndex)
           
 int indexOf(int ch)
           
 int indexOf(int ch, int fromIndex)
           
 int indexOf(String str)
           
 int indexOf(String str, int fromIndex)
           
 String intern()
           
(package private) static int lastIndexOf(char[] source, int sourceOffset, int sourceCount, char[] target, int targetOffset, int targetCount, int fromIndex)
           
 int lastIndexOf(int ch)
           
 int lastIndexOf(int ch, int fromIndex)
           
 int lastIndexOf(String str)
           
 int lastIndexOf(String str, int fromIndex)
           
 int length()
           
 boolean matches(non_null String regex)
           
 boolean regionMatches(boolean ignoreCase, int toffset, String other, int ooffset, int len)
           
 boolean regionMatches(int toffset, String other, int ooffset, int len)
           
 String replace(char oldChar, char newChar)
           
 String replaceAll(non_null String regex, non_null String replacement)
           
 String replaceFirst(non_null String regex, non_null String replacement)
           
 String[] split(non_null String regex)
           
 String[] split(non_null String regex, int limit)
           
 boolean startsWith(String prefix)
           
 boolean startsWith(String prefix, int toffset)
           
 CharSequence subSequence(int beginIndex, int endIndex)
           
 String substring(int beginIndex)
           
 String substring(int beginIndex, int endIndex)
           
 char[] toCharArray()
           
 String toLowerCase()
           
 String toLowerCase(non_null Locale locale)
           
 String toString()
           
 String toUpperCase()
           
 String toUpperCase(non_null Locale locale)
           
 String trim()
           
static String valueOf(boolean b)
           
static String valueOf(char c)
           
static String valueOf(non_null char[] data)
           
static String valueOf(non_null char[] data, int offset, int count)
           
static String valueOf(double d)
           
static String valueOf(float f)
           
static String valueOf(int i)
           
static String valueOf(Object obj)
           
static String valueOf(long l)
           
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Model Field Detail

stringSeq

public JMLValueSequence stringSeq

isInterned

public boolean isInterned
Field Detail

CASE_INSENSITIVE_ORDER

public static final Comparator CASE_INSENSITIVE_ORDER
Model Constructor Detail

String

protected String(JMLValueSequence seq)
Specifications: pure
protected normal_behavior
requires seq != null;
assignable stringSeq;
ensures this.stringSeq.equals(seq);
Constructor Detail

String

public String()
Specifications: pure
public normal_behavior
assignable stringSeq;
ensures this.stringSeq.equals(new org.jmlspecs.models.JMLValueSequence());
     also
public normal_behavior
assignable charArray;
ensures this.charArray != null;
ensures this.charArray.length == 0;

String

public String(String original)
Specifications: pure
public normal_behavior
requires original != null;
assignable stringSeq;
ensures this.stringSeq.equals(original.stringSeq);
     also
public normal_behavior
requires original != null;
assignable charArray;
ensures this.charArray != null;
ensures equal(this.charArray,original.charArray);

String

public String(non_null char[] value)
Specifications: pure
public normal_behavior
requires value != null;
assignable stringSeq;
ensures ( \forall int i; 0 <= i&&i < value.length; ((org.jmlspecs.models.JMLChar)(this.stringSeq.itemAt(i))).charValue() == value[i]);
ensures_redundantly this.stringSeq.equals(new java.lang.String(value, 0, value.length).stringSeq);
     also
public normal_behavior
requires value != null;
assignable charArray;
ensures this.charArray != null;
ensures equal(this.charArray,value);

String

public String(non_null char[] value,
              int offset,
              int count)
       throws StringIndexOutOfBoundsException
Throws:
StringIndexOutOfBoundsException
Specifications: pure
public normal_behavior
requires value != null&&0 <= offset&&(offset+count) < value.length&&0 <= count;
assignable stringSeq;
ensures ( \forall int i; offset <= i&&i < offset+count; ((org.jmlspecs.models.JMLChar)(this.stringSeq.itemAt((int)(i-offset)))).charValue() == value[i]);
     also
public exceptional_behavior
requires value != null&&(offset < 0||(offset+count) < value.length||count < 0);
signals_only java.lang.StringIndexOutOfBoundsException;
     also
public normal_behavior
requires value != null&&0 <= offset&&(offset+count) < value.length&&0 <= count;
assignable charArray;
ensures this.charArray != null;
ensures equal(this.charArray,0,value,offset,count);
ensures this.charArray.length == count;
     also
public exceptional_behavior
requires value != null&&(offset < 0||(offset+count) < value.length||count < 0);
signals_only java.lang.StringIndexOutOfBoundsException;

String

public String(non_null byte[] ascii,
              int hibyte,
              int offset,
              int count)
       throws StringIndexOutOfBoundsException
Deprecated. as of 1.1

Throws:
StringIndexOutOfBoundsException
Specifications: pure
public normal_behavior
requires ascii != null&&0 <= offset&&(offset+count) < ascii.length&&0 <= count;
assignable stringSeq;
ensures this.charArray != null;
ensures ( \forall int i; offset <= i&&i < offset+count; ((org.jmlspecs.models.JMLChar)(this.stringSeq.itemAt((int)(i-offset)))).charValue() == this.byteToChar(hibyte,ascii[i]));
     also
public exceptional_behavior
requires ascii != null&&(offset < 0||(offset+count) < ascii.length||count < 0);
signals_only java.lang.StringIndexOutOfBoundsException;
     also
public normal_behavior
requires ascii != null&&0 <= offset&&(offset+count) < ascii.length&&0 <= count;
ensures this.charArray != null;
ensures this.charArray.length == count;
ensures ( \forall int i; 0 <= i&&i < count; (this.charArray[i] == this.byteToChar(hibyte,ascii[i+offset])));
     also
public exceptional_behavior
requires ascii != null&&(offset < 0||(offset+count) < ascii.length||count < 0);
signals_only java.lang.StringIndexOutOfBoundsException;

String

public String(non_null byte[] ascii,
              int hibyte)
Deprecated. as of 1.1

Specifications: pure
public normal_behavior
requires ascii != null;
assignable stringSeq;
ensures this.charArray != null;
ensures ( \forall int i; 0 <= i&&i < ascii.length; ((org.jmlspecs.models.JMLChar)(this.stringSeq.itemAt(i))).charValue() == this.byteToChar(hibyte,ascii[i]));
     also
public normal_behavior
requires ascii != null;
ensures this.charArray != null;
ensures this.charArray.length == ascii.length;
ensures ( \forall int i; 0 <= i&&i < ascii.length; this.charArray[i] == this.byteToChar(hibyte,ascii[i]));

String

public String(non_null byte[] bytes,
              int offset,
              int length,
              non_null String charsetName)
       throws UnsupportedEncodingException
Throws:
UnsupportedEncodingException
Specifications: pure
public behavior
requires bytes != null&&charsetName != null&&0 <= offset&&(offset+length) < bytes.length&&0 <= length;
{|
requires (* charsetName is the name of a supporting encoding *);
assignable stringSeq;
ensures this.charArray != null;
ensures this.stringSeq.int_length() <= length&&( \forall int i; 0 <= i&&i < this.stringSeq.int_length(); (* stringSeq.itemAt(i).charValue() == char at position i of the conversion of subarray of bytes using the encoding charsetName *));
signals (java.lang.Exception) false;
also
requires (* !(charsetName is the name of a supporting encoding) *);
ensures false;
signals_only java.io.UnsupportedEncodingException;
|}
     also
ensures this.charArray.length == length;

String

public String(non_null byte[] bytes,
              non_null String charsetName)
       throws UnsupportedEncodingException
Throws:
UnsupportedEncodingException
Specifications: pure
public normal_behavior
requires bytes != null&&charsetName != null&&(* charsetName is the name of a supporting encoding *);
assignable stringSeq;
ensures this.stringSeq.equals(new java.lang.String(bytes, 0, bytes.length, charsetName));
     also
public exceptional_behavior
requires bytes != null&&charsetName != null&&(* !(charsetName is the name of a supporting encoding) *);
signals_only java.io.UnsupportedEncodingException;
     also
public normal_behavior
requires bytes != null&&charsetName != null;
ensures this.charArray != null;
ensures this.charArray.length == bytes.length;

String

public String(non_null byte[] bytes,
              int offset,
              int length)
Specifications: pure
public normal_behavior
requires bytes != null&&0 <= offset&&(offset+length) < bytes.length&&0 <= length;
assignable stringSeq;
ensures this.stringSeq.equals(new java.lang.String(bytes, offset, length, java.lang.System.getProperty("file.encoding")));
     also
ensures this.charArray != null;
ensures this.charArray.length == length;

String

public String(non_null byte[] bytes)
Specifications: pure
public normal_behavior
requires bytes != null;
assignable stringSeq;
ensures this.stringSeq.equals(new java.lang.String(bytes, 0, bytes.length, java.lang.System.getProperty("file.encoding")));
     also
public normal_behavior
requires bytes != null;
ensures this.charArray != null;
ensures this.charArray.length == bytes.length;

String

public String(non_null StringBuffer buffer)
Specifications: pure
public normal_behavior
requires buffer != null;
assignable stringSeq;
ensures this.stringSeq != null&&this.stringSeq.equals(buffer.accumulatedString.stringSeq);
     also
public normal_behavior
requires buffer != null;
ensures this.equals(buffer.accumulatedString);

String

String(int offset,
       int count,
       char[] value)
Specifications: pure
normal_behavior
requires value != null;
requires 0 <= offset&&0 <= count&&offset+count <= value.length;
ensures this.charArray != null;
ensures this.charArray.length == count;
ensures java.lang.CharSequence.equal(this.charArray,0,value,offset,count);
Model Method Detail

byteToChar

public char byteToChar(int hibyte,
                       byte ascii)
Specifications: pure
public normal_behavior
ensures \result == (char)(((hibyte&255) << 8)|(ascii&255));

byteArraysEqual

public boolean byteArraysEqual(byte[] a,
                               byte[] b)
Specifications: pure
public normal_behavior
ensures \result == (a.length == b.length)&&( \forall int i; 0 <= i&&i < a.length; a[i] == b[i]);

charEqualsIgnoreCase

public static boolean charEqualsIgnoreCase(char c1,
                                           char c2)
Specifications: pure
public normal_behavior
ensures \result <==> (c1 == c2)||(java.lang.Character.toUpperCase(c1) == java.lang.Character.toUpperCase(c2))||(java.lang.Character.toLowerCase(c1) == java.lang.Character.toLowerCase(c2));

lessThan

public static boolean lessThan(JMLValueSequence s1,
                               JMLValueSequence s2)
Specifications: pure
public normal_behavior
requires s1 != null&&s2 != null&&( \forall int i; 0 <= i&&i < s1.int_length(); (s1.itemAt(i) instanceof org.jmlspecs.models.JMLChar))&&( \forall int i; 0 <= i&&i < s2.int_length(); (s2.itemAt(i) instanceof org.jmlspecs.models.JMLChar));
{|
requires s2.isEmpty()&&s1.isEmpty();
ensures !\result ;
also
requires s1.isEmpty()&&!s2.isEmpty();
ensures \result ;
also
requires !s1.isEmpty()&&s2.isEmpty();
ensures !\result ;
also
requires ((org.jmlspecs.models.JMLChar)s1.first()).charValue() < ((org.jmlspecs.models.JMLChar)s2.first()).charValue();
ensures \result ;
also
requires ((org.jmlspecs.models.JMLChar)s1.first()).charValue() > ((org.jmlspecs.models.JMLChar)s2.first()).charValue();
ensures !\result ;
also
requires ((org.jmlspecs.models.JMLChar)s1.first()).charValue() == ((org.jmlspecs.models.JMLChar)s2.first()).charValue();
ensures \result == lessThan(s1.trailer(),s2.trailer());
|}

lessThan

public static boolean lessThan(char[] s1,
                               char[] s2)
Specifications: pure
public normal_behavior
requires s1 != null&&s2 != null;
{|
requires s2.length == 0&&s1.length == 0;
ensures !\result ;
also
requires s1.length == 0&&s2.length != 0;
ensures \result ;
also
requires s1.length != 0&&s2.length == 0;
ensures !\result ;
also
requires s1.length > 0&&s2.length > 0&&s1[0] != s2[0];
ensures \result == (s1[0] < s2[0]);
also
ensures \result == (( \exists int i; 0 <= i&&i < s1.length&&i < s2.length; s1[i] < s2[i]&&equal(s1,0,s2,0,i))||(s1.length < s2.length&&equal(s1,0,s2,0,s1.length)));
|}

lessThanIgnoreCase

public static boolean lessThanIgnoreCase(JMLValueSequence s1,
                                         JMLValueSequence s2)
Specifications: pure
public normal_behavior
forall org.jmlspecs.models.JMLValueSequence s1up;
forall org.jmlspecs.models.JMLValueSequence s2up;
forall org.jmlspecs.models.JMLValueSequence s1down;
forall org.jmlspecs.models.JMLValueSequence s2down;
requires s1 != null&&s2 != null;
requires s1up != null&&s2up != null&&s1down != null&&s2down != null&&s1up.int_length() == s1.int_length()&&s1down.int_length() == s1.int_length()&&s2up.int_length() == s2.int_length()&&s2down.int_length() == s2.int_length();
requires ( \forall int i; 0 <= i&&i < s1.int_length(); (s1.itemAt(i) instanceof org.jmlspecs.models.JMLChar)&&(s1up.itemAt(i) instanceof org.jmlspecs.models.JMLChar)&&(s1down.itemAt(i) instanceof org.jmlspecs.models.JMLChar)&&java.lang.Character.toUpperCase(((org.jmlspecs.models.JMLChar)(s1.itemAt(i))).charValue()) == ((org.jmlspecs.models.JMLChar)(s1up.itemAt(i))).charValue()&&java.lang.Character.toLowerCase(((org.jmlspecs.models.JMLChar)(s1.itemAt(i))).charValue()) == ((org.jmlspecs.models.JMLChar)(s1down.itemAt(i))).charValue())&&( \forall int i; 0 <= i&&i < s2.int_length(); (s2.itemAt(i) instanceof org.jmlspecs.models.JMLChar)&&(s2up.itemAt(i) instanceof org.jmlspecs.models.JMLChar)&&(s2down.itemAt(i) instanceof org.jmlspecs.models.JMLChar)&&java.lang.Character.toUpperCase(((org.jmlspecs.models.JMLChar)(s2.itemAt(i))).charValue()) == ((org.jmlspecs.models.JMLChar)(s2up.itemAt(i))).charValue()&&java.lang.Character.toLowerCase(((org.jmlspecs.models.JMLChar)(s2.itemAt(i))).charValue()) == ((org.jmlspecs.models.JMLChar)(s2down.itemAt(i))).charValue());
ensures \result <==> lessThan(s1,s2)||lessThan(s1up,s2up)||lessThan(s1down,s2down);
Method Detail

length

public int length()
Specified by:
length in interface CharSequence
Specifications: pure
     also
public normal_behavior
ensures \result == this.stringSeq.int_length();
     also
public normal_behavior
ensures \result == this.charArray.length;
Specifications inherited from overridden method in interface CharSequence:
public normal_behavior
assignable objectState;
ensures \result >= 0;
ensures \result == this.charArray.length;

charAt

public char charAt(int index)
            throws StringIndexOutOfBoundsException
Specified by:
charAt in interface CharSequence
Throws:
StringIndexOutOfBoundsException
Specifications: pure
     also
public normal_behavior
requires 0 <= index&&index < this.length();
ensures \result == ((org.jmlspecs.models.JMLChar)(this.stringSeq.itemAt(index))).charValue();
     also
public exceptional_behavior
requires index < 0||index >= this.length();
signals_only java.lang.StringIndexOutOfBoundsException;
     also
public normal_behavior
requires 0 <= index&&index < this.charArray.length;
ensures \result == this.charArray[index];
     also
public exceptional_behavior
requires index < 0||index >= this.charArray.length;
signals_only java.lang.StringIndexOutOfBoundsException;
Specifications inherited from overridden method charAt(int index) in interface CharSequence:
public normal_behavior
requires 0 <= index&&index < this.charArray.length;
assignable objectState;
ensures \result == this.charArray[index];
     also
public exceptional_behavior
requires !(0 <= index&&index < this.charArray.length);
assignable objectState;
signals_only java.lang.IndexOutOfBoundsException;

getChars

public void getChars(int srcBegin,
                     int srcEnd,
                     char[] dst,
                     int dstBegin)
              throws StringIndexOutOfBoundsException
Throws:
StringIndexOutOfBoundsException
Specifications:
public normal_behavior
requires srcBegin >= 0&&srcEnd <= this.length()&&srcBegin <= srcEnd&&dst != null&&dst.length >= dstBegin+(srcEnd-srcBegin);
assignable dst[dstBegin .. dstBegin+srcEnd-srcBegin-1];
ensures ( \forall int i; srcBegin <= i&&i < srcEnd; dst[(int)(dstBegin+i-srcBegin)] == this.charAt(i));
     also
public exceptional_behavior
requires (srcBegin < 0||srcEnd > this.length()||srcBegin > srcEnd)&&dst != null&&dst.length >= dstBegin+(srcEnd-srcBegin);
assignable \nothing;
signals_only java.lang.StringIndexOutOfBoundsException;
     also
public normal_behavior
requires srcBegin >= 0&&srcEnd <= this.charArray.length&&srcBegin <= srcEnd&&dst != null&&dst.length >= dstBegin+(srcEnd-srcBegin);
assignable dst[dstBegin .. dstBegin+srcEnd-srcBegin-1];
ensures equal(this.charArray,srcBegin,dst,dstBegin,srcEnd-srcBegin);
     also
public exceptional_behavior
requires (srcBegin < 0||srcEnd > this.charArray.length||srcBegin > srcEnd)&&dst != null&&dst.length >= dstBegin+(srcEnd-srcBegin);
assignable \nothing;
signals_only java.lang.StringIndexOutOfBoundsException;

getBytes

public void getBytes(int srcBegin,
                     int srcEnd,
                     byte[] dst,
                     int dstBegin)
              throws StringIndexOutOfBoundsException
Deprecated. as of 1.1, use getBytes()

Throws:
StringIndexOutOfBoundsException
Specifications:
public normal_behavior
requires srcBegin >= 0&&srcEnd <= this.length()&&srcBegin <= srcEnd&&dst != null&&dst.length >= dstBegin+(srcEnd-srcBegin)+1;
assignable dst[dstBegin .. dstBegin+srcEnd-srcBegin-1];
ensures ( \forall int i; srcBegin <= i&&i < srcEnd; dst[(int)(dstBegin+i-srcBegin)] == (byte)(this.charAt(i)&255));
     also
public exceptional_behavior
requires (srcBegin <= 0||srcEnd > this.length()||srcBegin > srcEnd)&&dst != null&&dst.length >= dstBegin+(srcEnd-srcBegin)+1;
assignable \nothing;
signals_only java.lang.StringIndexOutOfBoundsException;

getBytes

public byte[] getBytes(String charsetName)
                throws UnsupportedEncodingException
Throws:
UnsupportedEncodingException
Specifications: pure non_null
public normal_behavior
requires charsetName != null&&(* charsetName is the name of a supporting encoding *);
ensures \result != null&&( \forall int i; 0 <= i&&i < \result .length; (* \result[i] is the byte at position i of the conversion of this string's chars using charsetName *));
     also
public exceptional_behavior
requires charsetName != null&&!(* (charsetName is the name of a supporting encoding) *);
signals_only java.io.UnsupportedEncodingException;

getBytes

public byte[] getBytes()
Specifications: pure non_null
public normal_behavior
ensures \result != null&&this.byteArraysEqual(\result ,this.getBytes(java.lang.System.getProperty("file.encoding")));
     also
public normal_behavior
ensures \result != null&&\result .length == this.charArray.length;

equals

public boolean equals(nullable Object anObject)
Description copied from interface: CharSequence
According to the javadocs, the equals method should not be called.

Specified by:
equals in interface CharSequence
Overrides:
equals in class Object
Specifications: pure
     also
public normal_behavior
requires anObject != null&&(anObject instanceof java.lang.String);
ensures \result == (this.stringSeq.equals(((java.lang.String)anObject).stringSeq));
     also
public normal_behavior
requires anObject != null&&(anObject instanceof java.lang.String);
ensures \result == equal(this.charArray,((java.lang.String)anObject).charArray);
     also
requires this == anObject;
ensures \result ;
     also
requires anObject == null||!(anObject instanceof java.lang.String);
ensures !\result ;
Specifications inherited from overridden method equals(Object obj) in class Object:
       pure
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
     also
public normal_behavior
requires this == obj;
ensures \result ;
     also
public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
     also
diverges false;
ensures obj == null ==> !\result ;
Specifications inherited from overridden method equals(Object obj) in interface CharSequence:
     also
requires false;

contentEquals

public boolean contentEquals(StringBuffer sb)
Specifications: pure

equalsIgnoreCase

public boolean equalsIgnoreCase(String anotherString)
Specifications: pure
public normal_behavior
requires anotherString != null;
ensures \result <==> (this.length() == anotherString.length())&&( \forall int i; 0 <= i&&i < this.length(); charEqualsIgnoreCase(this.charAt(i),anotherString.charAt(i)));
     also
requires anotherString == null;
ensures !\result ;

compareTo

public int compareTo(non_null String anotherString)
Specifications: pure
public normal_behavior
requires anotherString != null;
{|
requires this.stringSeq.equals(anotherString.stringSeq);
ensures \result == 0;
also
requires lessThan(this.stringSeq,anotherString.stringSeq);
ensures \result < 0;
also
requires !lessThan(this.stringSeq,anotherString.stringSeq)&&!this.stringSeq.equals(anotherString.stringSeq);
ensures \result > 0;
|}
     also
public normal_behavior
requires anotherString != null;
{|
requires equal(this.charArray,anotherString.charArray);
ensures \result == 0;
also
requires lessThan(this.charArray,anotherString.charArray);
ensures \result < 0;
also
requires !lessThan(this.charArray,anotherString.charArray);
requires !equal(this.charArray,anotherString.charArray);
ensures \result > 0;
|}
Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure
public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
     also
public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

compareTo

public int compareTo(non_null Object o)
Specified by:
compareTo in interface Comparable
Specifications: pure
     also
public normal_behavior
requires o != null&&(o instanceof java.lang.String);
ensures \result == this.compareTo((java.lang.String)o);
     also
public exceptional_behavior
requires o == null&&!(o instanceof java.lang.String);
signals_only java.lang.ClassCastException;
Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
       pure
public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
     also
public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

compareToIgnoreCase

public int compareToIgnoreCase(nullable String str)
Specifications: pure
public normal_behavior
requires str != null;
{|
requires this.equalsIgnoreCase(str);
ensures \result == 0;
also
requires lessThanIgnoreCase(this.stringSeq,str.stringSeq);
ensures \result < 0;
also
requires !lessThanIgnoreCase(this.stringSeq,str.stringSeq)&&!this.stringSeq.equals(str.stringSeq);
ensures \result > 0;
|}

regionMatches

public boolean regionMatches(int toffset,
                             String other,
                             int ooffset,
                             int len)
Specifications: pure
public normal_behavior
requires other != null;
ensures \result == this.regionMatches(false,toffset,other,ooffset,len);

regionMatches

public boolean regionMatches(boolean ignoreCase,
                             int toffset,
                             String other,
                             int ooffset,
                             int len)
Specifications: pure
public normal_behavior
requires other != null;
{|
requires (0 <= toffset&&(toffset+len) <= this.length())&&(0 <= ooffset&&(ooffset+len) <= other.length())&&ignoreCase;
ensures \result == this.substring(toffset,(int)(toffset+len)).equalsIgnoreCase(other.substring(ooffset,(int)(ooffset+len)));
also
requires (0 <= toffset&&(toffset+len) <= this.length())&&(0 <= ooffset&&(ooffset+len) <= other.length())&&!ignoreCase;
ensures \result == this.substring(toffset,(int)(toffset+len)).equals(other.substring(ooffset,(int)(ooffset+len)));
also
requires (toffset < 0||(toffset+len) > this.length())||(toffset < 0||(ooffset+len) > other.length());
ensures !\result ;
|}

startsWith

public boolean startsWith(String prefix,
                          int toffset)
Specifications: pure
public normal_behavior
requires prefix != null&&toffset < this.length();
ensures \result == this.substring(toffset).stringSeq.isPrefix(prefix.stringSeq);
     also
public normal_behavior
requires prefix != null&&toffset < this.length();
ensures \result == equal(this.charArray,toffset,prefix.charArray,0,prefix.charArray.length);
     also
requires prefix != null&&toffset >= this.length();
ensures !\result ;

startsWith

public boolean startsWith(String prefix)
Specifications: pure
public normal_behavior
requires prefix != null;
ensures \result == this.startsWith(prefix,0);

endsWith

public boolean endsWith(String suffix)
Specifications: pure
public normal_behavior
requires suffix != null&&suffix.length() <= this.length();
ensures \result == this.substring((int)(this.length()-suffix.length())).equals(suffix);
     also
requires suffix != null&&suffix.length() > this.length();
ensures !\result ;

hashCode

public int hashCode()
Description copied from interface: CharSequence
According to the javadocs, the hashCode method should not be called.

Specified by:
hashCode in interface CharSequence
Overrides:
hashCode in class Object
Specifications inherited from overridden method in class Object:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public code normal_behavior
assignable \nothing;
Specifications inherited from overridden method in interface CharSequence:
     also
requires false;
assignable objectState;

indexOf

public int indexOf(int ch)
Specifications: pure
public normal_behavior
ensures \result == this.indexOf(ch,0);

indexOf

public int indexOf(int ch,
                   int fromIndex)
Specifications: pure
public normal_behavior
requires fromIndex >= this.length();
ensures \result == -1;
     also
requires fromIndex < 0;
ensures \result == this.indexOf(ch,0);
     also
requires 0 <= fromIndex&&fromIndex < this.length();
{|
requires this.charAt(fromIndex) == ch;
ensures \result == fromIndex;
also
requires this.charAt(fromIndex) != ch;
ensures \result == this.indexOf(ch,(int)(fromIndex+1));
also
ensures \result == -1 <==> ( \forall int i; fromIndex <= i&&i < this.charArray.length; this.charArray[i] != ch);
ensures \result != -1 <==> (fromIndex <= \result &&\result < this.charArray.length);
ensures \result != -1 <==> (this.charArray[\result ] == ch&&( \forall int i; fromIndex <= i&&i < \result ; this.charArray[i] != ch));
|}

lastIndexOf

public int lastIndexOf(int ch)
Specifications: pure
public normal_behavior
ensures \result == this.lastIndexOf(ch,(int)(this.length()-1));

lastIndexOf

public int lastIndexOf(int ch,
                       int fromIndex)
Specifications: pure
public normal_behavior
{|
requires fromIndex >= this.length();
ensures \result == this.lastIndexOf(ch,(int)(this.length()-1));
also
requires fromIndex < 0;
ensures \result == -1;
also
requires 0 <= fromIndex&&fromIndex < this.length();
{|
requires this.charAt(fromIndex) == ch;
ensures \result == fromIndex;
also
requires this.charAt(fromIndex) != ch;
ensures \result == this.lastIndexOf(ch,(int)(fromIndex-1));
also
ensures \result == -1 <==> ( \forall int i; 0 <= i&&i <= fromIndex; this.charArray[i] != ch);
ensures \result != -1 <==> (0 <= \result &&\result < fromIndex);
ensures \result != -1 <==> (this.charArray[\result ] == ch&&( \forall int i; \result < i&&i <= fromIndex; this.charArray[i] != ch));
|}
|}

indexOf

public int indexOf(String str)
Specifications: pure
public normal_behavior
requires str != null;
ensures \result == this.indexOf(str,0);

indexOf

public int indexOf(String str,
                   int fromIndex)
Specifications: pure
public normal_behavior
requires str != null;
{|
requires fromIndex >= this.length();
ensures \result == -1;
also
requires fromIndex < 0;
ensures \result == this.indexOf(str,0);
also
requires 0 <= fromIndex&&fromIndex < this.length();
{|
requires this.stringSeq.removePrefix(fromIndex).isPrefix(str.stringSeq);
ensures \result == fromIndex;
also
requires !this.stringSeq.removePrefix(fromIndex).isPrefix(str.stringSeq);
ensures \result == this.indexOf(str,(int)(fromIndex+1));
|}
also
requires 0 <= fromIndex&&fromIndex < this.length();
ensures \result == -1 <==> ( \forall int i; fromIndex <= i&&i+str.length() < this.length(); !equal(this.charArray,i,str.charArray,0,str.length()));
ensures \result != -1 <==> (fromIndex <= \result &&\result +str.length() <= this.length());
ensures \result != -1 <==> (equal(this.charArray,\result ,str.charArray,0,str.length())&&( \forall int i; fromIndex <= i&&i+str.length() < this.length(); !equal(this.charArray,i,str.charArray,0,str.length())));
|}

indexOf

static int indexOf(char[] source,
                   int sourceOffset,
                   int sourceCount,
                   char[] target,
                   int targetOffset,
                   int targetCount,
                   int fromIndex)
Specifications: pure

lastIndexOf

public int lastIndexOf(String str)
Specifications: pure
public normal_behavior
requires str != null;
ensures \result == this.lastIndexOf(str,(int)(this.length()-1));

lastIndexOf

public int lastIndexOf(String str,
                       int fromIndex)
Specifications: pure
public normal_behavior
requires str != null;
{|
requires fromIndex >= this.length();
ensures \result == this.lastIndexOf(str,(int)(this.length()-1));
also
requires fromIndex < 0;
ensures \result == -1;
also
requires 0 <= fromIndex&&fromIndex < this.length();
{|
requires this.stringSeq.removePrefix(fromIndex).isPrefix(str.stringSeq);
ensures \result == fromIndex;
also
requires !this.stringSeq.removePrefix(fromIndex).isPrefix(str.stringSeq);
ensures \result == this.indexOf(str,(int)(fromIndex-1));
|}
also
requires 0 <= fromIndex&&fromIndex < this.length();
ensures \result == -1 <==> ( \forall int i; 0 <= i&&i <= fromIndex; !equal(this.charArray,i,str.charArray,0,str.length()));
ensures \result != -1 <==> (0 <= \result &&\result <= fromIndex);
ensures \result != -1 <==> (equal(this.charArray,\result ,str.charArray,0,str.length())&&( \forall int i; 0 <= i&&i <= fromIndex; !equal(this.charArray,i,str.charArray,0,str.length())));
|}

lastIndexOf

static int lastIndexOf(char[] source,
                       int sourceOffset,
                       int sourceCount,
                       char[] target,
                       int targetOffset,
                       int targetCount,
                       int fromIndex)
Specifications: pure

substring

public String substring(int beginIndex)
                 throws StringIndexOutOfBoundsException
Throws:
StringIndexOutOfBoundsException
Specifications: pure non_null
public normal_behavior
requires 0 <= beginIndex;
requires beginIndex <= this.length();
ensures \result == this.substring(beginIndex,this.length());
     also
public exceptional_behavior
requires beginIndex < 0||beginIndex > this.length();
signals_only java.lang.StringIndexOutOfBoundsException;

substring

public String substring(int beginIndex,
                        int endIndex)
                 throws StringIndexOutOfBoundsException
Throws:
StringIndexOutOfBoundsException
Specifications: pure non_null
public normal_behavior
requires 0 <= beginIndex&&beginIndex <= endIndex&&(endIndex <= this.length());
ensures \result != null&&\result .stringSeq.equals(this.stringSeq.subsequence(beginIndex,endIndex));
     also
public normal_behavior
requires 0 <= beginIndex&&beginIndex <= endIndex&&(endIndex <= this.length());
ensures \result != null&&\fresh(\result )&&\result .length() == endIndex-beginIndex&&equal(\result .charArray,0,this.charArray,beginIndex,endIndex-beginIndex);
     also
public exceptional_behavior
requires 0 > beginIndex||beginIndex > endIndex||(endIndex > this.length());
signals_only java.lang.StringIndexOutOfBoundsException;

subSequence

public CharSequence subSequence(int beginIndex,
                                int endIndex)
Specified by:
subSequence in interface CharSequence
Specifications: pure
     also
public exceptional_behavior
requires 0 > beginIndex||beginIndex > endIndex||(endIndex > this.length());
signals_only java.lang.StringIndexOutOfBoundsException;
Specifications inherited from overridden method subSequence(int start, int end) in interface CharSequence:
public normal_behavior
requires 0 <= start&&start <= end&&end <= this.charArray.length;
assignable objectState;
ensures \result .charArray.length == end-start;
ensures equal(\result .charArray,0,this.charArray,start,end-start);
     also
public exceptional_behavior
requires start < 0||end < start||end > this.charArray.length;
assignable objectState;
signals_only java.lang.IndexOutOfBoundsException;

concat

public String concat(non_null String str)
Specifications: pure non_null
public normal_behavior
requires str != null;
ensures \result != null&&\result .stringSeq.equals(this.stringSeq.concat(str.stringSeq));
     also
public normal_behavior
requires str != null;
ensures \result != null&&\fresh(\result )&&\result .length() == this.length()+str.length()&&equal(\result .charArray,0,this.charArray,0,this.length())&&equal(\result .charArray,this.length(),str.charArray,0,str.length());

replace

public String replace(char oldChar,
                      char newChar)
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .length() == this.length()&&\fresh(\result )&&( \forall int i; 0 <= i&&i < this.length(); \result .charAt(i) == ((this.charAt(i) == oldChar) ? newChar : this.charAt(i)));

matches

public boolean matches(non_null String regex)
Specifications: pure
public normal_behavior
requires regex != null;
assignable \nothing;
ensures \result <==> java.util.regex.Pattern.matches(regex,this);

replaceFirst

public String replaceFirst(non_null String regex,
                           non_null String replacement)
Specifications: pure non_null
public normal_behavior
requires regex != null&&replacement != null;
assignable \nothing;
ensures \result .equals(java.util.regex.Pattern.compile(regex).matcher(this).replaceFirst(replacement));

replaceAll

public String replaceAll(non_null String regex,
                         non_null String replacement)
Specifications: pure non_null
public normal_behavior
requires regex != null&&replacement != null;
assignable \nothing;
ensures \result .equals(java.util.regex.Pattern.compile(regex).matcher(this).replaceAll(replacement));

split

public String[] split(non_null String regex,
                      int limit)
Specifications: pure non_null
public normal_behavior
requires regex != null;
assignable \nothing;
ensures \result .equals(java.util.regex.Pattern.compile(regex).split(this,limit));

split

public String[] split(non_null String regex)
Specifications: pure non_null
public normal_behavior
requires regex != null;
assignable \nothing;
ensures \result .equals(this.split(regex,0));

toLowerCase

public String toLowerCase(non_null Locale locale)
Specifications: pure non_null
public normal_behavior
requires locale != null;
ensures \fresh(\result )&&\result .length() == this.length();
ensures (* \result == a lower case conversion of this using the rules of the given locale *);

toLowerCase

public String toLowerCase()
Specifications: pure non_null
public normal_behavior
ensures \fresh(\result )&&\result .length() == this.length();
ensures \result != null&&\result .equals(this.toLowerCase(java.util.Locale.getDefault()));

toUpperCase

public String toUpperCase(non_null Locale locale)
Specifications: pure non_null
public normal_behavior
requires locale != null;
ensures \fresh(\result )&&\result .length() == this.length();
ensures (* \result == an upper case conversion of this using the rules of the given locale *);

toUpperCase

public String toUpperCase()
Specifications: pure non_null
public normal_behavior
ensures \fresh(\result )&&\result .length() == this.length();
ensures \result != null&&\result .equals(this.toUpperCase(java.util.Locale.getDefault()));

trim

public String trim()
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .length() <= this.length()&&\result .charAt(0) > 32&&\result .charAt((int)(\result .length()-1)) > 32;

toString

public String toString()
Specified by:
toString in interface CharSequence
Overrides:
toString in class Object
Specifications: pure non_null
     also
public normal_behavior
ensures \result != null&&\result == this;
Specifications inherited from overridden method in class Object:
       non_null
public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
     also
public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);
     also
public code model_program { ... }
    implies_that
assignable objectState;
ensures \result != null;
Specifications inherited from overridden method in interface CharSequence:
       non_null
     also
public normal_behavior
assignable objectState;
ensures \result != null&&equal(\result .charArray,this.charArray);

toCharArray

public char[] toCharArray()
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .length == this.length()&&( \forall int i; 0 <= i&&i < this.length(); \result [i] == this.charAt(i));
ensures \fresh(\result );
ensures equal(\result ,this.charArray);

valueOf

public static String valueOf(Object obj)
Specifications: pure non_null
public normal_behavior
{|
requires obj == null;
ensures \result != null&&\result .equals("null");
also
requires obj != null;
ensures \result != null;
also
requires obj instanceof java.lang.String;
ensures \result .equals(obj);
|}
     also
public model_program { ... }

valueOf

public static String valueOf(non_null char[] data)
Specifications: pure non_null
public normal_behavior
requires data != null;
ensures \result != null&&\result .equals(new java.lang.String(data));

valueOf

public static String valueOf(non_null char[] data,
                             int offset,
                             int count)
Specifications: pure non_null
public normal_behavior
requires data != null&&offset >= 0&&count >= 0&&offset+count < data.length;
ensures \result != null&&\result .equals(new java.lang.String(data, offset, count));

copyValueOf

public static String copyValueOf(non_null char[] data,
                                 int offset,
                                 int count)
Specifications: pure non_null
public normal_behavior
requires data != null;
ensures \result != null&&\result .equals(new java.lang.String(data, offset, count));

copyValueOf

public static String copyValueOf(non_null char[] data)
Specifications: pure non_null
public normal_behavior
requires data != null;
ensures \result != null&&\result .equals(new java.lang.String(data));

valueOf

public static String valueOf(boolean b)
Specifications: pure non_null
public normal_behavior
ensures \result != null&&(b ==> \result .equals("true")||!b ==> \result .equals("false"));

valueOf

public static String valueOf(char c)
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .length() == 1&&\result .charAt(0) == c;

valueOf

public static String valueOf(int i)
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .equals(java.lang.Integer.toString(i));

valueOf

public static String valueOf(long l)
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .equals(java.lang.Long.toString(l));

valueOf

public static String valueOf(float f)
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .equals(java.lang.Float.toString(f));

valueOf

public static String valueOf(double d)
Specifications: pure non_null
public normal_behavior
ensures \result != null&&\result .equals(java.lang.Double.toString(d));

intern

public String intern()
Specifications: pure non_null
public normal_behavior
ensures \result .isInterned;
ensures \result .equals(this);
ensures this.isInterned ==> (\result == this);
ensures_redundantly (* \result is a canonical representation for this *);
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.