Спецификация программ и преобразователь предикатов

Важнейший для дальнейшего изучения материал этого параграфа в более подробном изложении можно найти в книге [4]. Полезным будет также и знакомство с подходом учебного пособия [9].

Предикаты и документирование программ

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

Задача 6.1. Запишите предикат, утверждающий, что если $$i<j$$, а $$m>n$$, то $$u=v$$.

Решение. В данном случае все очевидно: $$i<j \land m>n \Rightarrow (u=v)$$.

Задача 6.2. Запишите предикат, утверждающий, что ни одно из следующих утверждений не является истинным: $$a<b$$, $$b<c$$ и $$x=y$$.

Решение Это задание тоже не является сложным. Вот несколько эквивалентных между собой решений: $$P_1 = ((a<b) = F) \land ((b<c) = F) \land ((x=y) = F)$$, $$P_2 = !(a<b) \land !(b<c) \land !(x=y)$$ и $$P_3 = a\geqslant b \land b\geqslant c \land x\ne y$$. Так как обычно нужно предъявить максимально простой предикат, то будем считать ответом последний из них — $$P_3$$.

В ряде последующих задач нам придется иметь дело с массивами, поэтому договоримся о следующих обозначениях: будем обозначать вырезку из массива $$b[0..m-1]$$, в которой содержатся все элементы данного массива с индексами от $$j$$ до $$k$$ включительно, символом $$b[j..k]$$. В случаях, когда $$j>k$$, $$k<0$$ или $$j\geqslant m$$, вырезка представляет из себя пустое множество.

Задача 6.3.Запишите предикат, утверждающий, что для массива $$b[0..n-1]$$ длины $$n>0$$ все элементы вырезки $$b[j..k]$$ являются нулевыми.

Решение. Используем квантор всеобщности: $$\forall i\ j\leqslant i<k+1\ b[i]=0$$.

Задача 6.4.Запишите предикат, утверждающий, что для массива $$b[0..n-1]$$ длины $$n>0$$ ни один из элементов вырезки $$b[j..k]$$ не нулевой.

Решение. Переформулировав данное высказывание (все элементы вырезки не нулевые), запишем ответ в следующем виде: $$\forall i\ j\leqslant i<k+1\ b[i]\ne 0$$.

Задача перевода высказывания с естественного языка на язык предикатов не всегда является однозначной, но именно это и является одной из причин его использования. Вот пример.

Задача 6.5. Запишите предикат, утверждающий, что для массива $$b[0..n-1]$$ длины $$n>0$$ некоторые из элементов вырезки $$b[j..k]$$ нулевые.

Решение. Данное высказывание можно понимать двояко: оно может означать, что в вырезке существует хотя бы один нулевой элемент, а может значить и то, что в ней как минимум два нулевых элемента. Вот ответы для каждого из этих вариантов трактовки задачи: $$P_1 = \exists i\ j\leqslant i<k+1\ b[i]=0$$ и $$P_2 = \exists i\ j\leqslant i<k+1\ \exists m\ (j\leqslant m<k+1 \land m \ne i) (b[i]=0)\land (b[m]=0)$$.

Вот аналогичные задачи из области математики.

Задача 6.6. Запишите предикат, который утверждает, что функция $$f\colon \{1, 2, 3, 4, 5\} \rightarrow \{1, 2, 3, 4, 5\}$$ является сюръективной и отрицание этого факта. Упростите получившиеся предикаты, если это возможно.

Решение. В соответствии с определением сюръективности имеем $$P=(\forall y\in \{1, 2, 3, 4, 5\}\ \exists x\in \{1, 2, 3, 4, 5\}\ y = f(x))$$. Построим отрицание и упростим его в соответствии с законами эквивалентности. $$!P = (!(\forall y\in \{1, 2, 3, 4, 5\}\ \exists x\in \{1, 2, 3, 4, 5\} \ y = f(x))) = (\exists y \in \{1, 2, 3, 4, 5\}\ !(\exists x\in \{1, 2, 3, 4, 5\}\ y = f(x))) = (\exists y \in \{1, 2, 3, 4, 5\}\ \forall x \in \{1, 2, 3, 4, 5\}\ !(y = f(x))) = (\exists y \in \{1, 2, 3, 4, 5\} \ \forall x\in \{1, 2, 3, 4, 5\}\ y \ne f(x))$$.

