java.lang
Class StringBuffer

java.lang.Object
  java.lang.StringBuffer

All Implemented Interfaces:

CharSequence, Serializable

public final class StringBuffer

extends Object

implements Serializable, CharSequence

JML's specification of StringBuffer.

Author:

David Cok, Gary T. Leavens

Class Specifications

Specifications inherited from class Object

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

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
String	accumulatedString

 

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

 

Constructor Summary

StringBuffer()

StringBuffer(int i)

StringBuffer(String s)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface java.lang.CharSequence

equal, equal

 

Method Summary
StringBuffer	append(boolean b)
StringBuffer	append(char c)
StringBuffer	append(char[] ca)
StringBuffer	append(char[] ca, int i, int j)
StringBuffer	append(double d)
StringBuffer	append(float f)
StringBuffer	append(int i)
StringBuffer	append(Object o)
StringBuffer	append(String s)
StringBuffer	append(StringBuffer s)
StringBuffer	append(long l)
int	capacity()
char	charAt(int index)
StringBuffer	delete(int i, int j)
StringBuffer	deleteCharAt(int index)
void	ensureCapacity(int minimumCapacity)
void	getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin)
int	indexOf(String str)
int	indexOf(String str, int fromIndex)
StringBuffer	insert(int offset, boolean b)
StringBuffer	insert(int offset, char c)
StringBuffer	insert(int offset, char[] ca)
StringBuffer	insert(int offset, char[] ca, int offset2, int len)
StringBuffer	insert(int offset, double d)
StringBuffer	insert(int offset, float f)
StringBuffer	insert(int offset, int i)
StringBuffer	insert(int offset, Object o)
StringBuffer	insert(int offset, String s)
StringBuffer	insert(int offset, long l)
int	lastIndexOf(String str)
int	lastIndexOf(String str, int fromIndex)
int	length()
StringBuffer	replace(int start, int end, String str)
StringBuffer	reverse()
void	setCharAt(int index, char c)
void	setLength(int i)
CharSequence	subSequence(int start, int end)
String	substring(int i)
String	substring(int start, int end)
String	toString()

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Methods inherited from interface java.lang.CharSequence

equals, hashCode

 

Model Field Detail

accumulatedString

public String accumulatedString

Specifications: non_null

StringBuffer

public StringBuffer()

Specifications: pure

public normal_behavior
ensures this.accumulatedString.equals("");

StringBuffer

public StringBuffer(int i)

Specifications: pure

public normal_behavior
ensures this.accumulatedString.equals("");

StringBuffer

public StringBuffer(String s)

Specifications: pure

public normal_behavior
requires s != null;
ensures this.accumulatedString.equals(s);

append

public StringBuffer append(char c)

Specifications:

public normal_behavior
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString+c));
ensures \result == this;

append

public StringBuffer append(boolean b)

Specifications:

public normal_behavior
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString+java.lang.String.valueOf(b)));
ensures \result == this;

append

public StringBuffer append(String s)

Specifications:

public normal_behavior
requires s != null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat(s)));
ensures \result == this;

     also

public normal_behavior
requires s == null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat("null")));
ensures \result == this;

append

public StringBuffer append(Object o)

Specifications:

public normal_behavior
requires o != null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat(o.theString)));
ensures \result == this;

     also

public normal_behavior
requires o == null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat("null")));
ensures \result == this;

    implies_that

public normal_behavior
requires o != null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString+o.theString));
ensures \result == this;

append

public StringBuffer append(StringBuffer s)

Specifications:

public normal_behavior
requires s != null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat(s.accumulatedString)));
ensures \result == this;

     also

public normal_behavior
requires s == null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat("null")));
ensures \result == this;

append

public StringBuffer append(char[] ca,
                           int i,
                           int j)

Specifications:

public normal_behavior
requires ca != null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat(java.lang.String.valueOf(ca,i,j))));
ensures \result == this;

append

public StringBuffer append(int i)

