Инварианты циклов с разрывами

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

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

Итак, учитывая следующий тривиальный цикл

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

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


algorithm clrs loop-invariant
person frog    schedule 04.01.2019    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

person templatetypedef    schedule 04.01.2019