Задача 6.7. Запишите предикат, который утверждает, что функция $$f\colon \{1, 2, 3, 4, 5\} \rightarrow \{1, 2, 3, 4, 5\}$$ все элементы, не превосходящие трех, не увеличивает, и отрицание этого факта. Упростите получившиеся предикаты, если это возможно.

Решение. $$P = (\forall x \in \{1, 2, 3 \}\ f(x) \leqslant x)$$. Его отрицание можно упростить: $$!P = !(\forall x \in \{1, 2, 3 \}\ f(x) \leqslant x) = (\exists x \in \{1, 2, 3 \}\ f(x) > x)$$.

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

Часто, однако, полезно поручить проверку истинности предикатов в процессе выполнения программы непосредственно компьютеру. В различных языках программирования эта возможность реализована по-разному. Например, в программах на языке C можно использовать макрос assert(P), который в случае ложности его аргумента (предиката P ) немедленно прекращает выполнение программы, сообщая о причине этого.

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

Задача 6.8. Напишите программу, содержащую проверку истинности утверждения о положительности введенного с клавиатуры целого числа.

Текст программы

public class Assert {
    public static void main(String[] args) throws Exception {    
        int n = Xterm.inputInt("Введите n -> ");
        if (n <= 0) 
            throw new Exception("n <= 0");
        Xterm.println("n = " + n);
    }
}

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

java.lang.Exception: n<=0
        at Assert.main(Assert.java:4)

Богатые возможности работы с исключениями, имеющиеся в языке, позволяют реализовать гораздо более изощренные способы проверки истинности предикатов, нежели использованный в программе простейший вариант возбуждения исключения типа Exception без попыток его последующей обработки. Эти возможности, однако, не будут рассматриваться в нашем курсе.

Спецификация программы и преобразователь предикатов wp

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

Определение 6.1. Спецификацией $$\{Q\} \; S \; \{R\}$$ программы $$S$$, где $$Q$$ и $$R$$ — предикаты, называется предикат, означающий, что если выполнение $$S$$ началось в состоянии, удовлетворяющем $$Q$$ , то имеется гарантия, что оно завершится через конечное время в состоянии, удовлетворяющем $$R$$.

Под программой $$S$$ в данном определении может пониматься один или несколько отдельных операторов или же действительно целая большая программа.

Определение 6.2. Предикат $$Q$$ называется предусловием или входным утверждением $$S$$ ; $$R$$ — постусловием или выходным утверждением программы $$S$$.

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

Спецификация $$\{i=0\} \; "i++;" \; \{i=1\}$$ является тавтологией, спецификация $$\{i=0\} \; "i++;" \; \{i=0\}$$ ложна во всех состояниях, а спецификация $$\{i=0\} \; "i++;" \; \{i=j\}$$ истинна при $$j=1$$ и ложна в остальных состояниях.

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

Определение 6.3. Программа $$S$$ является правильной при заданных $$Q$$ и $$R$$, если спецификация $$\{Q\} \; S \; \{R\}$$ является тавтологией.

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

Слабейшее предусловие — предикат, описывающий максимально широкое множество в пространстве состояний переменных программы $$S$$, на котором гарантируется получение постусловия $$R$$. Сильнейшее постусловие — предикат, описывающий максимально сильные ограничения на состояние переменных программы $$S$$, которые могут быть получены при данном предусловии $$Q$$.

Для целей доказательства правильности программ особенно важен следующий предикат.

Определение 6.4. Слабейшее предусловие $$wp(S,R)$$ — предикат, представляющий множество всех состояний переменных программы $$S$$, для которых выполнение команды $$S$$, начавшееся в таком состоянии, обязательно закончится через конечное время в состоянии, удовлетворяющем $$R$$.

Проиллюстрируем введенное понятие на нескольких примерах.

$$wp(\Cmd{i = i + 1;}, i\leqslant 1) = (i\leqslant 0)$$, так как если переменная $$i$$ удовлетворяла условию $$i\leqslant 0$$, то после выполнения программы $$\Cmd{i = i + 1;}$$ она действительно будет удовлетворять неравенству $$i\leqslant 1$$.

