<<
>>

Определение инварианта цикла по индукции

Определяют инвариант по индукции, многократно вычисляя слабейшие предусловия. При этом полагают, что на основе частных случаев будет выявлено общее утверждение.

Определение инварианта цикла по индукции

197

Выработку слабейшего предусловия удобно рассматривать как вычисление псевдофункции wp:

1лф (оператор_тела, постусловие) = предусловие

Для нахождения значений ыр выполняем обратную развертку итераций тела цикла, начиная с нуля итераций (рис.
7.6).

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

Если тело цикла содержит единственный оператор присваивания, то инструментами вычисления будут:

1. Аксиома присваивания (для перехода в рамках одной итерации от постусловия к предусловию).

2. Правило вывода для последовательности (для перехода от предусловия к постусловию соседних итераций).

Пример доказательства цикла

Рассмотрим цикл

<< | >>

Еще по теме Определение инварианта цикла по индукции:

  1. II. 1. 4. Инварианты.
  2. ПРОЦЕСС НЕРВНЫЙ: ИНДУКЦИЯ
  3. ИНДУКЦИЯ
  4. Тема 6. Модели жизненного цикла
  5. Глава 6. Модели жизненного цикла
  6. ЗОДИАКАЛЬНЫЕ ЗНАКИ И ФАЗЫ ЦИКЛА
  7. 6.2. Примеры моделей жизненного цикла
  8. В.В. Розанов. Из цикла «Эмбрионы»
  9. М.Е. Салтыков-Щедрин. Из цикла «Письма к тетеньке»
  10. М.Е. Салтыков-Щедрин. Из цикла «Круглый год»
  11. Статья 55. Лишение права занимать определенные должности или заниматься определенной деятельностью