6 О ПРОЕКТИРОВАНИИ ПРАВИЛЬНО ЗАВЕРШАЕМЫХ КОНСТРУКЦИЙ
Основная теорема для конструкции повторения применительно к условию
Р, сохраняемому инвариантно истинным, утверждает, что
Замечание 2. Часто на практике расщепляют уравнение (9) на два уравнения:
и рассматривают их по отдельности. Тем самым разделяются две задачи: (9а) относится к тому, что остается инвариантным, тогда как (96) относится к тому, что обеспечивает продвижение вперед. Если, имея дело с уравнением (9а), мы приходим к решению Bj, такому, что
Р => Bj, то тогда очевидно, что это условие не будет удовлетворять уравнению (96), поскольку при таком Bj инвариантность Р привела бы к недетерминированности (Конец замечания 2.)Таким образом, мы можем построить конструкцию DO, такую, что
Наши условия Bj должны быть достаточно сильными, чтобы удовлетворялись следования (9); в результате этого новое гарантируемое постусловие Р and поп В В может оказаться слишком слабым и не обеспечить нам желаемого постусловия R. В таком случае мы все-таки не решили нашу проблему и нам следует рассмотреть другие возможности.