$$wp(\Cmd{if (x >= y) z=x; else z=y;}, z = max(x, y)) = T$$, ибо выполнение программы $$\Cmd{if (x >= y) z=x; else z=y;}$$ при любых начальных условиях приведет к тому, что переменная $$z$$ станет равной максимальному значению из величин $$x$$ и $$y$$.

$$wp(\Cmd{if (x >= y) z=x; else z=y;}, z = y) = (y \geqslant x)$$, потому что $$y$$ будет равно максимуму из чисел $$x$$ и $$y$$ (а именно таково будет $$z$$ после выполнения программы $$\Cmd{if (x >= y) z=x; else z=y;}$$ ) тогда и только тогда, если именно переменная $$y$$ имеет большее значение.

$$wp(\Cmd{if (x >= y) z=x; else z=y;}, z = y-1) = F$$. Это (пустое множество состояний) означает, что ни при каких начальных условиях программа $$\Cmd{if (x >= y) z=x; else z=y;}$$ не сможет сделать величину $$z$$ меньше, чем $$y$$.

$$wp(\Cmd{if (x >= y) z=x; else z=y;}, z = y+1) = (x=y+1)$$, ибо только при таком начальном условии после выполнения приведенной программы переменная $$z$$ станет равной $$y+1$$.

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

Предложение 6.1. $$\{Q\}\; S\; \{R\} = (Q \Rightarrow wp(S,R))$$.

Определение 6.5. Преобразователем предикатов (обозначаемый через $$wp_S(R)$$ ) называют $$wp(S,R)$$ когда фиксируют программу $$S$$ и рассматривают $$wp(S,R)$$ как функцию одной переменной $$R$$.

Предложение 6.2. Преобразователь предикатов $$wp(S,R)$$ обладает следующими свойствами:

1) $$wp(S,F) = F$$ (закон исключенного чуда);

2) $$wp(S,Q)\land wp(S,R) = wp(S, Q \land R)$$ (дистрибутивность конъюнкции);

3) $$(Q \Rightarrow R) \Rightarrow (wp(S,Q) \Rightarrow wp(S,R))$$ (закон монотонности);

4) $$wp(S,Q) \lor wp(S,R) = wp(S, Q \lor R)$$ (дистрибутивность дизъюнкции).

Величина $$wp(S,F)$$ описывает такое множество начальных условий, при которых выполнение программы $$S$$ завершится через конечное время в состояний, удовлетворяющем $$F$$, то есть ни в каком состоянии. Этого, конечно, быть не может, что и поясняет название свойства — закон исключенного чуда.

Докажем аккуратно дистрибутивность конъюнкции. Для доказательства эквивалентности достаточно показать, что из условия $$wp(S,Q)\land wp(S,R)$$, стоящего в левой части, вытекает условие $$wp(S, Q \land R)$$, размещенное в правой, и наоборот. Для доказательства импликации $$wp(S,Q)\land wp(S,R) \Rightarrow wp(S, Q \land R)$$ рассмотрим произвольное состояние $$s$$, удовлетворяющее условию $$wp(S,Q)\land wp(S,R)$$. Так как выполнение программы $$S$$, начавшееся в $$s$$, завершится при истинных $$Q$$ и $$R$$, то истинным будет и предикат $$Q \land R$$.

Для доказательства обратной импликации $$wp(S, Q \land R) \Rightarrow wp(S,Q)\land wp(S,R)$$ рассмотрим состояние $$s$$, удовлетворяющее условию $$wp(S, Q \land R)$$. Тогда выполнение $$S$$, начавшееся в $$s$$, обязательно завершится в некотором состоянии $$s'$$, удовлетворяющем $$Q \land R$$. Но любое такое $$s'$$ обязательно удовлетворяет и $$Q$$ и $$R$$, так что $$s$$ удовлетворяет и $$wp(S,Q)$$ и $$wp(S,R)$$, что и завершает доказательство.

Закон монотонности докажите самостоятельно, а вот по поводу последнего свойства преобразователя предикатов — дистрибутивности дизъюнкции — надо сделать некоторые замечания. Дело в том, что если в качестве $$S$$ рассмотреть операцию бросания монеты, которая может завершиться либо выпадением герба ( $$G$$ ), либо решки ( $$R$$ ), то $$wp(S,G) = wp(S,R) = F$$, ибо нельзя гарантированно предсказать результат бросания ни при каких начальных условиях. С другой стороны, $$wp(S,G \lor R) = T$$, так как всегда выпадет либо герб, либо решка.