Specifications:

public normal_behavior
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString+java.lang.String.valueOf(i)));
ensures \result == this;

append

public StringBuffer append(float f)

Specifications:

public normal_behavior
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString+java.lang.String.valueOf(f)));
ensures \result == this;

append

public StringBuffer append(double d)

Specifications:

public normal_behavior
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString+java.lang.String.valueOf(d)));
ensures \result == this;

append

public StringBuffer append(char[] ca)

Specifications:

public normal_behavior
requires ca != null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat(java.lang.String.valueOf(ca))));
ensures \result == this;

     also

public normal_behavior
requires ca == null;
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.concat("null")));
ensures \result == this;

append

public StringBuffer append(long l)

Specifications:

public normal_behavior
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString+java.lang.String.valueOf(l)));
ensures \result == this;

charAt

public char charAt(int index)

Specified by:

charAt in interface CharSequence

Specifications: pure

     also

public normal_behavior
requires 0 <= index&&index < this.accumulatedString.length();
ensures \result == this.accumulatedString.charAt(index);

     also

public exceptional_behavior
requires !(0 <= index&&index < this.accumulatedString.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)

Specifications:

requires 0 <= srcBegin&&srcBegin <= srcEnd;
requires srcEnd <= this.accumulatedString.length();
requires 0 <= dstBegin&&dstBegin+srcEnd-srcBegin <= dst.length;
assignable dst[dstBegin .. dstBegin+srcEnd-srcBegin];
ensures java.lang.CharSequence.equal(this.accumulatedString.charArray,srcBegin,dst,dstBegin,srcEnd-srcBegin);

indexOf

public int indexOf(String str)

Specifications: pure

public normal_behavior
requires str != null;
ensures \result != -1 <==> (0 <= \result &&\result <= this.accumulatedString.length()-str.length());
ensures this.accumulatedString.startsWith(str,\result );
ensures ( \forall int i; 0 <= i&&i < \result ; !this.accumulatedString.startsWith(str,i));

     also

public normal_behavior
requires str != null;
requires !( \exists int k; 0 <= k&&k < this.accumulatedString.length(); this.accumulatedString.startsWith(str,k));
ensures \result == -1;

indexOf

public int indexOf(String str,
                   int fromIndex)

Specifications: pure

public normal_behavior
requires str != null;
requires ( \exists int k; 0 <= k&&k < this.accumulatedString.length(); this.accumulatedString.startsWith(str,k)&&k >= java.lang.Math.min(fromIndex,str.length()));
ensures \result == ( \min int k; 0 <= k&&k < this.accumulatedString.length()&&this.accumulatedString.startsWith(str,k)&&k >= java.lang.Math.min(fromIndex,str.length()); k);

     also

public normal_behavior
requires str != null;
requires !( \exists int k; 0 <= k&&k < this.accumulatedString.length(); this.accumulatedString.startsWith(str,k)&&k >= java.lang.Math.min(fromIndex,str.length()));
ensures \result == -1;

lastIndexOf

public int lastIndexOf(String str)

Specifications: pure

public normal_behavior
requires str != null;
requires ( \exists int k; 0 <= k&&k < this.accumulatedString.length(); this.accumulatedString.startsWith(str,k));
assignable \nothing;
ensures \result == ( \max int k; 0 <= k&&k < this.accumulatedString.length()&&this.accumulatedString.startsWith(str,k); k);

     also

public normal_behavior
requires str != null;
requires !( \exists int k; 0 <= k&&k < this.accumulatedString.length(); this.accumulatedString.startsWith(str,k));
assignable \nothing;
ensures \result == -1;

lastIndexOf

public int lastIndexOf(String str,
                       int fromIndex)

Specifications: pure

public normal_behavior
requires str != null;
requires ( \exists int k; 0 <= k&&k < this.accumulatedString.length(); this.accumulatedString.startsWith(str,k)&&k <= java.lang.Math.min(fromIndex,str.length()));
ensures \result == ( \max int k; 0 <= k&&k < this.accumulatedString.length()&&this.accumulatedString.startsWith(str,k)&&k <= java.lang.Math.min(fromIndex,str.length()); k);

     also

