3. Доказательство свойств программы.

14.3.1. Обоснования программ. Формализация свойств программ.

Для повышения надежности программных средств весьма полезно снабжать программы дополнительной информацией, с использованием которой можно существенно повысить уровень контроля ПС. Такую информацию можно задавать в форме неформализованных или формализованных утверждений, привязываемых к различным фрагментам программ. Будем называть такие утверждения обоснованиями программы. Неформализованные обоснования программ могут, например, объяснять мотивы принятия тех или иных решений, что может существенно облегчить поиск и исправление ошибок, а также изучение программ при их сопровождении. Формализованные же обоснования позволяют доказывать некоторые свойства программ как вручную, так и контролировать (устанавливать) их автоматически.

Одной из используемых в настоящее время концепций формальных обоснований программ является использование так называемых триад Хоора. Пусть S - некоторый обобщенный оператор над информационной средой IS, P и Q - некоторые предикаты (утверждения) над этой средой. Тогда запись {P}S{Q} и называют триадой Хоора, в которой предикат P называют предусловием, а предикат Q - постусловием относительно оператора S. Говорят, что оператор (в частности, программа) S обладает свойством {P}S{Q}, если всякий раз, когда перед выполнением оператора S истинен предикат P, после выполнения этого оператора S будет истинен предикат Q.

Простые примеры свойств программ:

(1) {n=0} n:=n+1 {n=1},

(2) {n<m} n:=n+k {n<m+k},

(3) {n<m+k} n:=3*n {n<3*(m+k)},

(4) {n>0} p:=1; m:=1;

ПОКА m /= n ДЕЛАТЬ

m:=m+1; p:=p*m

ВСЕ ПОКА

{p=n!}.

Для доказательства свойства программы S используются свойства простых операторов языка программирования (мы здесь ограничимся пустым оператором и оператором присваивания) и свойствами управляющих конструкций (композиций), с помощью которых строится программа из простых операторов (мы здесь ограничимся тремя основными композициями структурного программирования, см. Лекцию 8). Эти свойства называют обычно правилами верификации программ.

2. Свойства простых операторов.

Для пустого оператора справедлива

Теорема 4.1. Пусть P - предикат над информационной средой. Тогда имеет место свойство {P}{P}.

Доказательство этой теоремы очевидно: пустой оператор не изменяет состояние информационной среды (в соответствии со своей семантикой), поэтому его предусловие сохраняет истинность и после его выполнения.

Для оператора присваивания справедлива

Теорема 4.2. Пусть информационная среда IS состоит из переменной X и остальной части информационной среды RIS:

IS = {X, RIS}.

Тогда имеет место свойство

{Q(F(X, RIS), RIS)} X:= F(X, RIS) {Q(X, RIS)} ,

где F(X, RIS) - некоторая однозначная функция, Q - предикат.

Доказательство. Пусть до выполнения оператора присваивания был истинен предикат Q(F(X0, RIS0), RIS0), где {X0, RIS0} - некоторое произвольное состояние информационной среды IS, тогда после выполнения оператора присваивания будет истинен предикат Q(X, RIS), так как X получит значение F(X0, RIS0), а состояние RIS не изменяется данным оператором присваивания, и, следовательно, после выполнения этого оператора присваивания в этом случае

Q(X, RIS)=Q(F(X0, RIS0), RIS0).

В силу произвольности выбора состояния информационной среды теорема доказана.

Примером свойства оператора присваивания может служит пример 9.1.