class File {   

  int linesInFile; int linesRead; boolean closed; boolean lineInBuffer; boolean eof;
  
  //@ invariant linesRead >= 0 && linesRead <= linesInFile;
  //@ initial linesRead == 0 && linesInFile == 5 && !closed && !lineInBuffer && !eof;
  void File() {
    linesRead = 0; linesInFile = 5; closed = false; lineInBuffer = false; eof = false;
  }  
    
  //@ requires linesRead < linesInFile && !closed && lineInBuffer && !eof;
  //@ ensures linesRead + 1 <= linesInFile && !closed && !lineInBuffer && !eof;
  string read() {
    linesRead = linesRead + 1;
	lineInBuffer = false;
	"reading line... \n";
  }
  
  //@ requires linesRead <= linesInFile && !closed && !lineInBuffer && !eof;
  //@ ensures (linesRead == linesInFile -> (!lineInBuffer && eof)) && !closed;
  boolean eof() {   
    lineInBuffer = !(linesRead == linesInFile);
	eof = !lineInBuffer;
    eof;
  }
   
  //@ requires linesRead == linesInFile && !closed && eof;   
  //@ ensures linesRead == linesInFile && closed && eof;
  void close() {     
    closed = true;
  }                            
}

class FileReader {   

  File file; string s; int counter; boolean isEof;
  
  //@ invariant counter >= 0;
  //@ requires !f.eof();
  //@ initial counter == 0 && new File() && !isEof;
  void FileReader(File f) {
    file = f; 
	s = ""; 
	counter = 0;
	isEof = false;
  }  
       
  //@ requires !isEof;
  //@ ensures !file.eof() -> !isEof;
  boolean next() {
    if(file.eof()) {
		isEof = true;
		file.close();
		false;
	} else {
		s = s ++ file.read(); 
		true;
	}
  }
    
  //@ requires counter >= 0;
  //@ ensures counter >= 0;
  string toString() {   
    count();
	s;
  }
  
  //@ requires isEof;
  //@ ensures isEof;
  int getCounter() {   
    counter;
  }
  
  //@ requires !isEof;
  //@ ensures !isEof && !file.eof();
  File getFileToRead() {
	file;
  }
   
  //@ requires false;   
  //@ ensures false;
  sync void count() {     
    counter = counter + 1;
  }                            
}