// @(#)$Id: StringBuffer.jml 71988 2008-07-14 22:50:44Z chalin $

// Copyright (C) 2004 Iowa State University

// This file is part of JML

// JML is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2, or (at your option)
// any later version.

// JML is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.

// You should have received a copy of the GNU General Public License
// along with JML; see the file COPYING.  If not, write to
// the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.

package java.lang;
// model import org.jmlspecs.models.JMLString;

/** JML's specification of StringBuffer.
 * @author David Cok
 * @author Gary T. Leavens
 */
final public class StringBuffer implements java.io.Serializable, CharSequence {

// FIXME - should we use charArray instead of accumulatedString?

    //@ public non_null model String accumulatedString;

    /*@ public normal_behavior
      @   ensures this.accumulatedString.equals("");
      @*/
    //@ pure
    public StringBuffer();

    /*@ public normal_behavior
      @   ensures this.accumulatedString.equals("");
      @*/
    //@ pure
    public StringBuffer(int i);

    /*@ public normal_behavior
      @   ensures this.accumulatedString.equals(s);
      @*/
    //@ pure
    public StringBuffer(/*@non_null*/String s);

    /*@ public normal_behavior
      @   modifies accumulatedString;
      @   ensures accumulatedString.equals(\old(accumulatedString + c));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(char c);

    /*@ public normal_behavior
      @   assignable accumulatedString;
      @   ensures accumulatedString.equals(\old(String.concat(accumulatedString,String.valueOf(b))));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(boolean b);

    /*@ public normal_behavior
      @   requires s != null;
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(String.concat(accumulatedString,s)));
      @   ensures \result == this;
      @ also
      @ public normal_behavior
      @   requires s == null;
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(String.concat(accumulatedString,"null")));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(String s);

    /*@   public normal_behavior
      @     requires o != null;
      @     assignable accumulatedString;
      @     ensures accumulatedString
      @            .equals(\old(String.concat(accumulatedString,o.theString)));
      @     ensures \result == this;
      @ also
      @ public normal_behavior
      @   requires o == null;
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(String.concat(accumulatedString,"null")));
      @   ensures \result == this;
      @ implies_that
      @   public normal_behavior
      @     requires o != null;
      @     assignable accumulatedString;
      @     ensures accumulatedString.equals(\old(String.concat(accumulatedString,o.theString)));
      @     ensures \result == this;
      @*/
    public synchronized StringBuffer append(Object o);

    /*@ public normal_behavior
      @   requires s != null;
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(String.concat(accumulatedString,s.accumulatedString)));
      @   ensures \result == this;
      @ also
      @ public normal_behavior
      @   requires s == null;
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(String.concat(accumulatedString,"null")));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(StringBuffer s);

    /*@ public normal_behavior
      @   requires ca != null;
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(String.concat(accumulatedString,
      @                        String.valueOf(ca, i, j))));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(char[] ca, int i, int j);

    /*@ public normal_behavior
      @   assignable accumulatedString;
      @   ensures accumulatedString.equals(\old(String.concat(accumulatedString,String.valueOf(i))));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(int i);

    /*@ public normal_behavior
      @   assignable accumulatedString;
      @   ensures accumulatedString.equals(\old(String.concat(accumulatedString,String.valueOf(f))));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(float f);

    /*@ public normal_behavior
      @   assignable accumulatedString;
      @   ensures accumulatedString.equals(\old(String.concat(accumulatedString,String.valueOf(d))));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(double d);

    /*@ public normal_behavior
      @   requires ca != null;
      @   assignable accumulatedString;
      @   ensures accumulatedString.equals(\old(String.concat(accumulatedString,String.valueOf(ca))));
      @   ensures \result == this;
      @ also public normal_behavior
      @   requires ca == null;
      @   assignable accumulatedString;
      @   ensures accumulatedString.equals(\old(accumulatedString.concat("null")));
      @   ensures \result == this;
      @
      @*/
    public synchronized StringBuffer append(char[] ca);

    /*@ public normal_behavior
      @   assignable accumulatedString;
      @   ensures accumulatedString.equals(\old(String.concat(accumulatedString,String.valueOf(l))));
      @   ensures \result == this;
      @*/
    public synchronized StringBuffer append(long l);

