Теорема для конструкции выбора представляет особую важность в случае, когда пара предикатов Q и R может быть записана в виде
для всех состояний.
Эту теорему, которая известна также под названием "основная теорема инвариантности для циклов", на интуитивном уровне не трудно понять. Предпосылка (7) говорит нам, что если предикат Р первоначально истинен и одна из охраняемых команд выбирается для выполнения, то после ее выполнения Р сохранит свою истинность. Иначе говоря, предохранители гарантируют, что выполнение соответствующих списков операторов не нарушит истинности Р, если начальное значение Р было истинным. Следовательно, вне зависимости от того, как часто производится выборка охраняемой команды из имеющегося набора, предикат Р будет справедлив при любой новой проверке предохранителей. После завершения всей конструкции повторения, когда ни один из предохранителей не является истиной, мы тем самым закончим работу в конечном состоянии, удовлетворяющем Р and nonBB. Вопрос в том, завершится ли работа правильно. Да, если условие wp(-DO, Т) справедливо и вначале; поскольку любое состояние удовлетворяет
Т, то wp(-DO, Т) по определению является слабейшим предусловием для начального состояния, такого, что запуск оператора DO приведет к правильно завершаемой работе.Формальное доказательство основной теоремы для конструкции повторения основывается на формальном описании семантики этой конструкции (см. предыдущую главу), из которого мы выводим
Равенство в первой строке следует из (10), равенство во второй строке следует из того, что всегда wp(/-F,
К) => ВВ, логическое следование в третьей строке вытекает из (7), равенство в четвертой строке основывается на свойстве 3 преобразователей предикатов, следование в пятой строке вытекает из свойства 2 преобразователей предикатов и из индуктивного предположения (13) для k = К — 1, и последняя строка следует из (12). Итак, мы доказали (13) для k = К, а следовательно, для всех значений k > 0.Наконец, для любой точки в пространстве состояний мы имеем, в силу (13),
и тем самым доказана основная теорема (8) для конструкции повторения. Ценность основной теоремы для конструкции повторения основывается на том, что ни в предпосылке, ни в ее следствии не упоминается фактическое число выборок охраняемой команды. Поэтому она применима даже в тех случаях, когда это число не определяется начальным состоянием.
