<<
>>

Вычисление предусловия для цикла FOR

Количество итераций цикла FOR заранее известно, поэтому данный цикл может трактоваться как повторение последовательности операторов его тела.

Вычисление предусловия здесь может выполняться обратной разверткой цикла (рис.

7.5).

Развертка цикла

Рис. 7.5. Обратная развертка цикла FOR

196

Глава 7. Формальная семантика языков программирования

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

Отсюда заключение: самостоятельное правило вывода для оператора цикла FOR не требуется.

<< | >>

Еще по теме Вычисление предусловия для цикла FOR:

  1. Вычисление ошибки репрезентативности для собственно случайной выборки.
  2. Тема 6. Модели жизненного цикла
  3. Глава 6. Модели жизненного цикла
  4. ЗОДИАКАЛЬНЫЕ ЗНАКИ И ФАЗЫ ЦИКЛА
  5. 6.2. Примеры моделей жизненного цикла
  6. В.В. Розанов. Из цикла «Эмбрионы»
  7. Вычисление символических дирекций
  8. ВЫЧИСЛЕНИЕ СРОКА СТАБИЛЬНОСТИ БРАКА
  9. М.Е. Салтыков-Щедрин. Из цикла «Письма к тетеньке»
  10. М.Е. Салтыков-Щедрин. Из цикла «Круглый год»
  11. Вычисление ошибки выборки.
  12. Вычисление ошибки выборки.
  13. Вычисление ошибки выборки.
  14. Вычисление местного звездного времени
  15. Статья 676. Вычисление гарантийного срока