Модели множеств последовательностей и доказательство правильности программ

Описывается класс программ, доказательство определенных свойств («правильность») которых методом Флойда–Хоора требует построения соотношений между переменными, устроенных не менее сложно, чем сами программы. Даются примеры соотношений, которые являются инвариантами циклов, но это не может быть доказано непосредственным применением метода Хоора.