Полезное:
Как сделать разговор полезным и приятным
Как сделать объемную звезду своими руками
Как сделать то, что делать не хочется?
Как сделать погремушку
Как сделать так чтобы женщины сами знакомились с вами
Как сделать идею коммерческой
Как сделать хорошую растяжку ног?
Как сделать наш разум здоровым?
Как сделать, чтобы люди обманывали меньше
Вопрос 4. Как сделать так, чтобы вас уважали и ценили?
Как сделать лучше себе и другим людям
Как сделать свидание интересным?
Категории:
АрхитектураАстрономияБиологияГеографияГеологияИнформатикаИскусствоИсторияКулинарияКультураМаркетингМатематикаМедицинаМенеджментОхрана трудаПравоПроизводствоПсихологияРелигияСоциологияСпортТехникаФизикаФилософияХимияЭкологияЭкономикаЭлектроника
|
Правила верификации К. Хоара.Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям. A1. Аксиома присваивания: { Ro } x:= Е { R } Неформальное объяснение аксиомы: так как x после выполнения будет содержать значение Е, то R будет истинно после выполнения, если результат подстановки Е вместо x в R истинен перед выполнением. Таким образом, Ro = R(x) при x = E. Для Ro вводится обозначение: Ro = RxЕ (у Вирта) или Rx→Е (у Дейкстры), что означает, что x заменяется на Е. Аксиома присваивания будет иметь вид:{RxЕ} x:= Е {R}. Сформулируем два очевидных правила монотонности. A2. Если известно: { Q } S { P } и { P } => { R }, то { Q } S { R } A3. Если известно: { Q } S { P } и { R } => { Q }, то { R } S { P } Пусть S - это последовательность из двух операторов S1; S2 (составной оператор). A4. Если известно:{ Q } S1 { P1 } и { P1 } S2 { R }, то { Q } S { R }. Это правило можно сформулировать для последовательности, состоящей из n операторов. Сформулируем правило для условного оператора (краткая форма). A5. Если известно: { Q AND B } S1 { R } и { Q NOT B } => { R },то { Q } if B then S1 { R }. Правило A5 соответствует интерпретации условного оператора в языке программирования. Сформулируем правило для альтернативного оператора (полная форма условного оператора). A6. Если известно: { Q AND B } S1 { R } и { Q NOT B } S2 { R },то { Q } if B then S1 else S2 { R }. Сформулируем правила для операторов цикла. Предусловия и постусловия цикла until удовлетворяют правилу: A7. Если известно: { Q AND NOT B } S1 { Q }, то { Q } repeat S1 until B { Q AND NOT B } Правило отражает инвариантность цикла. В данном случае единственная операция - это выполнение шага цикла при условии истинности Q вначале. Предусловия и постусловия цикла while удовлетворяют правилу: A8. Если известно: { Q AND B } S1 { Q }, то { Q } while B do S1 { Q AND NOT B } Правила A1 - A8 можно использовать для проверки согласованности передачи данных от оператора к оператору, для анализа структурных свойств текстов программ, для установления условий окончания цикла и для анализа результатов выполнения программы. Пример 2.12. Пусть надо определить частное q и остаток r от деления x на y. Входные данные x, y и выходные данные q, r Î Nat, причем y > 0. Задать(x,y); /* x,y получают конкретные значения X,Y */ r:= x; q:= 0; while y £ r do Begin r:= r - y; q:= q + 1 end; выдать(q,r); Сформулируем постусловие R: (r < y) AND (x = y*q + r) Нужно доказать, что {y > 0 AND x/y} S {(r < y) AND (x = y*q + r)}. Доказательство. 1. Очевидно, что Q => x = x + y * 0. 2. Применим аксиому A1 к оператору r:= x, тогда получим { x = x + y * 0 } r:= x { x = r + y * 0 } 3. Аналогично, применяя A1 к оператору q:= 0, получим: { x = r + y * 0 } q:= 0 { x = r + y*q } 4. Применяя правило A3 к результатам пунктов 1 и 2, получим { Q } r:= x { x = r + y * 0 } 5. Применяя правило A4 к результатам пунктов 4 и 3, получим { Q } r:= x; q:= 0 { x = r + y*q } 6. Выполним равносильное преобразование x = r + y * q AND y £ r => x = (r - y) + y*(q + 1) 7. Применяя правило A1 к оператору r:= r - y, получим {x = (r - y) + y*(q + 1)} r:= r - y {x = r+ y*(q+1)} 8. Для оператора q:= q + 1 аналогично получим { x = r + y*(q + 1) } q:= q + 1 { x = r + y*q }
|