Если $$S$$ является недетерминированной, то эквивалентность в законе дистрибутивности дизъюнкции превращается в импликацию. Однако для программ $$S$$, реализованных с помощью большинства языков программирования, подобная ситуация невозможна.

Определение простейших операторов языка Java

До сих пор все наши манипуляции с $$wp$$ основывались на том, что мы считали известным, как именно выполняются те или иные команды, из которых состоит программа $$S$$.

Сейчас мы полностью изменим точку зрения. Будем считать первичным предикат $$wp$$ и условия, которым он удовлетворяет. Это позволит нам определить в терминах $$wp$$ все команды языка, а затем доказывать всевозможные утверждения о программах.

Первым оператором, который мы определим, будет пустой оператор.

Определение 6.6. $$wp(";", R) = R$$.

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

Определение 6.7. $$wp("System.exit(0);", R) = F$$.

Выполнение вызова метода " System.exit(0) " приводит к немедленному завершению выполнения программы. Поэтому вполне естественно, что ни при каком начальном состоянии после его выполнения предикат $$R$$ истинным не будет.

Следующее определение связано с последовательным выполнением двух операторов одного за другим.

Определение 6.8. $$wp("S1; S2;", R) = wp("S1;", wp("S2;", R))$$.

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

Более сложным и интересным является определение оператора присваивания, которое будет рассмотрено нами в двух вариантах. Сначала рассмотрим случай присваивания простой переменной.

Определение 6.9. $$wp("x = e;", R) = domain(e) \lands R^x_e$$, где $$domain(e)$$ — предикат, описывающий множество всех состояний, в которых может быть вычислено значение $$e$$ (т.е., где $$e$$ определено), а $$R^x_e$$ обозначает подстановку в предикат $$R$$ выражения $$e$$ вместо всех свободных вхождений переменной $$x$$.

Это определение может вызвать определенные вопросы, так как на первый взгляд кажется, что оно не соответствует нашему интуитивному пониманию того, что делает оператор присваивания. Поэтому рассмотрим ряд примеров, которые развеют эти сомнения.

$$wp("x = 5;", x=5) = (T \\ (5=5)) = T$$, что вполне правильно, так как присваивание переменной $$x$$ числа 5 всегда делает $$x=5$$.

$$wp("x = 5;", x\ne 5) = (T \\ (5\ne5)) = F$$, что тоже правильно, ибо присваивание переменной $$x$$ числа 5 никогда не может сделать $$x\ne5$$.

Часто можно позволить себе опустить предикат $$domain(e)$$ и считать, что $$wp("x = e;", R) = R^x_e$$, так как присваивание всегда должно выполняться только в тех ситуациях, когда $$e$$ может быть вычислено. В случае сомнений, однако, лучше воспользоваться исходным определением.

$$wp("x = 1/y;", x\leqslant0) = (y\ne0)\\(1/y\leqslant0) = (y<0)$$.

Случай присваивания элементу массива несколько сложнее, так как выражение $$b[i]$$ само по себе может оказаться неопределенным из-за некорректного значения индекса $$i$$. Введем предикат $$inrange(b,i)$$, который будет определять множество допустимых значений индекса.

Определение 6.10. Для присваивания элементу массива слабейшее предусловие $$wp("b[i] = e;", R) = inrange(b,i) \lands domain(e) \lands R^{b[i]}_e$$.

В качестве примера рассмотрим массив $$b[0..9]$$ и вычислим слабейшее предусловие $$wp("b[i] = i;", b[i] = i) = (inrange(b,i) \lands domain(i) \lands i = i) = ((0 \leqslant i < 10) \lands T \lands T) = (0 \leqslant i < 10)$$

Оператор if и слабейшее предусловие

Перед тем, как дать формальное определение оператора if-else в терминах $$wp$$, заметим, что управляющая конструкция if (без else части) эквивалентна использованию пустого оператора в else -ветви. Оператор switch также может быть заменен несколькими вложенными друг в друга операторами if-else. Таким образом, для того чтобы задать все основные конструкции выбора языка Java, достаточно дать определение только одной из них, — конструкции "if (e) S1; else S2;".

Определение 6.11.

$$wp("if (e) S1; else S2;", R) = domain(e)\lands\\ (e \Rightarrow wp("S1;",R))\land (!e \Rightarrow wp("S2;",R))$$

