Методы Флойда

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

Как и в примере, доказательство полной корректности будет проводиться в два этапа. Сначала доказывается частичная корректность программы. Для этого мы будем использовать метод индуктивных утверждений Флойда. Вторым шагом проводится доказательство завершаемости программы. Для решения этой задачи мы будем использовать метод фундированных множеств Флойда.

Метод индуктивных утверждений Флойда

Будем рассматривать пути в блок-схемах и обозначать их следующим образом: \( \alpha \) – путь в блок-схеме, начинающийся со связки \( e_1 \) и завершающийся связкой \( e_k \) (связка \( e_1 \) выходит из некоторого оператора \( n_1 \), связка \( e_k \) входит в некоторый оператор \( n_{k+1} \) ): \( n_1 - e_1 \to n_2 - e_2 \to \ldots - e_k \to n_{k+1}\). Внутри этого пути находятся операторы \( n_2, n_3, \ldots n_k \).

Дадим несколько вспомогательных определений. Определим предикат допустимости пути \(\alpha\) (или просто предикат пути \( \alpha \)) \( \mbox{R}_{\alpha}(\mathbf{x}, \mathbf{y}): \mbox{D}_{\mathbf{x}} \times \mbox{D}_{\mathbf{y}} \to \{ \mbox{T}, \mbox{F} \} \) и функцию пути \( \alpha - \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y}): \mbox{D}_{\mathbf{x}} \times \mbox{D}_{\mathbf{y}} \to \mbox{D}_{\mathbf{y}} \). Предикат пути \( \mbox{R}_{\alpha}(\mathbf{x}, \mathbf{y}) \) определяет, какое должно быть значение входных и промежуточных переменных в начале пути (в момент выполнения перехода по связке \( e_1 \)), чтобы дальнейшее вычисление шло по пути \( \alpha \). Функция пути \( \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y}) \) определяет, как изменятся значения промежуточных переменных в результате исполнения последователь-ности операторов блок-схемы, находящихся внутри пути \( \alpha \).

Наиболее простым способом составления формул для предиката пути \( \mbox{R}_{\alpha}(\mathbf{x}, \mathbf{y}) \) и функции пути \( \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y}) \) является метод обратных подстановок.

Для каждого \( m \in \{ 1, \ldots, k \} \) определим предикат \( \mbox{R}_{\alpha}^m(\mathbf{x}, \mathbf{y}) \) и функцию \( \mbox{r}_{\alpha}^m(\mathbf{x}, \mathbf{y}) \). При m k это будут предикат и функция пути, состоящего из одной связки (внутри этого пути не будет ни одного оператора). А при положительных целых m < k это будут предикат и функция пути от связки \( e_m \) в связку \( e_k \) (т. е. пути \( n_m - e_m \to n_{m+1} - e_{m+1} \to \ldots \to n_k - e_k \to n_{k+1}\), проходящего через операторы \( n_{m+1}, \ldots, n_k \) ).

Таким образом,

\( \mbox{R}_{\alpha}(\mathbf{x}, \mathbf{y}) \equiv \mbox{R}_{\alpha}^1(\mathbf{x}, \mathbf{y}) \)

\( \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y}) \equiv \mbox{r}_{\alpha}^1(\mathbf{x}, \mathbf{y}) \)

Предикаты \( \mbox{R}_{\alpha}^m(\mathbf{x}, \mathbf{y}) \) и функции  \( \mbox{r}_{\alpha}^m(\mathbf{x}, \mathbf{y}) \) определим индукцией по m.

Базис индукции (для путей, состоящих из одной связи):

\( \mbox{R}_{\alpha}^k(\mathbf{x}, \mathbf{y}) \equiv \mbox{T} \)

\( \mbox{r}_{\alpha}^k(\mathbf{x}, \mathbf{y}) \equiv \mathbf{y} \)

Индуктивное предположение:

Зафиксируем некоторое \( m < k \). Предположим, что \( \mbox{R}_{\alpha}^{m+1}(\mathbf{x}, \mathbf{y}) \) и \( \mbox{r}_{\alpha}^{m+1}(\mathbf{x}, \mathbf{y}) \) уже определены, т. е. определены предикат и функция пути \( n_{m+1} - e_{m+1} \to \ldots \to n_k - e_k \to n_{k+1}\), проходящего через операторы \( n_{m+2}, \ldots, n_k \).

Индуктивный переход:

Тогда в пути из связки \( e_m \) в связку \( e_k \) cвязка \( e_m \) будет входить в оператор \( n_{m+1} \), за которым идет путь, рассмотренный в индуктивном предположении. Поэтому можно определить \( \mbox{R}_{\alpha}^m(\mathbf{x}, \mathbf{y}) \) и \( \mbox{r}_{\alpha}^m(\mathbf{x}, \mathbf{y}) \) в зависимости от оператора \( n_{m+1} \):

