Определение инварианта цикла по индукции
Определение инварианта цикла по индукции |
197 |
Выработку слабейшего предусловия удобно рассматривать как вычисление псевдофункции wp: 1лф (оператор_тела, постусловие) = предусловие |
Для нахождения значений ыр выполняем обратную развертку итераций тела цикла, начиная с нуля итераций (рис. 7.6). |
Рис. 7.6. Обратная развертка цикла WHILE |
Если тело цикла содержит единственный оператор присваивания, то инструментами вычисления будут: 1. Аксиома присваивания (для перехода в рамках одной итерации от постусловия к предусловию). 2. Правило вывода для последовательности (для перехода от предусловия к постусловию соседних итераций). |