org.jmlspecs.samples.reader
Class BufferedReader

java.lang.Object
  org.jmlspecs.samples.reader.BufferedReader

All Implemented Interfaces:

Reader

Direct Known Subclasses:

BlankReader

public abstract class BufferedReader

extends Object

implements Reader

Buffered 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

public represents valid <- this != null&&0 <= this.lo&&this.lo <= this.cur&&this.cur <= this.hi&&this.buff != null&&this.hi-this.lo <= this.buff.length&&this.svalid;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
boolean	svalid

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Model fields inherited from interface org.jmlspecs.samples.reader.Reader

state, valid

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
[spec_public] protected  char[]	buff
[spec_public] protected  int	cur
[spec_public] protected  int	hi
[spec_public] protected  int	lo

 

Constructor Summary

BufferedReader()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
int	read()
abstract  void	refill()

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Methods inherited from interface org.jmlspecs.samples.reader.Reader

close

 

Model Field Detail

svalid

public boolean svalid

Specifications:
is in groups: valid
datagroup contains: org.jmlspecs.samples.reader.BlankReader.num lo hi buff

lo

protected int lo

Specifications: spec_public
is in groups: valid state svalid

hi

protected int hi

Specifications: spec_public
is in groups: valid state svalid

cur

protected int cur

Specifications: spec_public
is in groups: valid state

buff

protected char[] buff

Specifications: spec_public
is in groups: valid state svalid
maps buff[*] \into state

BufferedReader

public BufferedReader()

read

public int read()

Specified by:

read in interface Reader

Specifications inherited from overridden method in interface Reader:

public normal_behavior
requires this.valid;
assignable state;
ensures -1 <= \result &&\result <= 65535;

refill

public abstract void refill()

Specifications:

public normal_behavior
requires this.valid;
assignable state;
ensures this.cur == \old(this.cur);