Обратите внимание, что в этом перечислении нет начального и завершающего оператора — причина в том, что эти операторы не могут встречаться внутри пути. Однако в них могут входить и выходить первая или последняя связка пути. Если началом первой связки пути \( \alpha \) является начальный оператор START: \( \mathbf{y} \gets f(\mathbf{x}) \), то будем использовать предикат \(\mbox{R'}_{\alpha}(\mathbf{x}) \equiv \mbox{R}_{\alpha}(\mathbf{x}, f(\mathbf{x})) \wedge f(\mathbf{x}) \neq \omega \) и функцию \( \mbox{r'}_{\alpha}(\mathbf{x}) \equiv \mbox{r}_{\alpha}(\mathbf{x}, f(\mathbf{x})) \). Если концом последней связки пути \( \alpha \) является завершающий оператор HALT: \( \mathbf{z} \gets h(\mathbf{x}) \), то будем использовать предикат \( \mbox{R''}_{\alpha}(\mathbf{x}, \mathbf{y}) \equiv \mbox{R}_{\alpha}(\mathbf{x}, \mathbf{y}) \wedge h(\mathbf{x}, \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y})) \neq \omega \) и функцию \( \mbox{r''}_{\alpha}(\mathbf{x}, \mathbf{y}) \equiv h(\mathbf{x}, \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y})) \) \( (\mbox{r''}_{\alpha}(\mathbf{x}, \mathbf{y}): \mbox{D}_{\mathbf{x}} \times \mbox{D}_{\mathbf{y}} \to \mbox{D}_{\mathbf{z}}) \).

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

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

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

Шаг 2. Индуктивные утверждения. Выберем для каждой точки сечения i предикат \( p_i(\mathbf{x}, \mathbf{y}) \), который характеризует отношение между переменными блок-схемы при прохождении данной связки. Будем называть эти предикаты индуктивными утверждениями. Кроме того, свяжем входной предикат \( \varphi(\mathbf{x}) \) с начальным оператором блок-схемы, а выходной предикат \( \psi(\mathbf{x}, \mathbf{z}) \) – со всеми завершающими операторами.

Шаг 3. Условия верификации. На третьем шаге сконструируем для каждого промежуточного базового пути \( \alpha \), начинающегося в точке сечения i и завершающегося в точке сечения j, условия верификации: $$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}, \forall \mathbf{y} \in \mbox{D}_{\mathbf{y}}: [ \varphi(\mathbf{x}) \wedge \mbox{p}_i(\mathbf{x},\mathbf{y}) \wedge \mbox{R}_{\alpha}(\mathbf{x},\mathbf{y}) \Rightarrow \mbox{p}_j(\mathbf{x}, r_{\alpha}(\mathbf{x}, \mathbf{y}))] $$

Эти условия утверждают, что если предикат \( \mbox{p}_i(\mathbf{x},\mathbf{y}) \) истинен для некоторых значений переменных x и y, и эти значения такие, что, начиная из точки сечения i, вычисление пойдет по пути \(\alpha\) и успешно достигнет конца пути, то предикат \( \mbox{p}_j(\mathbf{x},\mathbf{y}) \) будет истинен для значений переменных x и y, после прохождения по пути \( \alpha \).

Для начального базового пути \( \alpha \), завершающегося в точке сечения j, условия верификации будут выглядеть следующим образом: $$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}: [ \varphi(\mathbf{x}) \wedge \mbox{R'}_{\alpha}(\mathbf{x}) \Rightarrow \mbox{p}_j(\mathbf{x}, r'_{\alpha}(\mathbf{x}))] $$

В этом случае условия утверждают, что если входной предикат \( \varphi(\mathbf{x}) \) истинен для некоторых значений входных переменных и эти значения такие, что начальное вычисление пойдет по пути \( \alpha \) и успешно достигнет конца пути, то предикат \( \mbox{p}_j(\mathbf{x},\mathbf{y}) \) будет истинен для значений переменных x и y, после прохождения по пути \( \alpha \).

Для каждого конечного базового пути \( \alpha \), начинающегося в точке сечения i, условия верификации конструируются следующим образом: $$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}, \forall \mathbf{y} \in \mbox{D}_{\mathbf{y}}: [ \varphi(\mathbf{x}) \wedge \mbox{p}_i(\mathbf{x},\mathbf{y}) \wedge \mbox{R''}_{\alpha}(\mathbf{x},\mathbf{y}) \Rightarrow \psi(\mathbf{x}, r''_{\alpha}(\mathbf{x}, \mathbf{y}))] $$