public normal_behavior
requires str != null;
requires !( \exists int k; 0 <= k&&k < this.accumulatedString.length(); this.accumulatedString.startsWith(str,k)&&k <= java.lang.Math.min(fromIndex,str.length()));
assignable \nothing;
ensures \result == -1;

length

public int length()

Specified by:

length in interface CharSequence

Specifications: pure

     also

public normal_behavior
ensures \result == this.accumulatedString.length();

Specifications inherited from overridden method in interface CharSequence:

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

replace

public StringBuffer replace(int start,
                            int end,
                            String str)

Specifications: non_null

subSequence

public CharSequence subSequence(int start,
                                int end)

Specified by:

subSequence in interface CharSequence

Specifications: pure non_null

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;

capacity

public int capacity()

Specifications: pure

ensureCapacity

public void ensureCapacity(int minimumCapacity)

Specifications:

ensures this.capacity() >= minimumCapacity;

deleteCharAt

public StringBuffer deleteCharAt(int index)

Specifications:

public normal_behavior
requires 0 <= index&&index < this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.subSequence(0,index).equals(\old(this.accumulatedString.subSequence(0,index)));
ensures this.accumulatedString.subSequence(index,this.accumulatedString.length()).equals(\old(this.accumulatedString.subSequence(index+1,this.accumulatedString.length())));
ensures this.accumulatedString.length() == \old(this.accumulatedString.length()-1);
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           long l)

Specifications:

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+java.lang.String.valueOf(l)+this.accumulatedString.substring(offset)));
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           char[] ca,
                           int offset2,
                           int len)

insert

public StringBuffer insert(int offset,
                           double d)

Specifications:

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+d+this.accumulatedString.substring(offset)));
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           char c)

Specifications:

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+c+this.accumulatedString.substring(offset)));
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           int i)

Specifications:

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+i+this.accumulatedString.substring(offset)));
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           char[] ca)

Specifications:

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+java.lang.String.valueOf(ca)+this.accumulatedString.substring(offset)));
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           boolean b)

Specifications:

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+b+this.accumulatedString.substring(offset)));
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           Object o)

Specifications:

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+o+this.accumulatedString.substring(offset)));
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           String s)

Specifications:

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+s+this.accumulatedString.substring(offset)));
ensures \result == this;

insert

public StringBuffer insert(int offset,
                           float f)

Specifications: non_null

public normal_behavior
requires 0 <= offset&&offset <= this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,offset)+f+this.accumulatedString.substring(offset)));
ensures \result == this;

reverse

public StringBuffer reverse()

Specifications: non_null

setCharAt

public void setCharAt(int index,
                      char c)

Specifications:

public normal_behavior
requires 0 <= index&&index < this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.equals(\old(this.accumulatedString.substring(0,index)+c+this.accumulatedString.substring(index+1)));

    implies_that

public normal_behavior
requires 0 <= index&&index < this.accumulatedString.length();
assignable accumulatedString;
ensures this.accumulatedString.length() == \old(this.accumulatedString.length())&&( \forall int i; 0 <= i&&i < this.accumulatedString.length()&&i != index; this.accumulatedString.charAt(i) == \old(this.accumulatedString.charAt(i)))&&this.accumulatedString.charAt(index) == c;

toString

public String toString()

Specified by:

toString in interface CharSequence

Overrides:

toString in class Object

Specifications: non_null

     also

public normal_behavior
assignable \nothing;
ensures \result .equals(this.accumulatedString);

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);

setLength

public void setLength(int i)

delete

public StringBuffer delete(int i,
                           int j)

Specifications: non_null

substring

public String substring(int i)

Specifications: non_null

substring

public String substring(int start,
                        int end)

Specifications: non_null