Инвариант цикла для повторных вызовов readLine()

У меня есть цикл while (показан ниже), который постоянно читает из файла, пока не будет достигнут EOF. Я должен написать инвариант цикла для любого нетривиального цикла. Это тривиальная петля? Если нет, то что будет инвариантом цикла для этого цикла while? Я никогда раньше не писал инварианты.

while (line != null) {
    System.out.println(line);
    line = reader.readLine();
}

java loop-invariant
person Alex Parker    schedule 22.01.2015    source источник
comment
Вы используете формализм вроде логики Хоара? en.wikipedia.org/wiki/Hoare_logic   -  person Codor    schedule 22.01.2015

Ответы (1)


arrow_upward
-1
arrow_downward

Вы можете использовать FileReader:

while ((line = fileReader.hasNextLine()) != null) {
    String line = fileReader.nextLine(); 
    System.out.println(line);
}

=D

person Kevin F    schedule 22.01.2015