Корректность программ с предикатной спецификацией

Для класса программ с предикатной спецификацией рассматривается программа вместе со своей спецификацией. Введенное в предыдущем разделе понятие предикатной спецификации уточняется следующим образом: спецификация есть формула P(x) & Q(x, y), где P(x) - предусловие, истинное перед исполнением программы, а Q(x, y) - постусловие, истинное после исполнения программы. Программа S со спецификацией записывается в виде известной тройки Хоара {P(x)} S {Q(x, y)}, см. [9].

Представление о правильности программы принято формулировать в виде понятия корректности программы. Корректность определяется условиями корректности, которые должны быть истинны для правильной программы. Истинность постусловия после завершения исполнения программы, безусловно, является условием корректности программы. Однако данное условие имеет смысл, если программа завершается. Условие того, что программа завершается, также является условием корректности. Поэтому истинность постусловия принято считать частичным условием корректности. Истинность постусловия вместе с условием завершения программы определяет условие полной (или тотальной) корректности программы.

Чтобы полностью записать условие корректности, определяющее истинность постусловия, следует в математическом виде представить эффект исполнения программы. Необходимым инструментом для этого является формальная семантика языка программирования. Различаются следующие виды формальной семантики: денотационная [8], аксиоматическая [9, 10] и операционная [11]. Мы будем использовать новый вид формальной семантики - логическую семантику [2].

Используя логическую семантику, можно построить формулу тотальной корректности программы.

Нашей задачей является разработка методов доказательства корректности программы «вручную», чтобы программист, разработав программу и спецификацию, мог бы доказать ее корректность в традиционном математическом стиле. Здесь необходима техника доказательства снизу вверх: если оператор S состоит из операторов A и B, то сначала следует доказать корректность операторов A и B, а затем по определенным правилам доказывать корректность оператора S. Мы построим систему правил доказательства для трех базисных операторов: оператора суперпозиции A; B, параллельного оператора A || B и условного оператора if ( C) A else B.