Проектирование цикла при помощи инварианта

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

Условия правильности цикла

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

Теорема 8.1. Если

то спецификация программы $$\{Q\}\ "S0;while(e)S;"\ \{R\}$$ является тавтологией.

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

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

public class MulI {
    public static void main(String[] args) throws Exception {    
        int a = Xterm.inputInt("a -> ");
        int b = Xterm.inputInt("b -> ");
        int x = a, y = b, z = 0;
        while (y > 0) { 
            if ((y1) == 0) {
                y >>>= 1; x +=  x;
            } else {
                y  -=  1; z +=  x;
            }
        }
        Xterm.println("a * b = " + z);
    }
}

Докажем частично правильность еще одной построенной в предыдущем параграфе программы.

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

public class Gcd {
    public static void main(String[] args) throws Exception {
        int x = Xterm.inputInt("x -> ");
        int y = Xterm.inputInt("y -> ");
        Xterm.print("gcd(" + x + "," + y + ") =");
        while ( (x != 0)  (y != 0) ) {
            if (x >= y) x -= y;
            else        y -= x;
        } 
        Xterm.println(" " + (x+y));
    }
}

Если в качестве ограничивающей функции взять $$h=x\cdot y$$, то правильность полученной программы легко может быть доказана. Обозначим через $$x_0$$ и $$y_0$$ начальные значения переменных $$x$$ и $$y$$, удовлетворяющих предусловию $$Q=(x \in \mathbb{Z}_M^+\land y \in \mathbb{Z}_M^+\land (x,y) \ne (0,0))$$. Заметим также, что постусловие программы в целом может быть записано в виде предиката $$R1 =$$ ( напечатан $$gcd(x,y)$$ ), а постусловием цикла является предикат $$R=(x=0\lor y=0)$$.

Полученная дизъюнкция истинна, если ложно условие $$(x=0\lor y=0)$$. В противном случае один из аргументов функции $$gcd$$ равен нулю и по соответствующему свойству наименьшего общего делителя истинным является второй дизъюнктивный член, что завершает доказательство правильности программы.

Теория воздушного шарика

До сих пор мы использовали для построения программ готовые, не ясно откуда взявшиеся инварианты. На практике, конечно, постановка задачи не включает в себя инвариант. Однако любая корректная постановка задачи содержит ее пред- и постусловия: $$\{Q\}\ "S0;while(e)S;"\ \{R\}$$, поэтому они и должны послужить основой для построения инварианта.

Теперь нужно понять, какой именно из двух предикатов $$Q$$ и $$R$$ более важен для построения инварианта. Приведем два аргумента в пользу постусловия $$R$$.

Первый таков: предусловие $$Q$$ достаточно часто имеет вид $$T$$, что соответствует отсутствию ограничений на начальные условия, в которых должна правильно работать программа. Понятно, что в этом случае инвариант можно строить только исходя из постусловия $$R$$.

Второй аргумент: представим себе $$R$$ в виде цели, которой должен достичь путник на местности, а $$Q$$ в виде точки его начального расположения. Инвариант, который мы хотим построить, должен помочь путнику достичь нужной ему цели. Можно ли надеяться на это, полностью проигнорировав $$R$$?

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

Именно по этой причине программирование называют целенаправленной деятельностью, а за основу для построения инварианта берут постусловие $$R$$.

Рассмотрим геометрическую иллюстрацию стоящей перед нами задачи, изобразив на множестве $$X$$ всех значений программных переменных подмножества $$X_{S0}$$ и $$X_R$$, второе из которых задается постусловием $$R$$, а первое представляет собой множество, которое может быть получено из $$X_Q$$ после выполнения совокупности простых присваиваний S0. Искомому инварианту цикла $$I$$ на рисунке 8.1 должно соответствовать какое-то неизвестное нам пока множество $$X_I$$.

Существует весьма красивое описание того, что происходит с множеством переменных программы в процессе выполнения цикла, называемое теорией воздушного шарика. Рассмотрим последовательность предикатов $$P_0$$, $$P_1$$, $$\ldots$$, $$P_n$$, описывающих множества переменных до начала цикла, после его первой итерации, $$\ldots$$, после $$n$$ -ой (последней) итерации.

Множества, определяемые этими предикатами, представляют последовательность вложенных друг в друга множеств, причем $$X_{P_0} = X_I$$, а $$X_{P_n} = X_R$$. Удобно представлять себе эти множества как последовательные состояния изначально надутого воздушного шарика, из которого на каждой очередной итерации цикла выпускают немного воздуха.

