|
Пусть P(x,z) - программа P с входными аргументами x и выходными z. Пусть Q(y) - некоторое логическое условие (предикат) над переменными программы y. Язык для записи предикатов Q(y) формализовать не будем. Отметим только, что он может быть шире языка, на котором записываются условия в программах, и включать, например, кванторы. Предусловием программы P(x,z) будем называть предикат Pre(x), заданный на входах программы. Постусловием программы P(x,z) будем называть предикат Post(x,z), связывающий входы и выходы программы. Для простоты будем полагать, что программа P не изменяет своих входов x в процессе своей работы. Теперь несколько определений:
Определение 1 (частичной корректности): Программа P(x,z) корректна (частично, или условно) по отношению к предусловию Pre(x) и постусловию Post(x,z), если из истинности предиката Pre(x) следует, что для программы P(x,z), запущенной на входе x, гарантируется выполнение предиката Post(x,z) при условии завершения программы.
Условие частичной корректности записывается в виде триады Хоара, связывающей программу с ее предусловием и постусловием:
[Pre(x)]P(x,z)[Post(x,z)]
Определение 2 (полной корректности): Программа P(x,z) корректна (полностью, или тотально) по отношению к предусловию Pre(x) и постусловию Post(x,z), если из истинности предиката Pre(x) следует, что для программы P(x,z), запущенной на входе x, гарантируется ее завершение и выполнение предиката Post(x,z).
Условие полной корректности записывается в виде триады Хоара, связывающей программу с ее предусловием и постусловием:
{Pre(x)}P(x,z){Post(x,z)}
Доказательство полной корректности обычно состоит из двух независимых этапов - доказательства частичной корректности и доказательства завершаемости программы
|