Задача верификации

Частичная и полная корректность программ

Пусть программа задана своей моделью в виде блок-схемы P, а ее спецификация \(\Phi\) – предикатами \(\varphi\) и \(\psi\). Мы будем говорить, что

Заметим, что полная корректность программы P относительно входного предиката \(\varphi\) и выходного предиката T эквивалентна тому, что программа P завершается всегда, когда вектор значений входных переменных удовлетворяет \(\varphi\). В этом случае мы будем говорить, что P завершается на \(\varphi\). Напомним, что это означает, что соответствующее вычисление заканчивается в одном из операторов HALT со значениями всех переменных не равными \(\omega\).

Лемма 2. Пусть даны программа P и спецификация \(\Phi = (\varphi, \psi) \). В этом случае \( \langle \varphi \rangle \mbox{P} \langle \psi \rangle \) тогда и только тогда, когда \( \{\varphi\} \mbox{P} \{\psi\} \) и \( \langle \varphi \rangle \mbox{P} \langle \mbox{T} \rangle \).

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

Из определения корректности также следует, что и частичная, и полная корректность сохраняется при замене входного предиката на более сильный и выходного на более слабый. Таким образом, верна следующая лемма:

Лемма 3. Пусть дана программа P. Пусть предикаты \( \varphi, \varphi', \psi, \psi' \) таковы, что формулы \( \varphi' \to \varphi \) и \( \psi \to \psi' \) истинны. Тогда:

Следующая лемма позволяет по нескольким утверждениям о частичной и полной корректности получать новые утверждения:

Лемма 4. Пусть дана программа P. Тогда для любых предикатов \( \varphi, \psi_1, \psi_2 \) выполнены следующие утверждения:

Верификация программы целочисленного деления

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

Для этого вернемся к программе целочисленного деления, блок-схема которой представлена на рисунке (далее она будет обозначаться как \(\mbox{P}_{div}\) ). Мы докажем ее полную корректность относительно спецификации, заданной следующими предикатами:

\( \varphi \equiv (x_1 \geq 0) \wedge (x_2 > 0) \)

\( \psi \equiv (x_1 = z_1 x_2 + z_2) \wedge (0 \leq z_2 < x_2) \)

Входной предикат спецификации утверждает, что нас будет интересовать поведение программы только на неотрицательных значениях переменной \( x_1 \) и положительных значениях переменной \( x_2 \). Выходной предикат определяет, что значения выходных переменных программы должно удовлетворять определению целочисленного деления с остатком.

Доказательство полной корректности будет разбито на два этапа. Сначала мы докажем, что программа является частично корректной относительно входного предиката \( \varphi_0 \equiv (x_1 \geq 0) \wedge (x_2 \geq 0) \) и выходного предиката \( \psi \). А затем мы докажем завершаемость программы на \( \varphi \). Из этого, по леммам 2 и 3, будет следовать требуемое утверждение.

Заметим, что входной предикат \( \varphi_0 \), используемый при доказательстве частичной корректности, является более слабым, чем \( \varphi \). Это связано с тем, что при значении входной переменной \( x_2 \) равном 0, программа является частично корректной, но не завершается.