Здесь условия верификации утверждают, что если предикат \( \mbox{p}_i(\mathbf{x},\mathbf{y}) \) истинен для некоторых значений переменных x и y и эти значения такие, что, начиная из точки сечения i, вычисление пойдет по пути \( \alpha \), то предикат  \( \psi(\mathbf{x},\mathbf{z}) \) будет истинен для значений переменных x и z после успешного завершения работы блок-схемы при прохождении по пути \( \alpha \).

Если в блок-схеме существуют простые базовые пути, то для каждого такого пути \( \alpha \) (входящего в оператор HALT с функцией h) условия верификации будут выглядеть следующим образом: $$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}: [ \varphi(\mathbf{x}) \wedge \mbox{R'}_{\alpha}(\mathbf{x}) \wedge h(\mathbf{x}, r'_{\alpha}(\mathbf{x})) \neq \omega \Rightarrow \psi(\mathbf{x}, h(\mathbf{x}, r'_{\alpha}(\mathbf{x}) ) ) ] $$

В этом случае условия утверждают, что если входной предикат \( \varphi(\mathbf{x}) \) истинен для некоторых значений входных переменных и эти значения такие, что вычисление пойдет по пути \( \alpha \) и успешно достигнет его конца, то выходной предикат \( \psi(\mathbf{x}, \mathbf{y}) \) будет истинен для значений переменных x и z после завершения работы блок-схемы при прохождении по пути \( \alpha \).

Лемма 5. Пусть все условия верификации истинны. Пусть дано вычисление блок-схемы P, входные переменные которого удовлетворяют входному предикату \( \varphi \). Тогда для каждого прохода вычисления \( C_k - C_{k+1} \) через точку сечения i, предикат \( \mbox{p}_i(\mathbf{x},\mathbf{y}) \) будет истинен на значениях переменных x и y в конфигурации \( C_k \).

Теорема 1. (Метод индуктивных утверждений Флойда)

Пусть даны блок-схема P и ее спецификация \( \Phi = (\varphi, \psi) \). Выполним следующие действия:

  1. Выберем точки сечения;

  2. Найдем подходящий набор индуктивных утверждений;

  3. Построим условия верификации для всех базовых путей.

Если все условия шага 3 истинны, то блок-схема P частично корректна относительно спецификации \( \Phi \).

Доказательство леммы и теоремы предоставляется читателю в качестве упражнения.

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

Метод фундированных множеств Флойда

Далее мы рассмотрим метод доказательства завершаемости программ, представленных в виде блок-схем.

Напомним некоторые определения. Частично-упорядоченным множеством \( (\mbox{W}, \prec) \) называется непустое множество W и любое бинарное отношение \( \prec \) на этом множестве, которое удовлетворяет следующим свойствам:

  1. Для всех \( a,b,c \in \mbox{W} \) из \( a \prec b \) и \( b \prec c \) следует \( a \prec c \) [Транзитивность].

  2. Для всех \( a,b \in \mbox{W} \) из \( a \prec b \) следует \( \neg (b \prec a) \) [Асимметричность].

  3. Для всех \( a \in \mbox{W}: \neg (a \prec a) \) [Иррефлексивность].

Знаком \( \succ \) будем обозначать бинарное отношение, такое, что для любых \( a,b \in \mbox{W} a \succ b \) тогда и только тогда, когда \( b \prec a \). Частично-упорядоченное множество \(  ( \mbox{W}, \prec ) \) называется фундированным, если не существует бесконечно убывающей последовательности его элементов, т. е. такой последовательности \( \{ a_i \} \), что \( a_1 \succ a_2 \succ a_3 \succ \ldots \). Наиболее известным примером фундированного множества является множество натуральных чисел с отношением порядка \( < \).

Пусть P – блок-схема, а \( \varphi \) – ее входной предикат. Рассмотрим следующий метод доказательства завершаемости программы P на \( \varphi \).

Шаг 1. Точки сечения. Выберем множество точек сечения блок-схемы таким образом, чтобы каждый цикл в блок-схеме содержал, по крайней мере, одну точку сечения, и некоторое фундированное множество \(  ( \mbox{W}, \prec ) \). Для каждой точки сечения i выберем индуктивное утверждение \( q_i(\mathbf{x}, \mathbf{y}) \). Построим условия верификации для индуктивных утверждений \( q_i(\mathbf{x}, \mathbf{y}) \) согласно методу, рассмотренному ранее, для начальных базовых и промежуточных базовых путей и докажем их истинность.

Шаг 2. Оценочные функции. Определим для каждой точки сечения i оценочную функцию \( u_i(\mathbf{x}, \mathbf{y}): \mbox{D}_{\mathbf{x}} \times \mbox{D}_{\mathbf{y}} \to \mbox{W}_i \), где \(\mbox{W}_i \supseteq \mbox{W} \), и сформулируем условие корректности определения оценочной функции:

$$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}, \forall \mathbf{y} \in \mbox{D}_{\mathbf{y}}: [ \varphi(\mathbf{x}) \wedge q_i(\mathbf{x}, \mathbf{y}) \Rightarrow u_i(\mathbf{x}, \mathbf{y}) \in \mbox{W} ] $$

Это условие утверждает, что для всех векторов значений переменных x и y, удовлетворяющих в точке сечения i индуктивному утверждению \( q_i(\mathbf{x}, \mathbf{y}) \), оценочная функция ставит в соответствие элемент множества W (а не его надмножества).

Шаг 3. Условия завершимости. Сконструируем для каждого промежуточного базового пути \( \alpha \), начинающегося в точке сечения i и завершающегося в точке сечения j, условие завершимости:

$$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}, \forall \mathbf{y} \in \mbox{D}_{\mathbf{y}}: [ \varphi(\mathbf{x}) \wedge q_i(\mathbf{x}, \mathbf{y}) \wedge \mbox{R}_{\alpha}(\mathbf{x}, \mathbf{y}) \Rightarrow u_j(\mathbf{x}, \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y}) ) \prec u_i(\mathbf{x}, \mathbf{y}) ] $$