Используя эту модель, можно сказать, что построение инварианта требует так надуть шарик, находящийся в состоянии $$X_R$$, чтобы он стал содержать множество $$X_{S0}$$. С математической точки зрения необходимо ослабить предикат $$R$$ до такой степени, чтобы истинность этого ослабленного предиката (который и будет взят в качестве инварианта $$I$$ ) могла быть получена из истинного $$Q$$ с помощью простых начальных присваиваний S0.

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

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

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

Устранение конъюнктивного члена

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

Рассмотрим в качестве примера следующую задачу.

Задача 8.1 Напишите программу, находящую приближенное значение квадратного корня $$a \in \mathbb{Z}_M^+$$ из заданного неотрицательного целого числа $$n$$. Вот более точная формулировка пред- и постусловия: $$Q=(n\in \mathbb{Z}_M \land n \geqslant 0)$$, $$R= (a \in \mathbb{Z}_M \land a \geqslant 0 \land a^2\leqslant n \land (a + 1)^2 > n)$$. При написании программы величину $$n$$ изменять нельзя.

Решение Построим инвариант с помощью метода устранения конъюнктивного члена $$(a + 1)^2 > n$$ из постусловия: $$I = (a \geqslant 0 \land a^2\leqslant n)$$. В качестве условия продолжения цикла e может быть взято отрицание удаленного конъюнктивного члена: $$e=( (a + 1)^2 \leqslant n)$$, что эквивалентно выбору ограничивающей функции $$h=n-(a + 1)^2+1$$. Истинность инварианта перед началом выполнения цикла легко устанавливается присваиванием "a=0;" и нам остается только понять, как реализовать тело цикла S.

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

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

public class Sqrt {
    public static void main(String[] args) throws Exception {
        int n = Xterm.inputInt("n -> ");
        int a = 0;
        while ( n >= (a+1)*(a+1) )
            a += 1;
        Xterm.println("sqrt(" + n + ") = " + a);
    }
}

Эту программу можно переписать в чуть более компактном виде:

Фрагмент программы

int a, n = Xterm.inputInt("n -> ");
        for (a=0; n >= (a+1)*(a+1); a++);
        Xterm.println("sqrt(" + n + ") = " + a);

Докажем все пять условий ее правильности.

Следовательно,$$(I\land e \Rightarrow wp("h1=h; S;", h<h1))= \\ (I\land e \Rightarrow T) = (!I \lor !e \lor T) = T.$$

Применим метод устранения конъюктивного члена для построения инварианта цикла при решении еще одной задачи.

Задача 8.2 Напишите программу (линейный поиск), определяющую первое вхождение заданного целого числа $$x$$ в заданный массив $$b[0..m-1]$$ целых чисел ( $$m>0$$ ). Известно, что $$x$$ находится в массиве $$b$$. Значения элементов массива $$b$$ и число $$x$$ в программе изменять нельзя.

Решение Выпишем формально заданные нам пред- и постусловия: $$Q = (0<m \land x \in b[0..m-1])$$, $$R = ((0 \leqslant i < m) \land (\forall j\ 0 \leqslant j < i\ x \ne b[j]) \land (x = b[i]))$$.

Так как добиться истинности третьего конъюнктивного члена одним или несколькими простыми присваиваниями трудно, устраним именно его. Тогда получим $$I=((0 \leqslant i < m) \land (\forall j\ 0 \leqslant j < i\ x \ne b[j]))$$. В качестве условия продолжения цикла можно взять отрицание удаленного члена ( $$e=(x \ne b[i])$$ ), а инвариант легко сделать истинным, выполняя команду "i=0;", поэтому программа должна иметь вид "i=0;while(x!=b[i])S;" с неизвестным нам пока S.

В качестве ограничивающей функции можно попробовать взять $$h=m-i$$, a для того, чтобы она уменьшалась, достаточно увеличивать $$i$$ на каждой итерации цикла. Понятно, что увеличивая $$i$$ более, чем на единицу, можно пропустить первое вхождение $$x$$ в массив, поэтому одной из команд, входящих в S, должна быть команда "i=i+1;". Так как выполнение данной команды при условии истинности $$e$$ сохраняет инвариант, то эта команда является единственной в теле цикла. Программа построена.

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

