java.lang
Interface CharSequence

All Known Implementing Classes:

String, StringBuffer

public interface CharSequence

JML's specification of java.lang.CharSequence.

Version:

$Revision: 1.14 $

Author:

Gary T. Leavens

Class Specifications

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;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
[instance]  char[]	charArray

 

Model Method Summary
static boolean	equal(char[] a, char[] b)
static boolean	equal(char[] a, int astart, char[] b, int bstart, int length)

 

Method Summary
char	charAt(int index)
boolean	equals(nullable Object obj)           According to the javadocs, the equals method should not be called.
int	hashCode()           According to the javadocs, the hashCode method should not be called.
int	length()
CharSequence	subSequence(int start, int end)
String	toString()

 

Model Field Detail

charArray

public char[] charArray

Specifications: instance

equal

public static boolean equal(char[] a,
                            char[] b)

Specifications: pure

public normal_behavior
ensures \result == (a == b||(a != null&&b != null&&a.length == b.length&&( \forall int i; 0 <= i&&i < a.length; a[i] == b[i])));

equal

public static boolean equal(char[] a,
                            int astart,
                            char[] b,
                            int bstart,
                            int length)

Specifications: pure

public normal_behavior
requires a != null&&b != null&&astart >= 0&&bstart >= 0&&length >= 0&&astart+length <= a.length&&bstart+length <= b.length;
ensures \result == ((a == b&&astart == bstart)||( \forall int i; 0 <= i&&i < length; a[i+astart] == b[i+bstart]));

length

public int length()

Specifications:

public normal_behavior
assignable objectState;
ensures \result >= 0;
ensures \result == this.charArray.length;

charAt

public char charAt(int index)
                     throws IndexOutOfBoundsException

Throws:

IndexOutOfBoundsException

Specifications:

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;

subSequence

public CharSequence subSequence(int start,
                                int end)
                                  throws IndexOutOfBoundsException

Throws:

IndexOutOfBoundsException

Specifications:

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;

toString

public String toString()

Overrides:

toString in class Object

Specifications: non_null

     also

public normal_behavior
assignable objectState;
ensures \result != null&&equal(\result .charArray,this.charArray);

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;

equals

public boolean equals(nullable Object obj)

According to the javadocs, the equals method should not be called.

Overrides:

equals in class Object

Specifications: (inherited)pure

     also

requires false;

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 ;

hashCode

public int hashCode()

According to the javadocs, the hashCode method should not be called.

Overrides:

hashCode in class Object

Specifications:

     also

requires false;
assignable objectState;

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;