В качестве примера использования этого определения убедимся в том, что

$$wp("if (x >= y) z=x; else z=y;", z = max(x, y)) = T$$

В самом деле,

$$wp("if (x >= y) z=x; else z=y;", z = max(x, y)) = (((x \geqslant y) \Rightarrow \\ wp("z=x;", z = max(x, y))) \land !(x \geqslant y) \Rightarrow "z=y;", z = max(x, y)) =\\(((x \geqslant y) \Rightarrow (x = max(x, y))) \land !(x \geqslant y) \Rightarrow (y = max(x, y))) =\\ =((!(x \geqslant y) \lor (x = max(x, y))) \land !(!(x \geqslant y)) \lor (y = max(x, y))) =\\ =(((x < y) \lor (x = max(x, y))) \land (x \geqslant y) \lor (y = max(x, y)))$$

Покажем, что каждый из двух членов получившейся конъюнкции является тавтологией. Рассмотрим, например, первый из них — $$((x < y) \lor (x = max(x, y))$$. Если $$x<y$$, то истинен первый член дизъюнкции. В противном случае $$x\geqslant y$$ и поэтому истинен ее второй член, что и доказывает требуемое. Аналогичные рассуждения можно провести и для выражения $$(x \geqslant y) \lor (y = max(x, y)))$$, что и завершает доказательство.

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

Теорема 6.1.

Пусть предикат $$Q$$ удовлетворяет условию

$$((Q\land e)\Rightarrow wp(S1, R))\land ((Q\land !e)\Rightarrow wp(S2, R)).$$

Тогда (и только тогда)

$$Q\Rightarrow wp("if (e) S1; else S2;", R).$$

Доказательство

$$$((Q\land e)\Rightarrow wp(S1, R)) = (!(Q\land e)\lor wp(S1, R)) = (!Q\lor !e\lor wp(S1, R)) =\\= (!Q\lor (e\Rightarrow wp(S1, R))) = (Q\Rightarrow (e\Rightarrow wp(S1, R)))$$$

Аналогично получаем

$$((Q\land !e)\Rightarrow wp(S2, R)) = (Q\Rightarrow (!e\Rightarrow wp(S2, R))),$$

и, следовательно,

$$$(((Q\land e)\Rightarrow wp(S1, R))\land ((Q \land !e)\Rightarrow wp(S2, R))) = ((Q\Rightarrow (e\Rightarrow wp(S1, R)))\land (Q\Rightarrow (!e\Rightarrow wp(S2, R)))) = (Q\Rightarrow ((e\Rightarrow wp(S1, R))\land (!e\Rightarrow wp(S2, R)))) = (Q\Rightarrow wp(\Cmd{if (e) S1; else S2;}, R))$$$

Циклы в терминах wp

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

Для определения слабейшего предусловия $$wp("while(e)S;", R)$$ нам потребуются следующие вспомогательные определения:

Определение 6.12. $$H_0(R) = domain(e) \lands (!e \land R)$$, $$H_k(R) = H_{k-1}(R) \lor (domain(e) \lands wp(S, H_{k-1}(R)))$$, где предикат $$H_k(R)$$ описывает множество всех состояний, в которых выполнение цикла "while(e)S;" заканчивается не более, чем за $$k$$ итераций, в состоянии, удовлетворяющем $$R$$.

Теперь можно дать основное определение.

Определение 6.13. $$wp("while(e)S;", R) = (\exists k \geqslant 0 H_k(R))$$.

Для цикла "while (i<1) i=i+1;" и постусловия $$R=(i=1)$$ имеем $$H_0(R)= (i\geqslant1 \land i=1) = (i=1)$$. Действительно, именно при таком предусловии выполнение цикла завершится за ноль итераций и даст результат $$R$$.

Далее, легко посчитать $$wp("i=i+1;",H_0(R))= (i+1=1) = (i=0)$$ и $$H_1(R) = (i=1)\lor(i<1 \land i=0) = (i=1 \lor i=0)$$.

Аналогично находим $$H_2(R)= (i=1 \lor i=0 \lor i=-1)$$ и т.д.

Вычисление слабейшего предусловия

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

Задача 6.9. Вычислите и упростите $$wp("i=i+2; j=j-2;", i+j=0)$$.

