Методы верификации программного обеспечения

часть программы на определенном языке, а 

и 

— формулы исчисления 
высказываний, зависящие от переменных, входящих в P. 

интерпретируется 
как условие, выполнение перед началом исполнения P (предусловие), а 

— как 
условие, которое должно быть выполнено после этого исполнения 
(постусловие). Если 

действительно всегда истинно после исполнения P в 
состоянии, где истинно 

, такая тройка тоже считается истинной.
В логике Хоара для некоторого языка программирования семантика этого языка 
задается в виде правил вывода, которые позволяют выводить шаг за шагом 
истинные тройки Хоара из тавтологий, тождественно истинных высказываний. 

Обобщением логик Хоара являются динамические или программные логики 
(dynamic logics, program logics) [140,141]. Они являются специальным типом 
модальных логик, в которых операторы модальности связаны с инструкциями 
программ. Обычно используются операторы [P] и
, где P — некоторая 
программа. Утверждение [P]

означает, что всегда после выполнения 
программы P формула 

истинна, а 

— что после выполнения P 

может 

---

58 
оказаться истинной. Тройка Хоара {

}P{

} может быть представлена в 
динамической логике как 


[P]

. 

Программные контракты (software contracts) [142,143], наоборот, являются 
частным случаем логики Хоара, сужающим возможности использования 
логических формул.
Программный контракт представляет собой описание поведения набора 
программных компонентов представленное в виде описания сигнатур операций 
каждого из этих компонентов, структур их состояний, а также предусловий и 
постусловий для каждой операции и наборов инвариантов для каждого 
компонента в отдельности.
Инвариант компонента является предикатом, зависящим от элементов состояния 
этого компонента, который должен быть выполнен в состояниях, когда ни одна 
из операций компонента не выполняется (т.е. либо еще не была вызвана, либо 
уже завершила работу). Инварианты описывают ограничения целостности 
внутренних данных компонента, и обязанность соблюдать их ложится на его 
реализацию.
Предусловие операции компонента представляет собой предикат, зависящий от 
элементов состояния этого компонента и параметров этой операции, который 
должен быть выполнен при корректных обращениях к этой операции извне 
компонента. При вызове операции с нарушением предусловия ее поведение не 
определено. Предусловие является частью контракта, которую обязано 
соблюдать окружение компонента, чтобы обеспечить его корректную работу. 
Постусловие операции представляет собой предикат, зависящий от параметров 
операции, ее результата, элементов состояния компонента до вызова операции и 
тех же элементов после окончания ее работы. Постусловие должно выполняться 
сразу после окончания работы операции, вызванной с выполненным 
предусловием, и формализует ответственность реализации компонента за 
корректность его работы.
Контракты часто невозможно выполнить непосредственно, поскольку 
постусловия не определяют прямо корректные результаты операций и 
следующие состояния, а лишь оценивают переданные им данные. 

---

59