Условие завершимости утверждает, что если предикат \( q_i(\mathbf{x}, \mathbf{y}) \) истинен для некоторых значений переменных x и y, и эти значения такие, что, начиная из точки сечения i, вычисление пойдет по пути \( \alpha \), то результат оценочной функции \( u_j(\mathbf{x}, \mathbf{y}) \)на значениях переменных x и y после прохождения по пути \( \alpha \) будет меньше результата оценочной функции \( u_i(\mathbf{x}, \mathbf{y}) \) на исходных значениях.

Шаг 4. Условия успешности вычисления функций. Для доказательства полной корректности необходимо показать, что функции, приписанные операторам блок-схемы, которые могут равняться \( \omega \), не вызываются с такими аргументами, при которых они равны \( \omega \).

Для оператора START, которому приписана функция f, составим следующее условие успешности вычисления функции f:

$$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}: [ \varphi(\mathbf{x}) \Rightarrow f(\mathbf{x}) \neq \omega ] $$

Для каждого пути \( \alpha \), начинающегося в точке сечения i, не содержащего в себе других точек сечения и завершающегося перед оператором ASSIGN с функцией g, составим следующее условие успешности вычисления функции g:

$$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}, \forall \mathbf{y} \in \mbox{D}_{\mathbf{y}}: [ \varphi(\mathbf{x}) \wedge q_i(\mathbf{x}, \mathbf{y}) \wedge \mbox{R}_{\alpha}(\mathbf{x},\mathbf{y}) \Rightarrow g(\mathbf{x}, \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y})) \neq \omega ] $$

Аналогичные условия составим для каждого пути \( \alpha \), начинающегося в точке сечения i, не содержащего в себе других точек сечения и завершающегося перед оператором HALT с функцией h:

$$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}, \forall \mathbf{y} \in \mbox{D}_{\mathbf{y}}: [ \varphi(\mathbf{x}) \wedge q_i(\mathbf{x}, \mathbf{y}) \wedge \mbox{R}_{\alpha}(\mathbf{x},\mathbf{y}) \Rightarrow h(\mathbf{x}, \mbox{r}_{\alpha}(\mathbf{x}, \mathbf{y})) \neq \omega ] $$

Теорема 2. (Метод фундированных множеств Флойда)

Пусть даны блок-схема P и ее входной предикат \( \varphi \). Выполним следующие действия:

  1. Выберем точки сечения с подходящим набором индуктивных утверждений и фундированное множество;

  2. Выберем подходящий набор оценочных функций;

  3. Построим условия верификации для всех базовых начальных и промежуточных путей, условия корректности определения всех оценочных функций и условия завершимости для всех промежуточных базовых путей.

  4. Построим условия успешности вычисления функций, приписанных всем операторам START, ASSIGN и HALT.

Если все условия на шагах 3 и 4 истинны, то блок-схема P успешно завершается на \( \varphi \).

Доказательство теоремы предоставляется читателю в качестве упражнения.

Замечания к методам Флойда

При доказательстве полной корректности блок-схемы на этапе доказательства завершаемости можно использовать те же точки се­чения и индуктивные утверждения, которые были использованы для доказательства частичной корректности. Это позволит сокра­тить объем доказательства полной корректности. Однако если ин­дуктивные утверждения достаточно громоздки, при доказательстве завершаемости следует рассмотреть возможность использования «новых» индуктивных утверждений, более компактных.