Решение. Для вычисления воспользуемся определениями слабейшего предусловия для последовательного выполнения операторов и оператора присваивания. Так как в данном случае все выражения заведомо являются определенными, то истинный предикат $$domain(e)$$ будет опущен изначально.

$$wp("i=i+2; j=j-2;", i+j=0) = wp("i=i+2;", wp("j=j-2;", i+j=0)) = wp("i=i+2;", i+j-2=0) = (i+2+j-2=0) = (i=-j)$$.

Задача 6.10. Вычислите и упростите $$wp("x=(x+y)*(x-y);", x+y^2 \ne 0)$$.

Решение. $$wp("x=(x+y)*(x-y);", x+y^2 \ne 0) = ( x^2 -y^2 + y^2 \ne 0 ) = (x^2 \ne 0) = (x\ne0)$$.

Задача 6.11. Вычислите и упростите $$wp("x=a/b;", x^2 \geqslant 0)$$.

Решение. В данном случае ответ $$T$$ является ошибочным, так как $$wp("x=a/b;", x^2 \geqslant 0) = (domain(a/b) \lands {(a/b)}^2 \geqslant 0) = (b\ne 0)$$.

Задача 6.12. Вычислите и упростите $$wp("i=1; s=b[0];", 1 \leqslant i < n \ \land \ s = b[0]+\ldots+b[i-1] )$$.

Решение.

$$wp("i=1; s=b[0];", 1 \leqslant i < n \ \land \ s = b[0]+\ldots+b[i-1] ) =\\ wp("i=1;", wp("s=b[0];", 1 \leqslant i < n \ \land \ s = b[0]+\ldots+b[i-1])) = wp("i=1;", 1 \leqslant i < n \ \land \ b[0] = b[0]+\ldots+b[i-1]) = \\ ( 1 \leqslant 1 < n \land (b[0] = b[0])) = (1<n \land (b[0] = b[0])) = (n>1).$$

Задача 6.13. Вычислите и упростите $$wp("if(true);", R)$$ для произвольного предиката $$R$$.

Решение.

$$wp(\Cmd{if(true);}, R) = wp(\Cmd{if(true); else ;}, R) = \\ ((T \Rightarrow wp(\Cmd{;}, R)) \land (F \Rightarrow wp(\Cmd{;}, R))) = ((F \lor R) \land (T \lor R)) = (R \land T) = R$$

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

Задача 6.14. Найдите такое значение выражения $$x$$, включающее другие переменные, для которого спецификация $$\{Q\} \; S \; \{R\}$$ становится тавтологией: $$\{T\} \; "a=a+1; b=x;" \; \{b=a+1\}$$.

Решение. Вспомним, что имеет место эквивалентность $$\{Q\}\; S\; \{R\} = (Q \Rightarrow wp(S,R))$$. Таким образом, нам необходимо подобрать такое $$x$$, для которого $$(T \Rightarrow wp("a=a+1; b=x;", b=a+1)) = T$$. Вычислим сначала слабейшее предусловие, входящее в этот предикат:

$$wp(\Cmd{a=a+1; b=x;},b=a+1) = wp(\Cmd{a=a+1;}, wp(\Cmd{b=x;}, b=a+1)) = \\ wp(\Cmd{a=a+1;}, x=a+1) = (x = a+2).$$

Легко убедиться, однако, что мы получили неверный результат! И все дело в том, что переменная $$x$$ зависит от $$a$$. Проведем вычисления повторно, заменив $$x$$ на $$x(a)$$: $$wp("a=a+1; b=x(a);", b=a+1) = wp("a=a+1;", wp("b=x(a);", b=a+1)) = wp("a=a+1;", x(a)=a+1) = (x(a+1) = a+2)$$.

Вернемся к исходной задаче. Нам нужно выяснить, при каких значениях $$x$$ выражение $$(T \Rightarrow (x(a+1) = a+2)) = T$$ окажется тавтологией. Упростим данное выражение:

$$((T \Rightarrow (x(a+1)= a+2)) = T) = (T \Rightarrow (x(a+1) = a+2)) = \\ (F \lor (x(a+1) = a+2)) = (x(a+1)=a+2)$$

Теперь ответ очевиден: $$x(a)=a+1$$ или просто $$x=a+1$$.

Задачи для самостоятельного решения

