S - его тело, а Init - группа предшествующих операторов, задающая инициализацию цикла. Реально ни один цикл не обходится без инициализирующей части. Синтаксически было бы правильно, чтобы Init являлся бы формальной частью оператора цикла. В операторе for эта частично сделано - инициализация счетчиков является частью цикла. Определение 3 (инварианта цикла): предикат Inv(x, z) называется инвариантом цикла while, если истинна следующая триада Хоара: {Inv(x, z)& B}S(x,z){Inv(x,z)} Содержательно это означает, что из истинности инварианта цикла до начала выполнения тела цикла и из истинности условия цикла, гарантирующего выполнение тела, следует истинность инварианта после выполнения тела цикла. Сколько бы раз ни выполнялось тело цикла, его инвариант остается истинным. Для любого цикла можно написать сколь угодно много инвариантов. Любое тождественное условие (2*2 =4) является инвариантом любого цикла. Поэтому среди инвариантов выделяются так называемые подходящие инварианты цикла. Они называются подходящими, поскольку позволяют доказать корректность цикла по отношению к его пред- и постусловиям. Как доказать корректность цикла? Рассмотрим соответствующую триаду: {Pre(x)} Init(x,z); while(B)S(x,z);{Post(x,z)} Доказательство разбивается на три этапа. Вначале доказываем истинность триады: (*) {Pre(x)} Init(x,z){RealInv(x,z)} Содержательно это означает, что предикат RealInv становится истинным после выполнения инициализирующей части. Далее доказывается, что RealInv является инвариантом цикла: (**) {RealInv(x, z)& B} S(x,z){RealInv(x,z)} На последнем шаге доказывается, что наш инвариант обеспечивает решение задачи после завершения цикла: (***) ~B & RealInv(x, z) -> Post(x,z) Это означает, что из истинности инварианта и условия завершения цикла следует требуемое постусловие. Определение 4 (подходящего инварианта): предикат RealInv, удовлетворяющий условиям (*), (**), (***) называется подходящим инвариантом цикла. |