После успешного доказательства частичной корректности с не­которыми индуктивными утверждениями можно использовать их следствия при доказательстве успешной завершимости и не состав­лять и передоказывать условия верификации для них.

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

Тем не менее, в некоторых случаях можно вносить такое «изме­нение» в индуктивное утверждение как «приписывание предусло­вия». А именно, в условиях верификации, завершимости и кор­ректности определения оценочной функции можно дописывать в конъюнкцию посылки импликации входной предикат, т. к. значе­ния входных переменных не меняются во время выполнения блок-схемы. Например, условие верификации для промежуточного базо­вого пути можно изменить следующим образом:

$$ \forall \mathbf{x} \in \mbox{D}_{\mathbf{x}}, \forall \mathbf{y} \in \mbox{D}_{\mathbf{y}}: [ p_i(\mathbf{x}, \mathbf{y}) \wedge \varphi(\mathbf{x}) \wedge \mbox{R}_{\alpha}(\mathbf{x}, \mathbf{y}) \Rightarrow p_j(\mathbf{x}, r_{\alpha}(\mathbf{x}, \mathbf{y}))] $$

Доказательство полной корректности программы цело­численного деления при помощи методов Флойда

Докажем полную корректность блок-схемы целочисленного де­ления, представленной на рисунке, относительно следующей спе­цификации:

$$ \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) $$

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

