JML

org.jmlspecs.samples.reader
Class BlankReader

java.lang.Object
  extended byorg.jmlspecs.samples.reader.BufferedReader
      extended byorg.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.

Field Summary
private  int num
           
 
Fields inherited from class org.jmlspecs.samples.reader.BufferedReader
buff, cur, hi, lo
 
Constructor Summary
BlankReader(int n)
           
 
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
Constructor Detail

BlankReader

public BlankReader(int n)
Method Detail

refill

public void refill()

close

public void close()

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.