<<
>>

Построение инварианта

Очевидно, что для нуля итераций слабейшее предусловие: {у = х}.

198

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

Для одной итерации:

Для двух итераций:

Для трех итераций:

Ясно, что {y < х} удовлетворяет условиям одной и более итераций.

Объединяя это утверждение с {у = х} для случая нуля итераций, получаем инвариант цикла:

Его можно использовать и как предусловие, то есть P = I.

Конечно, мы должны быть уверены, что наш инвариант удовлетворяет всем пяти требованиям.

<< | >>

Еще по теме Построение инварианта:

  1. II. 1. 4. Инварианты.
  2. ДВИЖЕНИЕ: ПОСТРОЕНИЕ
  3. КОНЦЕПЦИЯ УРОВНЕЙ ПОСТРОЕНИЯ ДВИЖЕНИЙ
  4. Хаос вопросов со строгой логикой построения
  5. II. МЕТОДИЧЕСКИЕ ОСНОВЫ ПОСТРОЕНИЯ СИСТЕМНЫХ ОПИСАНИЙ
  6. Построение гороскопа
  7. Построение здоровья
  8. § 3. Принципы построения системы (классификации) гражданских договоров
  9. I. 3. ОБЩАЯ ХАРАКТЕРИСТИКА СИСТЕМНЫХ ОПИСАНИЙ И МЕТОДОВ ИХ ПОСТРОЕНИЯ
  10. 3. Построение информации и ее восприятие
  11. СПОСОБЫ ПОСТРОЕНИЯ НАТАЛЬНОЙ КАРТЫ