Доказываем частичную корректность. Выберем в качестве единственную точку сечения – В. Она разбивает единственный цикл в этой блок-схеме. Сопоставим этой точке сечения индуктив­ное утверждение \( p(x_1, x_2, y_1, y_2) \equiv (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \). Необходимо составить условия верификации для следую­щих путей в блок-схеме: START – B, B – T – B, B – F – HALT.

Условие верификации для пути START – B:

$$ \forall x_1, x_2 \in \mathbb{Z}: [\varphi(x_1, x_2) \Rightarrow p(x_1, x_2, 0, x_1)] $$

Подставляем определения предикатов:

$$ \forall x_1, x_2 \in \mathbb{Z}: [(x_1 \geq 0) \wedge (x_2 > 0) \Rightarrow (x_1 = 0 \cdot x_2 + x_1) \wedge (x_1 \geq 0) ] $$

Очевидно, что данное утверждение истинно.

Условие верификации для пути B – T – B:

$$ \forall x_1, x_2, y_1, y_2 \in \mathbb{Z}: [ (x_1 \geq 0) \wedge (x_2 > 0) \wedge p(x_1, x_2, y_1, y_2) \wedge (y_2 \geq x_2) \Rightarrow p(x_1, x_2, y_1 + 1, y_2 - x_2) ]$$

Подставляем определения предикатов:

$$ \forall x_1, x_2, y_1, y_2 \in \mathbb{Z}: [ (x_1 \geq 0) \wedge (x_2 > 0) \wedge (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) ]$$

Достаточно раскрыть скобки и убедиться в истинности этого утверждения.

Условие верификации для пути B – F – HALT:

$$ \forall x_1, x_2, y_1, y_2 \in \mathbb{Z}: [ (x_1 \geq 0) \wedge (x_2 > 0) \wedge p(x_1, x_2, y_1, y_2) \wedge \neg (y_2 \geq x_2) \Rightarrow \psi(x_1, x_2, y_1, y_2) ]$$

Подставляем определения предикатов:

$$ \forall x_1, x_2, y_1, y_2 \in \mathbb{Z}: [ (x_1 \geq 0) \wedge (x_2 > 0) \wedge (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge \neg (y_2 \geq x_2) \Rightarrow (x_1 = y_1 x_2 + y_2) \wedge (0 \leq y_2 < x_2) ]$$

Очевидно, что и это утверждение истинно.

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

Доказываем завершаемость блок-схемы целочисленного деления на рисунке при всех значениях входных данных, удовлетворяю­щих предикату \( \varphi \equiv (x_2 \geq 0) \wedge (x_2 > 0) \)

В качестве множества точек сечения выберем единственную точку сечения В (ту же, которая была использована для доказательства частичной корректности) и стандартное фундированное множество \( ( \{0,1,2,\ldots \}, <) \). В этой точке сечения выберем то же индуктивное утверждение, которое было использовано при доказательстве частичной корректности, а в качестве оценочной функции выберем функцию \( u \equiv y_2 \) (см. рисунок ниже). В этом случае условия верификации повторно составлять не нужно – их мы возьмем из доказательства частичной корректности. Необходимо составить условие корректности определения оценочной функции для точки сечения В и условие завершимости для единственного промежуточного базового пути B – T – B.

Условие корректности определения оценочной функции в точке сечения В:

$$ \forall x_1, x_2, y_1, y_2 \in \mathbb{Z}: [ (x_1 \geq 0) \wedge (x_2 > 0) \wedge p(x_1, x_2, y_1, y_2) \Rightarrow u(x_1, x_2, y_1, y_2) \in \mathbf{W} ] $$

Подставляем определения предиката p, функции u и множества W:

$$ \forall x_1, x_2, y_1, y_2 \in \mathbb{Z}: [ (x_1 \geq 0) \wedge (x_2 > 0) \wedge (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \Rightarrow (y_2 \geq 0) ] $$

Очевидно, что это условие истинно.

Условие завершимости для пути B – T – B:

$$ \forall x_1, x_2, y_1, y_2 \in \mathbb{Z}: [ (x_1 \geq 0) \wedge (x_2 > 0) \wedge p(x_1, x_2, y_1, y_2) \wedge (y_2 \geq x_2) \Rightarrow u(x_1, x_2, y_1, y_2) > u(x_1, x_2, y_1 + 1, y_2 - x_2) ]$$

Подставляем определения предиката p и функции u:

$$ \forall x_1, x_2, y_1, y_2 \in \mathbb{Z}: [ (x_1 \geq 0) \wedge (x_2 > 0) \wedge (x_1 = y_1 x_2 + y_2) \wedge (y_2 \geq 0) \wedge (y_2 \geq x_2) \Rightarrow y_2 > y_2 - x_2 ]$$

Это условие является истинным.

Тем самым, согласно теореме 2, блок-схема целочисленного деления завершается при всех значениях входных данных, удовлетворяющих предикату \( \varphi \).

Нами доказана частичная корректность и завершаемость блок-схемы, а, значит, доказана ее полная корректность.

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

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

1. В блок-схеме на рисунке заданы путь \( \alpha \) и предикат \( p_1: \mbox{D}_{\mathbf{x}} \times \mbox{D}_{\mathbf{y}} \to \{\mbox{T}, \mbox{F}\} \) – на значения входных и промежуточных переменных в начале этого пути.

Записать точный предикат \( p_2: \mbox{D}_{\mathbf{x}} \times \mbox{D}_{\mathbf{y}} \to \{\mbox{T}, \mbox{F}\} \) – на значения входных и промежуточных переменных в конце этого пути, если вычисление идет по пути и начинается из конфигурации со значениями входных и промежуточных переменных, удовлетворяющими предикату \( p_1 \).

Т.е. записать предикат \( p_2 \), истинный на тех и только тех значениях \( x' \in \mbox{D}_{\mathbf{x}} \) и \( y' \in \mbox{D}_{\mathbf{y}} \), для которых существуют \( x \in \mbox{D}_{\mathbf{x}} \) и \( y \in \mbox{D}_{\mathbf{y}} \) такие, что выполнено \( p_1(x,y) \), и существует вычисление, начинающееся в конфигурации со значениями переменных (x, y), выполняющееся по пути \( \alpha \) и завершающееся в конфигурации в конце пути со значениями переменных \( x', y' \). Множество переменных \( \mbox{V} = \{x, y_1, y_2, z\} \) состоит из одной входной, двух промежуточных и одной выходной переменной. Доменами всех переменных является множество целых чисел.

    1. \( \alpha \): B – C; p1(x, y1, y2) = (x = 0 y1 = 0 ∧ y2 = 1)

    2. \( \alpha \): B – C; p1(x, y1, y2) = (y2 = 1)

    3. \( \alpha \): B – C; p1(x, y1, y2) = (y1 = x)

    4. \( \alpha \): B – C; p1(x, y1, y2) = (1 < y1 < 10 ∧ y2 > x)

    5. \( \alpha \): B – C – B; p1(x, y1, y2) = (y1·x = y2)

    6. \( \alpha \): B – C – B – C – B; p1(x, y1, y2) = (y1·x = y2)

    7. \( \alpha \): C – B – C; p1(x, y1, y2) = (y1·x = y2)

    8. \( \alpha \): C – B – C; p1(x, y1, y2) = (y2 < 0)

    9. \( \alpha \): A – B – C – A; p1(x, y1, y2) = (y1x)

    10. \( \alpha \): B – C – D; p1(x, y1, y2) = (y1 = 1 ∧ y2 = 0)

    11. \( \alpha \): B – C – D; p1(x, y1, y2) = (y1 = 1)

    12. \( \alpha \): START – A – B – C – B – C – A – D – HALT; p1(x, y1, y2) = (x = 2 ∧ 0 ≤ y1 < x)

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

a) \( \varphi(x) = (x > 0) \)

\( \psi(x, z) = (z > 0) \)

\( p_A(x, y_1, y_2) = (y_1 \geq 2 y_2) \)

\( W = (Nat_0, <) \)

\( u_A (x, y_1, y_2) = y_1 \)

b) \( \varphi(x) = (|x| < 10) \)

\( \psi(x, z) = (|x| = |z|) \)

\( p_A(x, y_1, y_2) = (y_1 = -x) \)

\( p_B(x, y_1, y_2) = (y_1 = -x) \)

\( p_C(x, y_1, y_2) = (y_2 = x \wedge x > 0) \)

\( W = (Nat_0, <) \)

\( u_B(x, y_1, y_2) = y_1 - 1 \)

\( u_A(x, y_1, y_2) = y_1 \)

\( u_C(x, y_1, y_2) = y_1 \)

c) \( \varphi(x) = (x > 0) \)

