В книге Вирта "Систематическое программирование" правила верификации для циклических конструкций записываются следующим образом:

Посылка: {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?