// @(#)$Id: StringBuffer.jml,v 1.15 2006/11/19 19:39:07 leavens Exp $ // Copyright (C) 2005 Iowa State University // // This file is part of the runtime library of the Java Modeling Language. // // This library is free software; you can redistribute it and/or // modify it under the terms of the GNU Lesser General Public License // as published by the Free Software Foundation; either version 2.1, // of the License, or (at your option) any later version. // // This library 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 // Lesser General Public License for more details. // // You should have received a copy of the GNU Lesser General Public License // along with JML; see the file LesserGPL.txt. If not, write to the Free // Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA // 02110-1301 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 { //@ 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 @ requires s != null; @ ensures this.accumulatedString.equals(s); @*/ //@ pure public StringBuffer(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(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(accumulatedString.concat(s))); @ ensures \result == this; @ also @ public normal_behavior @ requires s == null; @ assignable accumulatedString; @ ensures accumulatedString @ .equals(\old(accumulatedString.concat("null"))); @ ensures \result == this; @*/ public synchronized StringBuffer append(String s); /*@ public normal_behavior @ requires o != null; @ assignable accumulatedString; @ ensures accumulatedString @ .equals(\old(accumulatedString.concat(o.theString))); @ ensures \result == this; @ also @ public normal_behavior @ requires o == null; @ assignable accumulatedString; @ ensures accumulatedString @ .equals(\old(accumulatedString.concat("null"))); @ ensures \result == this; @ implies_that @ public normal_behavior @ requires o != null; @ assignable accumulatedString; @ ensures accumulatedString.equals(\old(accumulatedString + o.theString)); @ ensures \result == this; @*/ public synchronized StringBuffer append(Object o); /*@ public normal_behavior @ requires s != null; @ assignable accumulatedString; @ ensures accumulatedString @ .equals(\old(accumulatedString.concat(s.accumulatedString))); @ ensures \result == this; @ also @ public normal_behavior @ requires s == null; @ assignable accumulatedString; @ ensures accumulatedString @ .equals(\old(accumulatedString.concat("null"))); @ ensures \result == this; @*/ public synchronized StringBuffer append(StringBuffer s); /*@ public normal_behavior @ requires ca != null; @ assignable accumulatedString; @ ensures accumulatedString @ .equals(\old(accumulatedString @ .concat(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(accumulatedString + String.valueOf(i))); @ ensures \result == this; @*/ public synchronized StringBuffer append(int i); /*@ public normal_behavior @ assignable accumulatedString; @ ensures accumulatedString.equals(\old(accumulatedString + String.valueOf(f))); @ ensures \result == this; @*/ public synchronized StringBuffer append(float f); /*@ public normal_behavior @ assignable accumulatedString; @ ensures accumulatedString.equals(\old(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(accumulatedString.concat(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(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 @ requires str != null; @ 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 str != null; @ requires !(\exists int k; 0 <= k && k < accumulatedString.length(); @ accumulatedString.startsWith(str, k)); @ ensures \result == -1; @*/ public /*@ pure @*/ int indexOf(String str); /*@ public normal_behavior @ requires str != null; @ 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 str != null; @ 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(String str, int fromIndex); /*@ public normal_behavior @ requires str != null; @ 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 str != null; @ requires !(\exists int k; 0 <= k && k < accumulatedString.length(); @ accumulatedString.startsWith(str, k)); @ assignable \nothing; @ ensures \result == -1; @*/ public /*@ pure @*/ synchronized int lastIndexOf(String str); /*@ public normal_behavior @ requires str != null; @ 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 str != null; @ 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(String str, int fromIndex); /*@ also @ public normal_behavior @ ensures \result == accumulatedString.length(); @*/ public /*@ pure @*/ synchronized int length(); public synchronized /*@ non_null @*/ StringBuffer replace(int start, int end, String str); public /*@ pure non_null @*/ 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 /*@ non_null @*/ StringBuffer insert(int offset, float f); public synchronized /*@ non_null @*/ 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 /*@ non_null @*/ String toString(); public synchronized void setLength(int i); public synchronized /*@ non_null @*/ StringBuffer delete(int i, int j); public synchronized /*@ non_null @*/ String substring(int i); public synchronized /*@ non_null @*/ String substring(int start, int end); }