Формула корректности

Пусть А - это некоторая операция (оператор или тело программы). Формула корректности (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}