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.io
Class StringWriter

java.lang.Object
  extended byjava.io.Writer
      extended byjava.io.StringWriter
public class StringWriter
extends Writer

Class Specifications

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

Model Field Summary
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
 
Fields inherited from class java.io.Writer
lock
 
Constructor Summary
StringWriter()
           
StringWriter(int Param0)
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 void close()
           
 void flush()
           
 StringBuffer getBuffer()
           
 String toString()
           
 void write(non_null char[] Param0, int Param1, int Param2)
           
 void write(int Param0)
           
 void write(non_null String Param0)
           
 void write(non_null String Param0, int Param1, int Param2)
           
 
Methods inherited from class java.io.Writer
write
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Constructor Detail

StringWriter

public StringWriter()

StringWriter

public StringWriter(int Param0)
Method Detail

close

public void close()
           throws IOException
Throws:
IOException

flush

public void flush()

write

public void write(int Param0)
Overrides:
write in class Writer

write

public void write(non_null char[] Param0,
                  int Param1,
                  int Param2)

toString

public String toString()
Overrides:
toString in class Object
Specifications: non_null
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;

write

public void write(non_null String Param0)
Overrides:
write in class Writer

write

public void write(non_null String Param0,
                  int Param1,
                  int Param2)
Overrides:
write in class Writer

getBuffer

public StringBuffer getBuffer()
Specifications: non_null
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.