Вопрос №12 . Основные правила аналитической верификации программ №12

Правило (определение) 1. Программа S обладает свойством {P} S {Q}, где P и Q  некоторые утверждения о значениях используемых в программе переменных, если каждому набору начальных значений переменных, относительно которых справедливо P, отвечают после завершения программы S такие значения переменных, относительно которых справедливо Q.

Иногда P называют предусловием (предутверждением), Q  постусловием (постутверждением), а пару P и Q  спецификацией программы S. Программу называют корректной относительно спецификации, если она обладает свойством {P} S {Q}. Более точно, имеется в виду частичная корректность программы, поскольку свойство завершимости программы здесь предполагается и должно доказываться отдельно. Запись {P} S {Q} называют также тройкой Хоара.

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

Правило 2 (последовательного соединения). Пусть S₁ и S₂ – программы, обладающие свойствами {P} S₁ {R} и {R} S₂ {Q}. Тогда программа S  begin S₁; S₂ end обладает свойством {P} S {Q}.

Док-во: если до выполнения программы S было справедливо утверждение P, то после завершения первой части S₁ будет справедливо R, но тогда по свойству второй части {R} S₂ {Q} после завершения S₂ будет справедливо Q.

Это правило иногда записывают в форме так называемого правила вывода исчисления высказываний (предикатов)

{P} S₁ {R}, {R} S₂ {Q}

, (2.1)

{P} S {Q}

где над горизонтальной чертой располагают посылки, а под ней – следствие.

Об утверждениях A и B говорят, что A сильнее B, а B слабее A, если A  B (из A следует B). В утверждениях о переменных программы более слабое утверждение налагает меньше ограничений на переменные программы. Отсутствие ограничений соответствует самому слабому утверждению, тождественному значению True.

Пусть программа S имеет свойство {P} S {Q}. Можно ли применить программу S в другом контексте, например: {P₁} S {Q₁}? Это возможно, если выполняются соотношения P₁  P и Q  Q₁, и такой вывод следует непосредственно из правила 1. В свойстве {P₁} S {Q₁} по сравнению с исходным свойством {P} S {Q} усилено предусловие и ослаблено постусловие.

Правило 3 (об усилении предусловия и ослаблении постусловия). Пусть имеются свойство {P} S {Q} и утверждения P₁ и Q₁, такие, что P₁  P и Q  Q₁, тогда имеет место свойство {P₁} S {Q₁}.

В форме правила вывода это можно записать в виде

P₁  P, {P} S {Q}, Q  Q₁

 . (2,2)

{P₁} S {Q₁}

С точки зрения универсальности программы S правило 3 обосновывает естественное стремление найти такое св--во, в котором P было бы как можно слабее, а Q  как можно сильнее.

Основным элементарным оператором любой программы является оператор присваивания.

Правило 4 (свойство оператора присваивания). Пусть E – выражение, P – утверждение, а P(x  E) означает утверждение, полученное из утверждения P заменой всех вхождений переменной x на выражение E. Тогда оператор присваивания обладает свойством

{ P(x  E) } x := E {P}. (2.3) Запись (2.3) означает, что, если до выполнения присваивания верно утверждение P(x  E), то после выполнения будет верным утверждение P.

Доказательство свойства (2.3). Обозначим все переменные программы как a, b, ..., z (кроме уже выделенной переменной x). Пусть до выполнения оператора присваивания все переменные принимали значения a₀, b₀, ..., z₀ (включая x₀), а после выполнения  a₁, b₁, ..., z₁. Будем считать, что x₁ = E(x₀, a₀, b₀, ..., z₀), a₁ = a₀, b₁ = b₀, ..., z₁ = z₀. (2.4)

Цепочка равенств в (2.4), начиная со второго, означает, что при вычислении выражения E(x, a, b, ..., z) отсутствует побочный эффект. Пусть P = P(x, a, b, ..., z) и до выполнения оператора присваивания было справедливо P(x  E), т. е. P( E(x₀, a₀, b₀, ..., z₀),  a₀, b₀, ..., z₀), тогда с учетом (2.4) будет справедливо P(x₁, a₁, b₁, ..., z₁).

Оказывается, что верно и утверждение, обратное (2.3): если после выполнения присваивания верно утверждение P, то до выполнения было верно утверждение P(x  E).

Доказательство. Пусть после завершения присваивания справедливо утверждение P(x₁, a₁, b₁, ..., z₁), тогда с учетом (2.4) будет справедливо и утверждение P( E(x₀, a₀, b₀, ..., z₀), a₀, b₀, ..., z₀), т. е. P(x  E).

Итак, правило 4 можно усилить и сформулировать так: для того чтобы после завершения присваивания x := E было справедливо утверждение о переменных программы P, необходимо и достаточно, чтобы до выполнения оператора x := E было справедливо утверждение P(x  E).

Необходимость, а не только достаточность, условия P(x  E) можно интерпретировать следующим образом: предусловие P(x  E) является слабейшим из всех предусловий R, таких, что имеется свойство {R} x: = E {P} при заданном постусловии P.