Частичная корректность. Поставим в соответствие начальному оператору блок-схемы входной предикат \( \varphi_0 \), завершающему оператору – выходной предикат \( \psi \), а ребру между оператором соединения и условным оператором – промежуточный предикат p, задаваемый формулой \( \mbox{p}(x_1, x_2, y_1, y_2) \equiv (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \). Это ребро на рисунке ниже обозначено буквой B.

  1. Рассмотрим путь от начального оператора программы до ребра B. После выполнения начального оператора переменные принимают следующие значения:
    \(x_1\) \(x_1\)
    \(x_2\) \(x_2\)
    \(y_1\) 0
    \(y_2\) \(x_1\)
    Таким образом, $$ \mbox{p}(x_1, x_2, y_1, y_2) \equiv (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \equiv (x_1 = 0 \cdot x_2 + x_1) \wedge (x_1 \geq 0) \equiv (x_1 \geq 0). $$ Последнее неравенство является истинным в предположении, что выполнено предусловие программы \( \varphi_0 \equiv (x_1 \geq 0) \wedge (x_2 \geq 0) \). То есть: \( \varphi_0 \Rightarrow (x_1 \geq 0) \).
  2. Предположим, что предикат p истинен в точке B и рассмотрим путь B-D-B. После выполнения условного оператора значения переменных не изменяются, то есть в точке D предикат p также будет истинен, а так как точка D лежит на ребре, помеченном символом T, то в точке D будет истинно следующее утверждение: $$ (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge (y_2 \geq x_2)  $$ Докажем, что после выполнения последующего оператора присваивания предикат p также будет истинен. $$ D: (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge (y_2 \geq x_2) $$ $$ B: p(x_1, x_2, y_1 + 1, y_2 - x_2) \equiv (x_1 = (y_1 + 1) \cdot x_2 + y_2 - x_2) \wedge (y_2 - x_2 \geq 0) $$ поэтому нужно доказать, что истинно утверждение: $$ (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge (y_2 \geq x_2) \Rightarrow (x_1 = (y_1 + 1) \cdot x_2 + y_2 - x_2) \wedge (y_2 - x_2 \geq 0) $$ $$ (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge (y_2 \geq x_2) \Rightarrow (x_1 = y_1 x_2 + y_2) \wedge (y_2 - x_2 \geq 0) $$ $$ T $$
  3. В завершение рассмотрим последний путь: от точки B до завершающего оператора. Предположим, что в точке B истинен предикат p. Тогда при попадании в точку E будет истинно следующее утверждение: $$ (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge (y_2 < x_2) $$ Докажем, что после завершающего оператора будет истинен выходной предикат \( \psi \): $$ E: (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge (y_2 < x_2) $$ $$ C: \psi(x_1, x_2, y_1, y_2) \equiv (x_1 = y_1 x_2 + y_2) \wedge (0 \leq y_2 < x_2) $$ для этого необходимо показать, что истинно следующее утверждение: $$ (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge (y_2 < x_2) \Rightarrow (x_1 = y_1 x_2 + y_2) \wedge (0 \leq y_2 < x_2) $$ $$ T $$

Из рассмотренных свойств программы следует, что для любого конечного вычисления программы целочисленного деления при значениях входных переменных, удовлетворяющих предусловию, значения выходных переменных будут удовлетворять постусловию. Или, другими словами, что программа целочисленного деления является частично корректной относительно спецификации \( \Phi_0 = (\varphi_0, \psi) \).

Завершаемость. До сих пор мы доказали корректность про­граммы только условно. Мы доказали, что если программа завер­шается, то ее результат удовлетворяет предъявляемым к нему тре­бованиям. Теперь докажем, что программа целочисленного деления действительно завершается при значениях входных переменных, удовлетворяющих входному предикату \( \varphi \).Во время доказательства частичной корректности программы мы доказали, что если значения входных переменных удовлетворя­ют предикату \( \varphi_0 \), то при всяком прохождении точки B значения входных и промежуточных переменных будут удовлетворять следую­щему условию: \( (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \). Из этого следует, что если значения входных переменных удовлетворяют более силь­ному предикату \( \varphi \), то при всяком прохождении точки B значение промежуточной переменной \( y_2 \) будет неотрицательным. С другой стороны, значения входных переменных не изменяются в ходе вы­полнения программы, поэтому предикат \( \varphi \) является истинным в любой промежуточной точке. Отсюда следует, что в точке B будет выполнено следующее условие: \( (y_2 \geq 0) \wedge (x_2 > 0) \).Рассмотрим цикл B-D-B. После прохождения этого пути значе­ние переменной \( y_2 \) уменьшится на положительную величину ( \( x_2 \) ). С другой стороны, значение переменной \( y_2 \) останется неотрицательным. И так как не существует бесконечной убывающей последова­тельности неотрицательных целых чисел, то цикл B-D-B не может выполняться бесконечное число раз, если значения входных пере­менных программы удовлетворяли предикату \( \varphi \). Следовательно, программа целочисленного деления завершается на входном предикатe \( \varphi \).Мы доказали, что \( \{ \varphi_0 \} \mbox{P}_{div} \{ \psi \} \)  и \( \langle \varphi \rangle \mbox{P}_{div} \langle \mbox{T} \rangle \). Отсюда, по леммам 2 и 3, следует \( \langle \varphi \rangle \mbox{P}_{div} \langle \psi \rangle \), то есть полная корректность программы цело­численного деления относительно \( \varphi \) и \( \psi \).

Задачи и упражнения

  1. Для приведенной ниже блок-схемы и каждой из спецификаций ответить на вопрос, является ли эта блок-схема частично корректной относительно этой спецификации, является ли эта блок-схема полностью корректной относительно той же спецификации. Множество переменных состоит из одной входной, двух промежуточных и одной выходной переменной \( \mbox{V} = \{ x, y_1, y_2, z \} \). Доменом всех переменных является множество целых чисел.

    1. \( \varphi(x) = (x = 0); \psi(x,z) = (z=0) \)

    2. \( \varphi(x) = (x = 0); \psi(x,z) = (z=1) \)

    3. \( \varphi(x) = (x \geq 0); \psi(x,z) = (z=x^2) \)

    4. \( \varphi(x) = \mbox{T}; \psi(x,z) = (z=x^2) \)

    5. \( \varphi(x) = (|x| > 10); \psi(x,z) = (|z|>100) \)

    6. \( \varphi(x) = (x > 0); \psi(x,z) = (z>x) \)

    7. \( \varphi(x) = (x \geq 0); \psi(x,z) = (z \geq x) \)

  2. Для каждой из указанных ниже спецификаций приведите следующие блок-схемы или обоснуйте, почему они не существуют. Доменом всех входных, промежуточных и выходных переменных должно быть множество целых чисел. В качестве функций, приписанных операторам блок-схемы, можно использовать любую функцию, задаваемую арифметической формулой над операциями сложения, вычитания и умножения, и операциями сравнения (равно, неравно, больше, меньше и т. п.).

    • не являющуюся частично корректной относительно данной спецификации;

    • являющуюся частично корректной, но не являющуюся полностью корректной относительно данной спецификации;

    • являющуюся частично, но не полностью корректной относительно данной спецификации, и при этом завершающуюся на максимально возможном числе входных данных (т. е. завершающуюся при всех значениях входных данных, удовлетворяющих предусловию, при которых существуют значения выходных переменных, на которых выполнено постусловие);

    • являющуюся полностью корректной относительно данной спецификации.

    1. \( \varphi(x) = \mbox{T}; \psi(x,z) = \mbox{T} \)

    2. \( \varphi(x) = \mbox{T}; \psi(x,z) = \mbox{F} \)

    3. \( \varphi(x) = \mbox{F}; \psi(x,z) = \mbox{T} \)

    4. \( \varphi(x) = (x=0); \psi(x,z) = (z=0) \)

    5. \( \varphi(x_1, x_2) = (x_1 = x_2); \psi(x_1, x_2 ,z) = (x_1 = z + x_2) \)

    6. \( \varphi(x_1, x_2) = (x_1 > x_2 \geq 0); \psi(x_1, x_2 ,z_1, z_2) = (z_1 > x_1 > z_2 > x_2) \)

    7. \( \varphi(x_1, x_2) = (0 > x_1 > x_2); \psi(x_1, x_2 ,z_1, z_2) = (x_1^2 > z_1 > x_2^2 > z_2) \)

    8. \( \varphi(x_1, x_2) = (x_1 > x_2 \geq 0); \psi(x_1, x_2 ,z_1, z_2) = (x_2^2 > z_1 > x_1^2 > z_2) \)

    9. \( \varphi(x_1) = (x_1 > 0); \psi(x_1,z_1, z_2) = (z_1 = x_1 \cdot z_2) \wedge (z_1 < z_2) \)

    10. \( \varphi(x_1, x_2) = (x_1 + x_2 < 3); \psi(x_1, x_2 ,z_1, z_2) = (z_1 + x_2 > z_2) \wedge (z_1<x_1 + z_2) \)

  3. Доказать или опровергнуть утверждение. Заглавными буквами обозначены блок-схемы, строчными — предикаты.

    1. \( \forall a \forall \mbox{P} \exists b: \{ a \} \mbox{P} \{ b \} \Rightarrow \{ b \} \mbox{P} \{ a \} \)

    2. \( \forall a \forall \mbox{P} \exists b: \langle a \rangle \mbox{P} \langle b \rangle \Rightarrow \langle b \rangle \mbox{P} \langle a \rangle \)

    3. \( \forall \mbox{P} \exists a \exists b: \{ a \} \mbox{P} \{ b \} \)

    4. \( \forall \mbox{P} \exists a \exists b: \langle a \rangle \mbox{P} \langle b \rangle \)

    5. \( \forall \mbox{P} \exists a \exists b: \{ a \} \mbox{P} \{ b \} \wedge \neg \langle a \rangle \mbox{P} \langle b \rangle \)