Инварианты петли с перерывами

Question

Я пытаюсь понять, как инварианты цикла взаимодействуют с разрывами. CLRS 3e (pg19) описывает инвариант цикла как требующий, чтобы

Если оно равно true до итерации цикла, оно остается истинным до следующей итерации.

Так дан следующий тривиальный цикл

for i = 1 to 5
    if i == 3 then break

Было бы справедливо сказать, что i <4 </em> является инвариантным свойством цикла? Аргумент заключается в том, что, поскольку цикл заканчивается в операторе break , после нарушения этого свойства итерации не происходит.

Answer 1

Да, это был бы инвариант, именно по той причине, которую вы упомянули. Является ли это полезным инвариантом - это отдельный вопрос, который зависит от того, что вы пытаетесь доказать.