public class SearchL {
    static int b[], x;
    public static void main(String[] args) throws Exception {
        int m = Xterm.inputInt("m -> ");
        b = new int[m];  
        for (int k=0; k<m; k++)
            b[k] = Xterm.inputInt("b["+k+"] -> ");
        x = Xterm.inputInt("x -> ");
        int i=0;
        while (x != b[i])
            i += 1;
        Xterm.println("i = " + i);
    }
}

Докажем правильность этой программы.

Следовательно, $$(I\land e \Rightarrow wp("h1=h; S;", h<h1))= (I\land e \Rightarrow T) = (!I \lor !e \lor T) = T$$.

Замена константы переменной

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

Задача 8.3. Напишите программу, находящую сумму $$s$$ элементов заданного целочисленного массива $$b[0..n-1]$$, элементы которого и величину $$n$$ изменять нельзя. Точные пред- и постусловия: $$Q = (n>0)$$,$$\displaystyle R=\left(s = \sum_{j=0}^{n-1} b[j]\right).$$

Решение В постусловие входит константа $$n$$, которую мы можем заменить новой переменной $$i$$, меняющейся в диапазоне от $$0$$ до $$n$$ включительно. Таким образом, метод замены константы переменной приводит нас к инварианту$$\displaystyle I=\left(0\leqslant i \leqslant n \land \left(s = \sum_{j=0}^{i-1} b[j]\right)\right).$$ Понятно, что в качестве ограничивающей функции следует взять $$h=n-i$$.

Истинности инварианта легко добиться обнулением величин $$i$$ и $$s$$, поэтому искомая программа будет иметь вид "i=0;s=0;while(i<n)S;" с неизвестным нам пока телом цикла S.

Для того, чтобы цикл завершился, необходимо уменьшать $$h$$, что вполне естественно делать, увеличивая $$i$$ на единицу на каждой итерации цикла. Используя инвариант, находим, что вторым необходимым действием является добавление к $$s$$ значения $$b[i]$$:

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

public class SumArr {
    static int b[];
    public static void main(String[] args) throws Exception { 
        int n = Xterm.inputInt("n -> ");
        b = new int[n];  
        for (int k=0; k<n; k++)
            b[k] = Xterm.inputInt("b["+k+"] -> ");
        int i=0, s=0;
        while (i < n) {
            s += b[i]; 
            i += 1;
        }
        Xterm.println("s = " + s);
    }
}

Докажем ее правильность.

Следовательно, $$(I\land e \Rightarrow wp("h1=h; S;", h<h1))= (I\land e \Rightarrow T) = (!I \lor !e \lor T) = T$$.

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

Задача 8.4. Напишите программу, находящую приближенное значение квадратного корня $$a \in \mathbb{Z}_M^+$$ из заданного неотрицательного целого числа $$n$$. Точные пред- и постусловия требуемой программы, временная сложность которой не должна превосходить $$\Theta(\log n)$$, таковы: $$Q=(n\in \mathbb{Z}_M \land n \geqslant 0)$$, $$R= (a \in \mathbb{Z}_M \land a \geqslant 0 \land a^2\leqslant n \land (a + 1)^2 > n)$$. При написании программы величину $$n$$ изменять нельзя.

Решение Построим инвариант с помощью метода замены константы $$a+1$$ на переменную $$b$$. Из условия задачи вытекает, что $$a < b \leqslant n+1$$, следовательно инвариантом является предикат $$I=(a < b \leqslant n+1 \land a^2\leqslant n < b^2)$$. Условие продолжения цикла легко получается из того факта, что предикат $$(I \land !e \Rightarrow R)$$ должен быть тавтологией — $$e = (a+1\ne b)$$, а это означает использование ограничивающей функции $$h=b-a-1$$.

После присваиваний "a=0;b=n+1;" предикат $$I$$ становится истинным, следовательно наша программа имеет вид "a=0;b=n+1;while(a+1!=b)S;" с неизвестным пока телом цикла S.

Для того чтобы цикл завершился, необходимо уменьшать $$h$$, что эквивалентно сближению чисел $$a$$ и $$b$$. Уменьшение разности $$b-a$$ на единицу на каждой итерации цикла не позволит достичь требуемой в условии задачи эффективности программы. Нужная временная сложность может быть получена при использовании метода деления отрезка $$[a,b]$$ пополам на каждой итерации и выборе той из половинок, на которой лежит искомое приближенное значение квадратного корня. Реализация данной идеи приводит к следующей программе.

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

