org.jmlspecs.samples.reader
Class BlankReader

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

All Implemented Interfaces:

Reader

public class BlankReader

extends BufferedReader

A reader that delivers a stream of blanks.

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

private represents svalid <- this.hi <= this.num;

Specifications inherited from class BufferedReader

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

 

Model fields inherited from class org.jmlspecs.samples.reader.BufferedReader

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
private  int	num

 

Fields inherited from class org.jmlspecs.samples.reader.BufferedReader

buff, cur, hi, lo

 

Constructor Summary

BlankReader(int n)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	close()
void	refill()

 

Methods inherited from class org.jmlspecs.samples.reader.BufferedReader

read

 

Methods inherited from class java.lang.Object

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

 

Field Detail

num

private int num

Specifications:
is in groups: state svalid

BlankReader

public BlankReader(int n)

Specifications:

public normal_behavior
requires 0 <= n;
assignable valid, state;
ensures this.valid&&this.svalid;

refill

public void refill()

Specifications inherited from overridden method in class BufferedReader:

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

close

public void close()

Specifications inherited from overridden method in interface Reader:

public normal_behavior
requires this.valid;
assignable valid, state;