Вычисление предусловия для цикла FOR
Вычисление предусловия здесь может выполняться обратной разверткой цикла (рис.
7.5).
Развертка цикла Рис. 7.5. Обратная развертка цикла FOR |
196 |
Глава 7. Формальная семантика языков программирования |
Примем, что в теле цикла FOR используются только операторы присваивания. В этом случае каждая итерация развернутого цикла доказывается с помощью аксиомы присваивания и правила вывода для последовательности, обеспечивающих вычисление Р3 по Q3, P2 по Q2 и Р1 по Qt. Переход же от одной итерации к соседней также требует применения лишь правила вывода для последовательности, поскольку в нашем примере нужно только установить тождества: Q2 = Р3 и Q1 = Р2. Отсюда заключение: самостоятельное правило вывода для оператора цикла FOR не требуется. |