public class Sqrt3 {
    public static void main(String[] args) throws Exception {
        int a, b, n;
        n = Xterm.inputInt("n -> ");
        a = 0; 
        b = n+1;
        while (a+1 != b) {
            int c = (a+b)/2;
            if (c*c <= n) a = c;
            else          b = c;
        } 
        Xterm.println("sqrt(" + n + ") = " + a);
    }
}

Докажите самостоятельно ее правильность и оцените эффективность.

Расширение области значения переменной

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

В качестве примера разберем классическую задачу "Жулик на пособии". В оригинальном варианте рассматриваются три потенциально бесконечных упорядоченных по алфавиту списка фамилий — сотрудники исследовательского центра IBM, студенты Колумбийского университета и безработные Нью-Йорка. Требуется найти первую из фамилий, встречающуюся во всех трех списках (в предположении, что она есть).

Задача 8.5. Найдите минимальное число, содержащееся в каждом из трех упорядоченных по возрастанию массивов целых чисел, в предположении, что таковое существует.

Решение Пусть имеющиеся массивы — это $$a$$, $$b$$ и $$c$$. Переменные, содержащие значения индексов для каждого из этих массивов, обозначим через $$i$$, $$j$$ и $$k$$ соответственно, а индексы искомого числа в каждом из них — $$iv$$, $$jv$$ и $$kv$$.

Если не включать в предусловие информацию о том, что массивы являются упорядоченными (не забывая об этом, конечно), то пред- и постусловия искомой программы буду иметь вид $$Q=T$$, и $$R=((i=iv) \land (j=jv) \land (k=kv))$$.

Расширение области значений переменных $$i$$, $$j$$ и $$k$$ — естественный способ построения инварианта в данном случае: $$I= ((0\leqslant i \leqslant iv) \land (0\leqslant j \leqslant jv) \land (0\leqslant k \leqslant kv) )$$. В качестве ограничивающей функции можно взять $$h=iv-i+jv-j+kv-k$$, выбор начальных присваиваний S0 проблем тоже не вызывает — ясно, что операторы "i=0; j=0; k=0;" сделают инвариант истинным.

В качестве действий, которые будут приближать цикл к завершению можно использовать операторы "i++;", "j++;" и "k++;". При этом понятно, что каждый из них обязан присутствовать в итоговой программе.

Вычислим $$wp("i++;", I) = (i+1 \leqslant iv)$$. Это означает, что увеличение индекса $$i$$ в цикле нужно делать, когда $$i+1 \leqslant iv$$. К сожалению, записать подобное условие в программе невозможно, так как переменной $$iv$$ в ней просто может не быть!

Легко заметить, однако, что выполнение условия $$i+1 \leqslant iv$$ при истинном инварианте $$I$$ означает, что число $$a[i]$$ меньше искомого в задаче, а это может быть только при условии истинности дизъюнкции $$a[i] < b[j] \lor a[i] < c[k]$$. Аналогично заключаем, что если истинна дизъюнкция $$b[j] < a[i] \lor b[j] < c[k]$$, то можно увеличивать значение индекса $$j$$, а при истинности предиката $$c[k] < a[i] \lor c[k] < b[j]$$ — индекса $$k$$.

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

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

public class Arr3 {
    public static void main(String[] args){    
        int a[] = { 1, 2, 4, 8,16,32,64,128};
        int b[] = {10,12,14,16,18,20,22, 24};
        int c[] = { 9,12,13,16,17,20,21, 24};
        int i = 0, j = 0, k = 0;
        while (true) { 
            if (a[i] < b[j]) {
                i++; continue;
            }
            if (b[j] < c[k]) {
                j++; continue;
            }
            if (c[k] < a[i]) {
                k++; continue;
            }
            Xterm.println("Минимальное общее число=" + a[i]);
            return;
        }
    }
}

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

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

При решении задач необходимо построить и доказать правильность построенной программы вида "S0;while(e)S;", а при отсутствии в условии задачи явно заданных инварианта цикла и ограничивающей функции объяснить предварительно, каким образом они были получены.

Задача 8.6. Напишите программу, печатающую $$n$$ -ое число Фибоначчи ( $$f_0=0$$, $$f_1=1$$, $$f_k=f_{k-1}+f_{k-2} \ \mbox{для $k>1$}$$ ). При написании программы используйте $$Q=(n\in \mathbb{Z}_M \land n>0)$$, $$R=(a=f_n)$$, $$I=(1 \leqslant i \leqslant n \land a = f_i \land b = f_{i-1})$$, $$h=n-i$$. Число $$n$$ в программе изменять нельзя.

