Полезное:
Как сделать разговор полезным и приятным
Как сделать объемную звезду своими руками
Как сделать то, что делать не хочется?
Как сделать погремушку
Как сделать так чтобы женщины сами знакомились с вами
Как сделать идею коммерческой
Как сделать хорошую растяжку ног?
Как сделать наш разум здоровым?
Как сделать, чтобы люди обманывали меньше
Вопрос 4. Как сделать так, чтобы вас уважали и ценили?
Как сделать лучше себе и другим людям
Как сделать свидание интересным?
Категории:
АрхитектураАстрономияБиологияГеографияГеологияИнформатикаИскусствоИсторияКулинарияКультураМаркетингМатематикаМедицинаМенеджментОхрана трудаПравоПроизводствоПсихологияРелигияСоциологияСпортТехникаФизикаФилософияХимияЭкологияЭкономикаЭлектроника
Формула корректности
|
|
Пусть А - это некоторая операция (оператор или тело программы). Формула корректности (correctness formula) - это выражение в форме:
{P} A {Q}
Формула выражает свойство, которое может быть или не быть истинным:
Смысл формулы корректности {P} A {Q}
Любое выполнение А, начинающееся в состоянии, где P истинно, завершится и в заключительном состоянии будет истинно Q.
Формула корректности, называемая также триадой Хоара, - математическое понятие, а не программистская конструкция. Она не является частью языка программирования и введена для того, чтобы выражать свойства программных элементов. В этой формуле А, как было сказано, обозначает операцию, P и Q - свойства вовлекаемых в рассмотрение сущностей, называемые утверждениями (точный смысл этого термина будет определен ниже). Утверждение P называется предусловием, а Q - постусловием.
С этого момента обсуждение корректности ПО будет связываться не с программным элементом А, а с триадой, содержащей этот элемент А, предусловие P и постусловие Q. Единственной целью становится установление того, что триада Хоара {P} A {Q} выполняется (истинна).
Вот пример выполняемой тривиальной формулы, в которой полагается, что x имеет тип integer:
{x>=9} x:= x+5 {x>=13}
| Число 13 в постусловии не опечатка. Предполагая корректную реализацию целочисленной арифметики, данная формула действительно выполняется. Если предусловие x>=9 выполняется перед присваиванием, то x>=13 будет истинным по завершении оператора присваивания. Конечно, можно утверждать более интересную вещь: при заданном предусловии сильнейшим, насколько это возможно, будет постусловие x>=14. В свою очередь, при заданном постусловии x>=13 слабейшим предусловием будет x>=8. Из выполняемой формулы корректности всегда можно породить новые выполняемые формулы, ослабляя постусловие или усиливая предусловие. Займемся теперь выяснением того, что означают термины "сильнее" и "слабее" в пред- и постусловиях. |
Date: 2015-12-13; view: 424; Нарушение авторских прав