Задача 6.15. Запишите предикат, утверждающий, что самое большее одно из следующих утверждений истинно: $$a<b$$, $$b<c$$.

Задача 6.16. Запишите предикат, утверждающий, что следующие утверждения не являются истинными одновременно: $$a<b$$, $$b<c$$ и $$x=y$$.

Задача 6.17. Запишите предикат, утверждающий следующее: когда $$x<y$$, $$y<z$$ означает, что $$v=w$$, но если $$x\geqslant y$$, то $$y<z$$ не может выполняться; однако если $$v=w$$, то $$x<y$$.

Задача 6.18. Запишите предикат, утверждающий, что для массива $$b[0..n-1]$$ длины $$n>0$$ все нули массива находятся в вырезке $$b[j..k]$$.

Задача 6.19. Запишите предикат, утверждающий, что для массива $$b[0..n-1]$$ длины $$n>0$$ некоторые нули массива находятся в вырезке $$b[j..k]$$.

Задача 6.20. Запишите предикат, утверждающий, что для массива $$b[0..n-1]$$ длины $$n>0$$ справедливо высказывание: неверно, что все нули массива находятся в вырезке $$b[j..k]$$.

Задача 6.21. Запишите предикат, утверждающий, что для массива $$b[0..n-1]$$ длины $$n>0$$ справедливо высказывание: неверно, что не все нули массива находятся в вырезке $$b[j..k]$$.

Задача 6.22. Запишите предикат, который утверждает, что функция $$f\colon \{1, 2, 3, 4, 5\} \rightarrow \{1, 2, 3, 4, 5\}$$ является инъективной и отрицание этого факта. Упростите получившиеся предикаты, если это возможно.

Задача 6.23. Запишите предикат, который утверждает, что функция $$f\colon \{1, 2, 3, 4, 5\} \rightarrow \{1, 2, 3, 4, 5\}$$ является биективной и отрицание этого факта. Упростите получившиеся предикаты, если это возможно.

Задача 6.24. Запишите предикат, который утверждает, что функция $$f\colon \{1, 2, 3, 4, 5\} \rightarrow \{1, 2, 3, 4, 5\}$$ все существует единственный элемент $$x \in \{1, 2, 3, 4, 5\}$$, который функция $$f$$ уменьшает, и отрицание этого факта. Не используйте при этом квантора $$\exists$$!.

Задача 6.25. Основываясь на определении 6.4 и спецификации программы 6.1, докажите истинность эквивалентности $$\{Q\}\; S\; \{R\} = (Q \Rightarrow wp(S,R))$$.

Задача 6.26. Основываясь на определении 6.4, докажите закон монотонности $$(Q \Rightarrow R) \Rightarrow (wp(S,Q) \Rightarrow wp(S,R))$$.

Задача 6.27. Основываясь на определении 6.4, докажите закон дистрибутивности дизъюнкции $$wp(S,Q) \lor wp(S,R) = wp(S, Q \lor R) $$.

Задача 6.28. Вычислите и упростите $$wp("i=i+1; j=j-1;", i\cdot j=0)$$.

Задача 6.29. Вычислите и упростите $$wp("x=x+y;", x < 2y)$$.

Задача 6.30. Вычислите и упростите $$wp("i=i+1; j=j+1;", i=j)$$.

Задача 6.31. Вычислите и упростите $$wp("a=0; n=1;", a^2 < n \ \land \ (a + 1)^2 \geqslant n)$$.

Задача 6.32. Вычислите и упростите $$wp("s=s+b[i]; i=i+1;", 0<i<n\ \land\ s=b[0]+\ldots+b[i-1])$$.

Задача 6.33. Вычислите и упростите следующее слабейшее предусловие $$wp("if (a > b) a=a-b; else b=b-a;",a>0 \ \land \ b > 0)$$.

Задача 6.34. Найдите такое значение выражения $$x$$, включающее другие переменные, для которого спецификация $$\{Q\} \; S \; \{R\}$$ становится тавтологией: $$\{T\} \; "b=x; a=a+1;" \; \{b=a+1\}$$.

Задача 6.35. Найдите такое значение выражения $$x$$, включающее другие переменные, для которого спецификация $$\{Q\} \; S \; \{R\}$$ становится тавтологией: $$\{i=j\} \; "i=i+1; j=x;" \; \{i=j\}$$.