Задача 8.7. Напишите программу, находящую частное $$q$$ и остаток $$r$$ от деления $$x$$ на $$y$$, не использующую операций умножения и деления. При написании программы положите $$Q=(x\in \mathbb{Z}_M \land y\in \mathbb{Z}_M \land x\geqslant 0 \land y>0)$$, $$R=(0 \leqslant r < y \land q y + r = x)$$, $$I=(0 \leqslant r \land 0 < y \land q y + r = x)$$, $$h=r-y+1$$. Величины $$x$$ и $$y$$ в программе изменять не разрешается.

Задача 8.8. Напишите программу, находящую наибольший общий делитель $$gcd(X,Y)$$ двух целых положительных чисел $$X$$ и $$Y$$, не использующую операций умножения и деления и не изменяющую величин $$X$$ и $$Y$$. При написании программы положите $$Q=(X\in \mathbb{Z}_M \land Y\in \mathbb{Z}_M \land X>0 \land Y>0)$$, $$R=(x=y=gcd(X,Y))$$, $$I=(0<x \land 0<y \land gcd(x,y)=gcd(X,Y))$$, $$h=x+y-2\cdot gcd(x,y)$$.

Указание Воспользуйтесь следующими свойствами наибольшего общего делителя двух чисел не равных одновременно нулю (не забудьте научиться доказывать все эти свойства):$$gcd(x,y)=gcd(x,y-x)=gcd(x-y,y),$$ $$gcd(x,y)=gcd(x,y+x)=gcd(x+y,y),$$ $$gcd(x,x)=x,$$ $$gcd(x,y)=gcd(y,x)$$, $$gcd(x,0)=gcd(0,x)=x$$.

Задача 8.9. Напишите программу, находящую приближенное значение квадратного корня $$a \in \mathbb{Z}_M^+$$ из заданного неотрицательного целого числа $$n$$. Вот более точная формулировка пред- и постусловия: $$(Q=n\in \mathbb{Z}_M \land n \geqslant 0)$$, $$R= (a \in \mathbb{Z}_M \land a \geqslant 0 \land a^2\leqslant n \land (a + 1)^2 > n)$$. При написании программы величину $$n$$ изменять нельзя. Для построения инварианта удалите из постусловия конъюнктивный член $$a^2\leqslant n$$. Оцените временную сложность получившейся программы и сравните ее со сложностью программы, построенной в задаче 8.1.

Задача 8.10. Напишите программу, определяющую первое вхождение заданного целого числа $$x$$ в заданный массив массивов $$b[0..m-1][0..n-1]$$ целых чисел ( $$m>0, n>0$$ ). Значения элементов массива $$b$$ и числа $$x$$, $$m$$ и $$n$$ в программе изменять нельзя. В момент завершения должно быть либо $$b[i][j] = x$$, либо, если числа $$x$$ в массиве нет, $$i=m$$. Точные пред- и постусловия требуемой программы таковы: $$Q=(m>0 \land n>0)$$, $$R=((0\leqslant i <m \land 0 \leqslant j < n \land x = b[i][j])\lor (i=m \land x \notin b[0..m-1][0..n-1]))$$.

Указание Используйте инвариант, утверждающий, что $$x$$ не находится в уже проверенных строках $$b[0..i-1]$$ и среди уже проверенных элементов $$b[i][0..j-1]$$ текущей строки $$i$$. В качестве ограничивающей функции возьмите $$h=(m-i)\cdot n - j + m - i$$.

Задача 8.11. Напишите программу (бинарный или двоичный поиск), определяющую для упорядоченного по неубыванию массива $$b[0..n-1]$$ целых чисел и заданного целого числа $$x$$ позицию $$i$$, в которую может быть вставлено это число без нарушения упорядоченности массива. Точные пред- и постусловия требуемой программы, временная сложность которой не должна превосходить $$\Theta(\log n)$$, таковы: $$Q=(x\in \mathbb{Z}_M \land n\in \mathbb{Z}_M \land n >0 \land (\forall j\ 0 \leqslant j < n-1\colon b[j] \leqslant b[j+1]))$$, $$R=( (i=-1\land x < b[0])\lor (0\leqslant i < n-1\land b[i] \leqslant x < b[i+1])\lor (i=n\land b[n-1] \leqslant x) )$$. При написании программы величины $$x$$, $$n$$ и элементы массива $$b$$ изменять не разрешается, для построения инварианта используйте метод замены константы переменной.

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