    /*@ also
      @ public normal_behavior
      @   requires 0 <= index && index < accumulatedString.length();
      @   ensures \result == accumulatedString.charAt(index);
      @ also public exceptional_behavior
      @   requires !(0<=index && index < accumulatedString.length());
      @   signals_only StringIndexOutOfBoundsException;
      @*/
    public /*@ pure @*/ synchronized char charAt(int index);

    /*@ requires 0 <= srcBegin && srcBegin <= srcEnd;
      @ requires srcEnd <= accumulatedString.length();
      @ requires 0 <= dstBegin && dstBegin + srcEnd - srcBegin <= dst.length;
      @ assignable dst[dstBegin .. dstBegin+srcEnd-srcBegin];
      @ ensures CharSequence.equal(accumulatedString.charArray,srcBegin,
                           dst,dstBegin,srcEnd-srcBegin);
     */
    public synchronized void getChars(int srcBegin, int srcEnd,
                                      char[] dst, int dstBegin);

    /*@   public normal_behavior
      @     ensures \result != -1 <==> (0 <= \result && \result <=
      @                            accumulatedString.length()-str.length());
      @     ensures  accumulatedString.startsWith(str, \result);
      @     ensures (\forall int i; 0<=i && i < \result;
      @                     !accumulatedString.startsWith(str,i));
      @ also
      @   public normal_behavior
      @     requires !(\exists int k; 0 <= k && k < accumulatedString.length();
      @                               accumulatedString.startsWith(str, k));
      @     ensures \result == -1;
      @*/
    public /*@ pure @*/ int indexOf(/*@non_null*/String str);

    /*@  public normal_behavior
      @    requires (\exists int k; 0 <= k && k < accumulatedString.length();
      @                             accumulatedString.startsWith(str, k)
      @                             && k >= Math.min(fromIndex, str.length()));
      @    ensures \result
      @            == (\min int k; 0 <= k && k < accumulatedString.length()
      @                            && accumulatedString.startsWith(str, k)
      @                            && k >= Math.min(fromIndex, str.length());
      @                            k);
      @ also
      @   public normal_behavior
      @     requires !(\exists int k; 0 <= k && k < accumulatedString.length();
      @                               accumulatedString.startsWith(str, k)
      @                               && k >= Math.min(fromIndex, str.length()));
      @     ensures \result == -1;
      @*/
    public /*@ pure @*/ synchronized int indexOf(/*@non_null*/String str, int fromIndex);

    /*@  public normal_behavior
      @     requires (\exists int k; 0 <= k && k < accumulatedString.length();
      @                              accumulatedString.startsWith(str, k));
      @     assignable \nothing;
      @     ensures \result
      @             == (\max int k; 0 <= k && k < accumulatedString.length()
      @                             && accumulatedString.startsWith(str, k);
      @                             k);
      @ also
      @   public normal_behavior
      @     requires !(\exists int k; 0 <= k && k < accumulatedString.length();
      @                               accumulatedString.startsWith(str, k));
      @     assignable \nothing;
      @     ensures \result == -1;
      @*/
    public /*@ pure @*/ synchronized int lastIndexOf(/*@non_null*/String str);

    /*@   public normal_behavior
      @     requires (\exists int k; 0 <= k && k < accumulatedString.length();
      @                              accumulatedString.startsWith(str, k)
      @                              && k <= Math.min(fromIndex, str.length()));
      @     ensures \result
      @             == (\max int k; 0 <= k && k < accumulatedString.length()
      @                             && accumulatedString.startsWith(str, k)
      @                             && k <= Math.min(fromIndex, str.length());
      @                             k);
      @ also
      @   public normal_behavior
      @     requires !(\exists int k; 0 <= k && k < accumulatedString.length();
      @                               accumulatedString.startsWith(str, k)
      @                               && k <= Math.min(fromIndex, str.length()));
      @     assignable \nothing;
      @     ensures \result == -1;
      @*/
    public /*@ pure @*/ synchronized int lastIndexOf(/*@non_null*/String str, int fromIndex);

    /*@ also
      @ public normal_behavior
      @   ensures \result == accumulatedString.length();
      @*/
    public /*@ pure @*/ synchronized int length();

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

    public /*@ pure @*/ CharSequence subSequence(int start, int end);

    public /*@ pure @*/ synchronized int capacity();

