JML

org.jmlspecs.samples.reader
Interface Reader

All Known Implementing Classes:
BufferedReader

public interface Reader

Readers.

Author:
Arnd Poetzsch-Heffter from an example by K. Rustan M. Leino and Greg Nelson, in Data abstraction and information hiding, ACM Transactions on Programming Languages and Systems, Volume 24, number 5, pp. 491-553, September 2002.

Class Specifications

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

Model Field Summary
[instance]  Object state
           
[instance]  boolean valid
           
 
Method Summary
 void close()
           
 int read()
           
 

Model Field Detail

valid

public boolean valid
Specifications: instance
datagroup contains: org.jmlspecs.samples.reader.BufferedReader.lo org.jmlspecs.samples.reader.BufferedReader.hi org.jmlspecs.samples.reader.BufferedReader.cur org.jmlspecs.samples.reader.BufferedReader.buff org.jmlspecs.samples.reader.BufferedReader.svalid

state

public Object state
Specifications: instance
datagroup contains: org.jmlspecs.samples.reader.BlankReader.num org.jmlspecs.samples.reader.BufferedReader.lo org.jmlspecs.samples.reader.BufferedReader.hi org.jmlspecs.samples.reader.BufferedReader.cur org.jmlspecs.samples.reader.BufferedReader.buff buff[*]
Method Detail

read

public int read()
Specifications:
public normal_behavior
requires this.valid;
assignable state;
ensures -1 <= \result &&\result <= 65535;

close

public void close()
Specifications:
public normal_behavior
requires this.valid;
assignable valid, state;

JML

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.