В общем случае для заданных программы S и постусловия P слабейшее предусловие для P относительно S – это предикат, обозначаемый wp(S  P) и описывающий самое слабое условие, которому достаточно подчинить начальное состояние для того, чтобы выполнение программы S завершилось и привело к заключительному состоянию, удовлетворяющему P. В этих обозначениях P(x  E)  wp(S  P).

Итак, для проверки свойства {R} x := E {P} рекомендуется сначала найти wp(x := E  P), т. е. P(x  E), а затем проверить R  wp(x := E  P).

Примеры: 1) проверим свойство {(x = 2^p + 1) & (p > 0)} x := x mod 2 {x = 1}, где p: Integer; действительно, следуя рекомендации, имеем

wp(x := x mod 2 x = 1)  (x mod 2 = 1)  Odd(x)

и затем {(x = 2^p + 1) & (p > 0)}  Odd(x), что и доказывает требуемое;

2) рассмотрим следующее свойство:

{(x = a) & (y = b)} x := x + y; y := x – y; x := x  y {(x = b) & (y = a)},которое позволяет интерпретировать данную последовательность присваиваний как операцию обмена значений переменных x и y; для проверки этого свойства применяем правила 2 и 4, раccматривая отдельные операторы присваивания в порядке, обратном их выполнению:

wp (x := x  y  (x = b) & (y = a))  (x  y = b) & (y = a),

wp (y := x  y  (x – y = b) & (y = a))  (y = b) & (x  y = a),

wp (x := x + y  (y = b) & (x  y = a))  (y = b) & (x = a).

Вопрос №13 Правила вывода для структурных операторов :усл.опер,цикла с пред- постусловием №13

Правило 5 (для условного оператора). Пусть рассматривается свойство условного оператора

{P} if B then S₁ else S₂ {Q}. (2.5)

Для того чтобы это св-во имело место, необходимо и достаточно наличие свойств {P & B} S₁ {Q} и {P & not B} S₂ {Q}.

Док-во. Необходимость: пусть имеется (2.5); если условие B выполнено, то, в силу семантики оператора if-then-else, должен выполняться оператор S₁, но тогда должно быть {P & B} S₁ {Q}. Аналогично рассматривается случай, когда выполнено not B. Достаточность: пусть перед выполнением условного оператора справедливы P и B, тогда будет выполняться then-ветвь, а поскольку имеет место свойство {P & B} S₁ {Q}}, то после выполнения будет справедливо утверждение Q. Аналогично рассматривается выполнение else-ветви при справедливости P & not B.

Правило 6 (для цикла while-do). Пусть рассматривается оператор цикла while B do S, и пусть утверждение P таково, что тело цикла S обладает свойством {P & B} S {P}, тогда оператор цикла обладает свойством {P} while B do S {P & not B}.

В форме правила вывода это записывается так:

{P&B} S {P}

   . (2,6)

{P} while B do S {P & not B}

Док-во. Пусть имеет место св-во {P & B} S {P} и перед входом в цикл справедливо P, тогда либо условие продолжения цикла B не выполнено и требуемое постусловие {P & not B} получается сразу, либо условие продолжения B выполнено и тогда работает тело цикла, после чего, в силу свойства {P & B} S {P}, рассмотренная ситуация повторяется. Далее, если цикл завершился, то, рассмотрев последовательность шагов цикла begin S; S; ...; S end, индукцией по числу шагов легко показать, что при последней итерации вновь имеется свойство {P&B} S {P} и, следовательно, при завершении цикла справедливо постусловие {P & not B}.

Утверждение P, которое справедливо перед выполнением цикла и воспроизводится на каждом его шаге (соответственно свойству {P&B} S {P}), называют инвариантом цикла. Иногда его называют инвариантом Хоара или хоаровским инвариантом (по имени К.Хоара, предложившего правило 6).

В некоторых случаях используют более слабое, чем (2.6), правило

{P} S {P}

  .

{P} while B do S {P & not B}

Очевидно, что если тело цикла обладает свойством {P} S {P}, то оно обладает и свойством {P & B} S {P}. Поэтому хоаровский инвариант цикла P можно попытаться получить из инварианта тела цикла, т. е. из такого утверждения P*, что {P*} S {P*}.

Если рассматривается цикл с заданными предусловием Q и постусловием R, т. е. {Q} while B do S {R}, то полезно совместить правила 6 и 3:

Q  P, {P & B} S {P}, P & not B  R

. (2,7)

{Q} while B do S {R}

Не всякий инвариант цикла в смысле (2.6) представляет интерес. Обычно требуется указать либо самый сильный инвариант, либо инвариант, согласованный с постусловием R, т. е. такой, что P & not B  R.

Правило 7 (для цикла repeat-until):

{P} S {Q}, {Q & not B} S {Q}

 , (2,8) {P} repeat S until B {Q & B}

или, в другой форме,

{P} S {Q}, Q & not B  P

 . (2,9) {P} repeat S until B {Q & B}

Форма (2.8) явно предполагает наличие двух свойств тела цикла: для первой итерации и для всех остальных. Форму (2.9) иногда удобнее использовать, чем (2.8), так как в ней фигурирует лишь одно свойство тела цикла, хотя имеется еще дополнительное утверждение Q & not B  P.

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