BlankReader (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

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.

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