\( \psi(x,z) = (z \geq x) \)

\( p_A(x, y_1, y_2) = (y_1 = x) \)

\( W = (Nat_0, <) \)

\( u_A (x, y_1, y_2) = y_2 \)

d) \( \varphi(x) = (|x| < 5) \)

\( \psi(x,z) = (z \geq 0) \)

\( p_A(x, y_1, y_2) = (y_1 = -x) \)

\( p_B(x, y_1, y_2) = (y_1 = -x) \)

\( p_C(x, y_1, y_2) = (y_2 = x \wedge x > 0) \)

\( W = (Nat_0, <) \)

\( u_B(x, y_1, y_2) = y_1 - 1 \)

\( u_A(x, y_1, y_2) = y_1 \)

\( u_C(x, y_1, y_2) = y_1 \)

e) \( \varphi(x) = (x \geq 0) \)

\( \psi(x, z) = (z > 0) \)

\( p_A(x, y_1, y_2) = (y_2 = x) \)

\( p_B(x, y_1, y_2) = (y_2 = x) \)

\( p_C(x, y_1, y_2) = (y_2 = x \wedge y_1 \geq 0) \)

\( W = (Nat_0, <) \)

\( u_A(x, y_1, y_2) = y_1 + 2 \)

\( u_B(x, y_1, y_2) = y_1 \)

\( u_C(x, y_1, y_2) = y_1 + 1 \)

f) \( \varphi(x) = (x \geq 0) \)

\( \psi(x, z) = (|z| = x) \)

\( p_A(x, y_1, y_2) = (y_2 = x \wedge y_1 = 0) \)

\( p_B(x, y_1, y_2) = (y_2 = 0 \to y_1 = 0) \)

\( p_C(x, y_1, y_2) = (2 y_1 = y_2 + x) \)

\( W = (Nat_0, <) \)

\( u_C (x, y_1, y_2) = y_2 - 1 \)

\( u_A (x, y_1, y_2) = y_2 \)

\( u_B(x, y_1, y_2) = y_2 + 1 \)

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

Спецификация: φ(x) = T, ψ(x, z) = (z = 2x)

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

Спецификация: φ(x1, x2) = (x2 0), ψ(x1, x2, z1, z2) = (z1 - x1 = z2x2)

5. При помощи метода индуктивных утверждений доказать, что следующая блок-схема частично корректна относительно указанной спецификации (φ, ψ), доменом всех переменных является множество всех целых чисел:

φ(x) = (x 0), ψ(x, z) = (z2 x < (z + 1)2)

6. Следующая функция языка Си была промоделирована указанной ниже блок-схемой. В блок-схеме выделена точка сечения А, которой приписано утверждение p(x, y1, y2) = (0 ≤ y1 < x). Обос­нуйте или опровергните следующее утверждение: p выполнено вся­кий раз, когда вычисление находится в точке А (т. е. может быть использовано для доказательства частичной корректности). Функ­ция вызывается только с положительными значениями х.

int sum(int x) {
    int i = 0, s = 0;
    for(; i < x; i++)
    {
        s += i;
    }
    return s;
}

7. Обоснованно ответить на вопрос: какое требуется мини­мальное число точек сечения, чтобы доказать частичную коррект­ность хотя бы одной блок-схемы, имеющей указанные особенности, относительно хотя бы одной спецификации при помощи методов Флойда, если блок-схемы с указанными особенностями существу­ют.

Если ответ зависит от спецификации, привести не менее двух разных ответов и обосновать их.

  1. блок-схема содержит 2 цикла;

  2. блок-схема содержит не менее одного оператора соединения;

  3. блок-схема зацикливается на всех значениях входных данных из своих доменов;

  4. операторы и связки блок-схемы разбиваются на 3 независи­мые связные части так, что первая и вторая часть обладают единственной общей связкой, вторая и третья часть обладают единственной общей связкой, а первая и третья часть не об­ладают общими связками. Общих операторов у частей нет.

