Общий случай определения инварианта цикла
Общий случай определения инварианта цикла |
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}. Таким образом, правильность программы доказана.
Еще по теме Общий случай определения инварианта цикла:
-
Windows -
Архитектура компьютера -
Интернет -
Информатика -
Компьютер -
Компьютерные и телекоммуникационные системы -
Программирование -
Социальные сети -
-
Английский язык -
Астрология -
Астрономия -
Биология -
Военная литература -
Журналистика -
Компьютерная инженерия -
Педагогика -
Право -
Психология -
Социология -
Lecture.Center
|