> -- Rifat писал(а):
> В книге Вирта "Систематическое программирование" правила верификации для циклических конструкций записываются следующим образом:Посылка: {P and B} S {P}Следствие: {P} while B do S {P and not B}Посылка: {P} S {Q}              {Q and not B} S {Q}Следствие: {P} repeat S until B {Q}Можно ли аналогичные правила верификации записать для цикла LOOP из языка Oberon?
В общем виде, как представляется, нельзя. Поскольку нет явного  условия окончания цикла.