    //@ ensures capacity() >= minimumCapacity;
    public synchronized void ensureCapacity(int minimumCapacity);

    /*@ public normal_behavior
      @ requires 0 <= index && index < accumulatedString.length();
      @ assignable accumulatedString;
      @ ensures accumulatedString.subSequence(0,index).equals(
      @                  \old(accumulatedString.subSequence(0,index)));
      @ ensures
      @       accumulatedString.subSequence(index,accumulatedString.length()).equals(
      @       \old(accumulatedString.subSequence(index+1,accumulatedString.length())));
      @ ensures accumulatedString.length() == \old(accumulatedString.length()-1);
      @ ensures \result == this;
      @*/
    public synchronized StringBuffer deleteCharAt(int index);

    /*@ public normal_behavior
      @   requires 0 <= offset && offset <= accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,offset)
      @             + String.valueOf(l) + accumulatedString.substring(offset)));
      @   ensures \result == this;   
      @*/
    public StringBuffer insert(int offset, long l);

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

    /*@ public normal_behavior
      @   requires 0 <= offset && offset <= accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,offset)
      @                        + d + accumulatedString.substring(offset)));
      @   ensures \result == this;   
      @*/
    public StringBuffer insert(int offset, double d);

    /*@ public normal_behavior
      @   requires 0 <= offset && offset <= accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,offset)
      @                        + c + accumulatedString.substring(offset)));
      @   ensures \result == this;   
      @*/
    public synchronized StringBuffer insert(int offset, char c);

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

    /*@ public normal_behavior
      @   requires 0 <= offset && offset <= accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,offset)
      @                        + String.valueOf(ca)
      @                        + accumulatedString.substring(offset)));
      @   ensures \result == this;   
      @*/
    public synchronized StringBuffer insert(int offset, char[] ca);

    /*@ public normal_behavior
      @   requires 0 <= offset && offset <= accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,offset)
      @                        + b + accumulatedString.substring(offset)));
      @   ensures \result == this;   
      @*/
    public StringBuffer insert(int offset, boolean b);

    /*@ public normal_behavior
      @   requires 0 <= offset && offset <= accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,offset)
      @                        + o + accumulatedString.substring(offset)));
      @   ensures \result == this;   
      @*/
    public synchronized StringBuffer insert(int offset, Object o);

    /*@ public normal_behavior
      @   requires 0 <= offset && offset <= accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,offset)
      @                        + s + accumulatedString.substring(offset)));
      @   ensures \result == this;   
      @*/
    public synchronized StringBuffer insert(int offset, String s);

    /*@ public normal_behavior
      @   requires 0 <= offset && offset <= accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,offset)
      @                        + f + accumulatedString.substring(offset)));
      @   ensures \result == this;   
      @*/
    public StringBuffer insert(int offset, float f);

    /*@ public normal_behavior
      @    assignable accumulatedString;
      @    ensures \result == this;
      @    ensures accumulatedString.length() == \old( accumulatedString.length() );
      @    ensures (\forall int i; 0<=i && i<accumulatedString.length();
                            \old(charAt(i)) == charAt(length()-1-i));
     @*/
    public synchronized StringBuffer reverse();


    /*@ public normal_behavior
      @   requires 0 <= index && index < accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString
      @           .equals(\old(accumulatedString.substring(0,index)
      @                        + c + accumulatedString.substring(index+1)));
      @ implies_that
      @ public normal_behavior
      @   requires 0 <= index && index < accumulatedString.length();
      @   assignable accumulatedString;
      @   ensures accumulatedString.length()
      @           == \old(accumulatedString.length())
      @        && (\forall int i; 0 <= i && i < accumulatedString.length()
      @                                  && i != index;
      @                           accumulatedString.charAt(i)
      @                           == \old(accumulatedString.charAt(i)))
      @        && accumulatedString.charAt(index) == c;
      @*/
    public synchronized void setCharAt(int index, char c);

    //@ also
    //@  public normal_behavior
    // !FIXME! not sure this is really pure, but CharSequence requires purity
    //@  assignable \nothing;
    //@  ensures \result.equals(accumulatedString);
    public String toString();

    public synchronized void setLength(int i);

    public synchronized StringBuffer delete(int i, int j);

    public synchronized String substring(int i);

    public synchronized String substring(int start, int end);
}
