Class BlankReader

  extended byorg.jmlspecs.samples.reader.BufferedReader
      extended byorg.jmlspecs.samples.reader.BlankReader
All Implemented Interfaces:

public class BlankReader
extends BufferedReader

A reader that delivers a stream of blanks.

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
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
Method Summary
 void close()
 void refill()
Methods inherited from class org.jmlspecs.samples.reader.BufferedReader
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail


private int num
is in groups: state svalid
Constructor Detail


public BlankReader(int n)
public normal_behavior
requires 0 <= n;
assignable valid, state;
ensures this.valid&&this.svalid;
Method Detail


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);


public void close()
Specifications inherited from overridden method in interface Reader:
public normal_behavior
requires this.valid;
assignable valid, state;


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.