JML

org.jmlspecs.samples.reader
Class BufferedReader

java.lang.Object
  extended byorg.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
Field Detail

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
Constructor Detail

BufferedReader

public BufferedReader()
Method Detail

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

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.