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[*]

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;