<<
>>

Общий случай определения инварианта цикла

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

Общий случай определения инварианта цикла

199

цикла while зависит от нахождения инварианта, аксиоматическое доказательство корректности программ с циклами while может быть очень трудным.

Рассмотрим пример доказательства программы, вычисляющей функцию фак- ториала:

Метод нахождения инварианта по индукции здесь не работает. Требуется не- которая изобретательность.

Здесь переменная count последовательно принимает значения n, n-1, ..., 1, 0 (count означает: сколько операций умножения остается выполнить для того, чтобы получить n!).

Переменная fact последовательно принимает значения

Цикл вычисляет функцию так, что последнее умножение выполняется первым. Это значит, что первым вычисляется (n - 1) * n при допущении, что n > 1.

Итак, частью инварианта может быть fact = (count + 1) * (count + 2) * ...* (n - 1) * n

Но мы должны быть уверены, что величина count всегда не отрицательная, по- этому добавим это условие и получим инвариант:

I = (fact = (count + 1) * ...* n) and (count >= 0)

Далее, мы должны проверить, выполняет ли этот инвариант пять требований.

Первое требование.

Опять положим, что I будет использоваться как предусловие (это значит, что первое требование соблюдается).

Второе требование. Ясно, что вычисление булева условия count 0 не влияет на I (тем самым подтвердили второе требование).

Третье требование. Следующий вопрос: истинность

Это предложение редуцируется до (fact = (count + 1) * ...* n) and (count > 0).

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

Для {P} count = count - 1 {I} вычисляемое P примет вид:

{(fact = count * (count + 1) * ...* n) and (count >= 1)}

Используем его как постусловие для 1-го присваивания в теле цикла:

{P} fact = fact * count {(fact = count * (count + 1) * ...* n) and (count >= 1)}

В этом случае P равно:

{(fact = (count + 1) * ...* n) and (count >= 1)}

Сравним это значение со значением I and B. Поскольку предусловие всегда можно усилить, третье требование исполнено.

Четвертое требование. Наконец, четвертая проверка касается утверждения:

(I and (not B)) ^ Q

200

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

Для нашего примера это означает:

Совершенно ясно, что при count = 0 левая часть является точным определением факториала.

Следовательно, созданное высказывание I признается истинным инвариантом. Теперь можно использовать утверждение Р (то же, что и I) из while-оператора как постусловие для второго оператора присваивания в программе:

и сформировать утверждение для предусловия 2-го оператора:

(1 = (count + 1) * ...* n) and (count >= 0)

Используя его как постусловие для 1-го оператора присваивания в программе {P} count = n {(1 = (count + 1) * ...* n) and (count >= 0)} получим для предусловия P 1-го оператора:

{(n + 1) * ...* n = 1) and (n >= 0)}

Левый операнд логического умножения равен истине (так как 1 = 1), а правый операнд точно совпадает с предусловием всей программы {n > 0}. Таким образом, правильность программы доказана.

<< | >>

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

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