8. Обоснованно ответить на вопрос: какое требуется мини­мальное число точек сечения, чтобы доказать завершаемость хотя бы одной блок-схемы, имеющей указанные особенности, относи­тельно хотя бы одной спецификации при помощи методов Флойда, если блок-схемы с указанными особенностями существуют. Если ответ зависит от спецификации, привести не менее двух разных от­ветов и обосновать их. Если доказать завершаемость невозможно, обоснуйте это.

  1. блок-схема содержит 2 цикла;

  2. блок-схема содержит не менее одного оператора соединения;

  3. блок-схема зацикливается на всех значениях входных данных из своих доменов;

  4. операторы и связки блок-схемы разбиваются на 3 независи­мые связные части так, что первая и вторая часть обладают единственной общей связкой, вторая и третья часть обладают единственной общей связкой, а первая и третья часть не об­ладают общими связками. Общих операторов у частей нет.

9. Дано выражение. Обосновать или опровергнуть утверждение: существует блок-схема P, спецификация (, ψ) для нее и доказательство Pψ при помощи методов Флойда, в котором данное выражение используется в качестве оценочной функции.

  1. x (x – целое число);

  2. x2 (x – целое число);

  3. sin2 x + cos2 x (x – вещественное число);

  4. 1 / x (x – вещественное число);

  5. x (x – очередь из целых чисел);

  6. x (x – очередь из неотрицательных целых чисел).

10. Каково минимальное и максимальное число утверждений, которые необходимо доказать при использовании лишь одной точки сечения в рамках доказательства частичной корректности P (она задана в виде программой на языке Си)? полной корректности?

Ответ обосновать. Если одной точки сечения недостаточно, обосновать это. Напишите, как зависит ответ от спецификации этой блок-схемы.

  1. int P(int x) {
        int y1 = x, y2 = x;
        do { 
            if (y1 > y2 + y2) { y2 ++; }
            y1 += y2; 
        } while (y1 < y2); 
        return y1 + y2;
    }
  2. int P(int x1, int x2) {
        int y1 = x1, y2 = x2; 
        while (x1 > y1) { 
            switch (y1 + y2) { 
                case 0: y1++; 
                case 1: y2++; 
            } 
            return -1; 
        } 
        return y1 + y2;
    }
    
  3. int P(int x1, int x2) {
        int y1 = x1, y2 = x2, y3 = 0; 
        while (y3 < x) {
            if (y1 < y2) return y3;
            y1 = y2 = y3; 
        }
        while (y2 > 0) { 
            if (y1 < 2 * y3) break;
            y2--; 
        }
        return 0;
    }
  4. char *strcpy(char *dest, const char *src) {
        char *p = dest, *q = src;
        while (*q != 0) {
            *p = *q; q++; 
        } 
        return dest;
    }

11. Можно ли только при помощи методов Флойда доказать, что в указанной функции на языке Си значение указанной пере­менной всегда принадлежит указанному множеству значений? Если да, покажите, как (предъявив хотя бы несколько формальных вы­кладок). Если нет, обоснуйте это. Если спецификация не указана, считается, что она содержит тождественно истинные предусловие и постусловие. Если в этой функции указанная переменная не всегда принадлежит указанному множеству значений, обоснуйте это.

  1. void swap(int *x, int *y) { 
        int t = *x; 
        *x = *y; 
        *y = t;
    }

    Переменная: x; область значений: ненулевые указатели.

  2. int abs(int *x) {
        int y = -1; 
        if (x != 0 && (y = *x) < 0) 
        {
            *x = - y; 
            return *x; 
        }
        return -1;
    }

    Переменная: y; область значений: отрицательные числа; предусловие: x != 0.

  3. int search(int x, int *data, size_t len) { 
        int i = 0; 
        for ( ; i < len; i++) {
            if (data[i] == x) return i; 
        }
        return -1;
    }

    Переменная: i; область значений: 0 <= i < len.

12. Можно ли только при помощи методов Флойда доказать, что в приведенной ниже функции на языке Си никогда не выпол­няется указанное условие на значения переменных? Если да, пока­жите, как (предъявив хотя бы несколько формальных выкладок). Если нет, обоснуйте это. Если спецификация не указана, считается, что она содержит тождественно истинные предусловие и постусло­вие. Если в функции указанное условие может быть выполнено, обоснуйте это.

  1. void swap(int *x, int *y) { 
        int t = *x; 
        *x = *y; 
        *y = t;
    }

    Непосредственно в этой функции происходит разыменование нулевого указателя.

  2. long list_sum(struct node_t *list) {
        long sum = 0L; 
        struct_node_t *p = list; 
        while (p != 0) {
            sum += p->value; 
            p = p->next;
        }
        return sum;
    }

    Сумма элементов списка из одного элемента больше заглавного элемента.