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?
Посылка: {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?
Ежели разве что рассматривать LOOP как обычный цикл с "риторическим" вопросом условия...
