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
Interface DataInput

All Known Subinterfaces:
ObjectInput
All Known Implementing Classes:
ObjectInputStream, RandomAccessFile
public interface DataInput

JML's specification of DataInput.

Author:
Gary T. Leavens

Class Specifications
initially this.bytesRead.isEmpty();

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

Model Field Summary
[instance]  JMLValueSequence bytesRead
           
[instance]  JMLDataGroup input
           
 
Method Summary
 boolean readBoolean()
           
 byte readByte()
           
 char readChar()
           
 double readDouble()
           
 float readFloat()
           
 void readFully(byte[] b)
           
 void readFully(byte[] b, int off, int len)
           
 int readInt()
           
 String readLine()
           
 long readLong()
           
 short readShort()
           
 int readUnsignedByte()
           
 int readUnsignedShort()
           
 String readUTF()
           
 int skipBytes(int n)
           
 

Model Field Detail

input

public JMLDataGroup input
Specifications: instance
is in groups: objectState
datagroup contains: bytesRead

bytesRead

public JMLValueSequence bytesRead
Specifications: instance non_null
is in groups: input
Method Detail

readFully

public void readFully(byte[] b)
                        throws IOException
Throws:
IOException

readFully

public void readFully(byte[] b,
                      int off,
                      int len)
                        throws IOException
Throws:
IOException

skipBytes

public int skipBytes(int n)
                       throws IOException
Throws:
IOException

readBoolean

public boolean readBoolean()
                             throws IOException
Throws:
IOException
Specifications:
public behavior
assignable input;
ensures this.bytesRead.size() == \old(this.bytesRead.size()+1);
ensures this.bytesRead.header().equals(\old(this.bytesRead));
ensures \result <==> ((org.jmlspecs.models.JMLByte)this.bytesRead.last()).theByte != 0;
ensures_redundantly \result == false <==> ((org.jmlspecs.models.JMLByte)this.bytesRead.last()).theByte == 0;

readByte

public byte readByte()
                       throws IOException
Throws:
IOException
Specifications:
public behavior
assignable input;
ensures this.bytesRead.equals(\old(this.bytesRead).insertBack(new org.jmlspecs.models.JMLByte(\result )));
ensures_redundantly -128 <= \result &&\result < 127;
ensures_redundantly this.bytesRead.size() == \old(this.bytesRead.size()+1);
ensures_redundantly this.bytesRead.header().equals(\old(this.bytesRead));

readUnsignedByte

public int readUnsignedByte()
                              throws IOException
Throws:
IOException
Specifications:
public behavior
assignable input;
ensures this.bytesRead.size() == \old(this.bytesRead.size()+1);
ensures this.bytesRead.header().equals(\old(this.bytesRead));
ensures ((byte)\result ) == ((org.jmlspecs.models.JMLByte)this.bytesRead.last()).theByte;
ensures 0 <= \result &&\result <= 255;

readShort

public short readShort()
                         throws IOException
Throws:
IOException
Specifications:
public behavior
assignable input;
ensures this.bytesRead.size() == \old(this.bytesRead.size()+2);
ensures this.bytesRead.subsequence(0,this.bytesRead.size()-2).equals(\old(this.bytesRead));
ensures \result == (short)(((((org.jmlspecs.models.JMLByte)this.bytesRead.header().last()).theByte) << 8)|(((org.jmlspecs.models.JMLByte)this.bytesRead.last()).theByte&255));

readUnsignedShort

public int readUnsignedShort()
                               throws IOException
Throws:
IOException
Specifications:
public behavior
assignable input;
ensures this.bytesRead.size() == \old(this.bytesRead.size()+2);
ensures this.bytesRead.subsequence(0,this.bytesRead.size()-2).equals(\old(this.bytesRead));
ensures \result == (((((org.jmlspecs.models.JMLByte)this.bytesRead.header().last()).theByte&255) << 8)|(((org.jmlspecs.models.JMLByte)this.bytesRead.last()).theByte&255));

readChar

public char readChar()
                       throws IOException
Throws:
IOException
Specifications:
public behavior
assignable input;
ensures this.bytesRead.size() == \old(this.bytesRead.size()+2);
ensures this.bytesRead.subsequence(0,this.bytesRead.size()-2).equals(\old(this.bytesRead));
ensures \result == (char)(((((org.jmlspecs.models.JMLByte)this.bytesRead.header().last()).theByte) << 8)|(((org.jmlspecs.models.JMLByte)this.bytesRead.last()).theByte&255));

readInt

public int readInt()
                     throws IOException
Throws:
IOException

readLong

public long readLong()
                       throws IOException
Throws:
IOException

readFloat

public float readFloat()
                         throws IOException
Throws:
IOException

readDouble

public double readDouble()
                           throws IOException
Throws:
IOException

readLine

public String readLine()
                         throws IOException
Throws:
IOException

readUTF

public String readUTF()
                        throws IOException
Throws:
IOException
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.