МФСП, 08 лекция (от 22 октября)

Материал из eSyr's wiki.

(Различия между версиями)
Перейти к: навигация, поиск
 
(3 промежуточные версии не показаны)
Строка 1: Строка 1:
<!-- -x- --- x c overline -->
<!-- -x- --- x c overline -->
-
Мы рассм. метод фундированных множеств Флойда, который пот р. для док. заверш. программ. Также посм., как работать с небольшим расш. блок-схем, которые мы рассм, для работы с массивом.
+
Мы рассмотрим метод фундированных множеств Флойда, который потребуется для доказательства завершимости программ. Также посмотрим, как работать с небольшим расширением блок-схем, которые мы рассмотрим, для работы с массивом.
-
В след раз консультация. Потом коллоквиум.
+
В следующий раз консультация. Потом коллоквиум.
-
Фундированное множество. Что такое част. упор. мн-во, мы помним. Фундир. —- част упорядоченное, в котором не сущ. беск. упорядоченной посл.: (w, -<), в котором не сущ. беск. уб. посл.
+
Фундированное множество. Что такое частично упорядоченное множество, мы помним. Фундирование —- частично упорядоченное, в котором не существует бесконечно упорядоченной последовательности: (w, -<), в котором не существует бесконечно убывающей последовательности
Пример:
Пример:
Строка 21: Строка 21:
-
Шаг 1. Точка сечения. На этом же шаге ваыбир. индукт. утв. q_i(-x-, -y-), которые обычно совп. ..., которые выб. при метод. доказ. част. корректности
+
Шаг 1. Точка сечения. На этом же шаге выбирается индуктивное утверждение q_i(-x-, -y-), которые обычно совпадают с ..., которые выбираются при методе доказательства частично корректности
-
Шаг 2. Мы должгы выбрать оценочную функцию. Нам надо выбр. фундированное множество (w, -<), и для каждой точки сечения задать оценочную функцию u_i(-x-, -y-): D_-x- &times; D_-y- &rarr; w
+
Шаг 2. Мы должны выбрать оценочную функцию. Нам надо выбрать фундированное множество (w, -<), и для каждой точки сечения задать оценочную функцию u_i(-x-, -y-): D_-x- &times; D_-y- &rarr; w
-
Шаг 3. Условие завершимости. На котором для каждого промежуточного бащового пути должны выписать усл. завершимости, которое выглядмт следующим образом: &forall;-x-, &forall-y- q_i(-x-, -y-) &and; R_&alpha;(-x-, -y-) &rArr; (u_i(-x-, -y-) >- u_j(-x-, r_&alpha;(-x-, -y-))). Неформ. объясн: если в нач. точке сеч. выбр инвар. и поудйм по пути &alpha;, то когда приддём в конец, то оценочная функция даст на знач. строго меньшее, чем оценосчная функция в начале. Тем самым у нас уменьш. знач. функции, и, поск. мн-во фундированное, мы не сможем юеск. зодить по базовым путям и в конце уконцов выйдем на заверш. оператор.
+
Шаг 3. Условие завершимости. На котором для каждого промежуточного базового пути должны выписать условие завершимости, которое выглядит следующим образом: &forall;-x-, &forall;-y- q_i(-x-, -y-) &and; R_&alpha;(-x-, -y-) &rArr; (u_i(-x-, -y-) >- u_j(-x-, r_&alpha;(-x-, -y-))). Неформальное объяснение: если в начальной точке сечения выберем инварианты и пойдём по пути &alpha;, то когда придём в конец, то оценочная функция даст нам значение строго меньшее, чем оценочная функция в начале. Тем самым у нас уменьшится значение функции, и, поскольку множество фундированное, мы не сможем бесконечно ходить по базовым путям и в конце концов выйдем на завершающий оператор.
-
Можно заметить, что мы форм. условие только для промежуточных базовых путей.
+
Можно заметить, что мы формируем условие только для промежуточных базовых путей.
-
Какие есть ньюансы:
+
Какие есть нюансы:
-
# То, что при опр. оценочных функций и фунир. мн-ве неоюбх. показывать, что оценоч. функция опр. корректно. Что это значит: посм. на примере: у нас был инвар. определён следующего вида: q_i(-x-, -y-) = (x_1 = y_1 x_2 + y_2) &and; (y_2 &ge; 0) &and; (x_2 > 0). Оценоч. функцию, когда док., выбирали u_i(-x-, -y-) = y_2. При этом в кач-ве фундир. мн-ва мы выбирали просто мн-во нат. чисел. Когда лектор говорит о томм, что необх. показать корректность, то лектор говорит о том, что в каждой точке сечения там, где мы опр. u_i, у нас фактически вып. след. условие, условия корректности определения оценочной функции, уоторое говорит, что для любых x, y, для которых выполнен инвариант точки сечения, оценочсная функция действ. явл. значение, принадл. фундир. множеству: &forall; -x-, &forall; -y- q_i(-x-, -y-) &rArr; u_i(-x-, -y-) &isin; w. Соотв., когда опр. оцекноч. функцию, необх. также форм. усл. корректности опр. оценоч. функции, и именно это влечёт второй ньюанс, который состит в том, что
+
# То, что при определении оценочных функций и фундированных множеств необходимо показывать, что оценочная функция определена корректно. Что это значит: посмотрим на примере: у нас был инвариант определён следующего вида: q_i(-x-, -y-) = (x_1 = y_1 x_2 + y_2) &and; (y_2 &ge; 0) &and; (x_2 > 0). Оценочную функцию, когда доказывали, выбирали u_i(-x-, -y-) = y_2. При этом в качестве фундированного множества мы выбирали просто множество натуральных чисел. Когда говорится о том, что необходимо показать корректность, говорится о том, что в каждой точке сечения там, где мы определили u_i, у нас фактически выполняется следствие условие, условия корректности определения оценочной функции, которое говорит, что для любых x, y, для которых выполнен инвариант точки сечения, оценочная функция действ. явл. значение, принадлежащее фундированному множеству: &forall; -x-, &forall; -y- q_i(-x-, -y-) &rArr; u_i(-x-, -y-) &isin; w. Соответственно, когда определяют оценочную. функцию, необходимо также формировать условие корректности определения оценочной функции, и именно это влечёт второй нюанс, который состоит в том, что
-
# Жти инвар. q_i иногда отл. от инвар., исп. в методе док. част. корректности, потому, что там необх. добавить какой-то коньюнкт о том,Ю что какая-то переменная больше нуля. А это озн., то, что если q_i у нас отл. от того, что исп. на пред. шаге, то нам необх. вып. все усл. вериф., которые выпис. на осн .... . Поэтому лучше модиф. доказ., чтобы два разане выпис очень похожие условия.
+
# Эти инвар. q_i иногда отличаются от инвариантов, используемых в методе доказательства частичной корректности, потому, что там необходимо добавить какой-то коньюнкт о том, что какая-то переменная больше нуля. А это означает, то, что если q_i у нас отличается от того, что используется на предыдущем шаге, то нам необходимо выписать все условия верификации, которые выписывали на осн .... . Поэтому лучше модифицировать доказательство, чтобы два раза не выписывать очень похожие условия.
-
Опять же, существует теорема, которая утв. корректность этого метода:
+
Опять же, существует теорема, которая утверждает корректность этого метода:
-
Теорема. Если у нас выбр. программа P и некий входной предикат &phi;, то после вып. всех трёх шагов метода, у нас будет следовать завершимость программы, заданной своей блок-схемой, на входном предикате &phi;.
+
'''Теорема'''. Если у нас выбрана программа P и некий входной предикат &phi;, то после выполнения всех трёх шагов метода, у нас будет следовать завершимость программы, заданной своей блок-схемой, на входном предикате &phi;.
-
Если мыпосмотрим то, что у нас происзодит с прим. жтого метиода к нашему примеру с целочисл. делением, то происз.ж то же самое, что и на пред. олекции, когда док. заверш. схеми без исп. метода фунд. множеств., а именно:
+
Если мы посмотрим то, что у нас происходит с применением этого метода к нашему примеру с целочисленным делением, то происходит то же самое, что и на предыдущей лекции, когда доказательства завершались схеми без использования метода фундированных множеств, а именно:
-
Выбир точку, выбир индуктивное утв. q_i, затем выбир. фунд. мн-во, совп. с мн-вом нат. числе, опред. точки и записываем усл. корректности этой точки сечения, оно выгл. дост. очевидно, поск. в индукт. утв. есть y_2 &ge; 0, поэтому принадл. мн-ва зн. функции очевидно. После этого .... прохождение по циклу из точки сечения i в точку сечения i выгл. очевидно:
+
Выбираем точку, выбираем индуктивное утверждение q_i, затем выбираем фундированное множество, совпадающее с множеством натуральных чисел, определяющих точки и записываем условие корректности этой точки сечения, оно выглядит достаточно очевидно, поскольку в индуктивном утверждении есть y_2 &ge; 0, поэтому принадлежность множества значений функции очевидно. После этого .... прохождение по циклу из точки сечения i в точку сечения i выглядит очевидно:
-
i-i: &forall; -x- &forall; -y- (x_1 = y_1 x_2 + y_2) &and; (y_2 &ge; 0) &and (x_2 > 0) &and; (y_2 &ge; x_2) &rArr; y_2 > y_2 - x_2
+
i-i: &forall; -x- &forall; -y- (x_1 = y_1 x_2 + y_2) &and; (y_2 &ge; 0) &and; (x_2 > 0) &and; (y_2 &ge; x_2) &rArr; y_2 > y_2 - x_2
-
Несложно видеть, что данное усл. завершимости явл. корректным, поск. (x_2 > 0) &and; (y_2 &ge; x_2), и из этого следует y_2 > y_2 - x_2.
+
Несложно видеть, что данное условие завершимости является корректным, поскольку (x_2 > 0) &and; (y_2 &ge; x_2), и из этого следует y_2 > y_2 - x_2.
-
Двинемся дальше.
+
Мы с помощью метода индуктивных утверждений доказали частичную корректность программы ({&phi;} P {&psi;}), с помощью метода фундированных множеств доказали завершимость (<&phi;> P <T>) , из этого след. полная корректность относительно спецификации, заданной предикатами &phi; и &psi;: <&phi;> P <&psi;>
-
Мы с помощбю метода индукт. утв. доказали част. корр. программы ({&phi;} P {&psi;}), с помощью метода фунд. мн-в доказали завершимость (<&phi;> P <T>) , из этого след. полная корр. отн. спец., заданной предикатами &phi; и &psi;: <&phi;> P <&psi;>
+
Далее введём определение эквивалентности программ относительно предиката &phi;, задающего область ... значений программ. Прежде всего, программы P_1, P_2 характеризуются 3 доменами: D^1_-x-, D^1_-y-, D^1_-z- (домены входных, промежуточных, выходных переменных), аналогичные домены есть у второй программы. Программы сравнимы, если у них совпадают домены входных и выходных данных.
-
Далее введём опр. эквивалентности программ относительно предиката &phi;, задающего обл. ... значений программ. Прежде всего, программы P_1, P_2 характеризуются 3 доменами: D^1_-x-, D^1_-y-, D^1_-z- (домены входных, промежуточных, выходных перем), аналогичные домены есть у второй программы. Программы сравнимы., если у них совп. домены входных и выходных данных.
+
'''Опр'''. P_1 сравнима с P_2, если D^1_-x- = D^2_-x-, D^1_-z- = D^2_-z-
-
Опр. P_1 сравнима с P_2, если D^1_-x- = D^2_-x-, D^1_-z- = D^2_-z-
+
Соответственно, P_1 ~ P_2 относительно &phi;: D^1_-x- &rarr; {T, 1}, если для &forall; -x- &isin; D_-x- при условии, что выполнен предикат &phi;(-x-) &rArr; вычисления совпадают: M[P_1](-x-) = M[P_2](-x-). M[P] возвращают либо значение из выходного домена, либо &omega;, если вычисление не завершается.
-
 
+
-
Соответственно, P_1 ~ P_2 относитлеьно &phi;: D^1_-x- &rarr; {T, 1}, если для &forall; -x- &isin; D_-x- при условии, что вып предикат &phi;(-x-) &rArr; вычисления совпадают: M[P_1](-x-) = M[P_2](-x-). M[P] возвр. либо знач. из вых домена, либо &omega;, если выч. не завершается.
+
Рассмотрение программ с массивами.
Рассмотрение программ с массивами.
-
Если мы попробуем добавить в наши сущ. методы вериф. работу с массивами, то в блок-схемах факт. появляется некий новый тип переменных, наз. массивы неокотрой фик. размерности, которые могут участвовать во всех выр., опр. функци, припис. к усл. опер., опер. присваивания, нач., заверш. оператору... Собственно говоря, можно считать, сильно нового ничего не появляется. Наиболее интересный аспект получается связан с необх контролировать невыход за границы массива при индекс его эементами. Если у нас где-то встр. выражение x[i+j], а x — массив целых числер разм. 10, то для док. корр. программы необх. будет показывать, что в этом выр. i+j лежит в диапазоне между 0 и 10, то есть, явл. корр. индексом, чтобы программа вып. также корректно.
+
Если мы попробуем добавить в наши существующие методы верификации работу с массивами, то в блок-схемах фактически появляется некий новый тип переменных, называемый массивы некоторой фиксированной размерности, которые могут участвовать во всех выражениях, определениях функций, припис. к условным операторам, операторам присваивания, начальному, завершающему оператору. Собственно говоря, можно считать, сильно нового ничего не появляется. Наиболее интересный аспект получается связан с необходимостью контролировать невыход за границы массива при индекс его элементами. Если у нас где-то встретилось выражение x[i+j], а x — массив целых чисел размерности 10, то для доказательства корректности программы необходимо будет показывать, что в этом выражении i+j лежит в диапазоне между 0 и 10, то есть, является корректным индексом, чтобы программа выполнялась также корректно.
-
 
+
-
Соответственно, сейчас надо опр., как появл. данное изм. на соотв. шаги метода Флойда.
+
-
<!-- педедыв -->
+
Соответственно, сейчас надо определить, как появляется данное изменение на соответствующих шагах метода Флойда.
-
Cajhv/ vjlba/ vtnjlf Akjqlf? rjnjhst gjnh/ lkz hf,jns c vfccbdjv/ Gthtl 'nbv лектор хотел бы сказать, что товарищ МакКарти можно задать как две операции и аксиомы работы с ними:
+
Формальные модификации метода Флойда, которые порт. для работы с массивом можно задать как две операции и аксиомы работы с ними:
* x: Nat[N]
* x: Nat[N]
* c(x,i): Nat[N] &times; [x, N-1] &rarr; Nat
* c(x,i): Nat[N] &times; [x, N-1] &rarr; Nat
* a(x, i_1, n_1, ..., i_n, n_k): Nat[N](&times;[0,N-1]&times;Nat)^{1..N} &rarr; Nat[N]
* a(x, i_1, n_1, ..., i_n, n_k): Nat[N](&times;[0,N-1]&times;Nat)^{1..N} &rarr; Nat[N]
-
Этих опер. дост. Аксиомы, соотв., такие:
+
для этих операций достаточны аксиомы:
* &forall;x &forall;i &isin; [0, N-1] (i_1 &ne; i) &and; ... (i_k &ne; i) &rArr; c(a(x, i_1, n_1, ..., i_k, n_k), i) = c(x_i, i)
* &forall;x &forall;i &isin; [0, N-1] (i_1 &ne; i) &and; ... (i_k &ne; i) &rArr; c(a(x, i_1, n_1, ..., i_k, n_k), i) = c(x_i, i)
* &forall; x &forall; i (i=i_j) &rArr; c(a(x, i_1, n_1, ..., i_k, n_k), i) = n_j
* &forall; x &forall; i (i=i_j) &rArr; c(a(x, i_1, n_1, ..., i_k, n_k), i) = n_j
-
Для метода инд. утверждение у нас ост. всё то же самое:
+
Для метода индуктивных утверждений у нас осталось всё то же самое:
* Ш1.
* Ш1.
* Ш2.
* Ш2.
-
* Ш3. Добавл. усл. корр., связанное с невыходом за гр. массива. Усл. корр. опр. для всех операторов всех видов, кроме join. Для всех операторов, в которых встреччается инд. некоего массива: x[y], необх. &forall; путей, нач. во всех точках сечения i и зак. в операторе n (i-n), на котором нет других точек сечения, необх. сформ. усл. корректности: &forall; -x- &forall -y- p_i(-x-, -y-) &and; R_&alpha;(-x-, -y-) &rArr; 0 &le; y < N. Если говорить более форм., то в качестве инд. исп. f(-x-, -y-), соотв., если писать форм., то надо писать f(-x-, r_&alpha;(-y-)). Соответственно, аналогично требование для путей, которые нач. в начальном операторе: в любом опер., в котором есть разым., в любом путе, в котором есть нач. оператор, и которое не сод. точек сечения, будет аналог. сформ. выражение: &forall; -x- &phi;(-x-) &and; R'_&alpha;(-x-) &rArr; 0 &le; f('x', r_&alpha;(-x-)) < N
+
* Ш3. Добавляем условие корректности, связанное с невыходом за границы массива. Условие корректности определяется для всех операторов всех видов, кроме join. Для всех операторов, в которых встречается индекс некоего массива: x[y], необходимо &forall; путей, начинающихся во всех точках сечения i и заканчивающихся в операторе n (i-n), на котором нет других точек сечения, необходимо сформулировать условие корректности: &forall; -x- &forall -y- p_i(-x-, -y-) &and; R_&alpha;(-x-, -y-) &rArr; 0 &le; y < N. Если говорить более формально, то в качестве индекса используется f(-x-, -y-), соответственно, если писать формально, то надо писать f(-x-, r_&alpha;(-y-)). Соответственно, аналогично требование для путей, которые начинаются в начальном операторе: в любом операторе, в котором есть разыменование, в любом пути, в котором есть начальный оператор, и который не содержит точек сечения, будет аналог. сформируем выражение: &forall; -x- &phi;(-x-) &and; R'_&alpha;(-x-) &rArr; 0 &le; f('x', r_&alpha;(-x-)) < N
-
При док. завершимости программа, на самом деле, просто полезно иметь в виду, что у нас есть зорошее св-во фунд. мн-в: если у нас их есть неск., то дек. произв. с заданным на нём лекс. порядко есть фунд. множество. Именно этим способом орг. фунд. множество оказ удобно польз.ю при работе с массивами.
+
При доказательстве завершимости программы, на самом деле, просто полезно иметь в виду, что у нас есть хорошее свойство фундированных множеств: если у нас их есть несколько, то декартово произведение с заданным на нём лексикографическом порядке есть фундированное множество. Именно этим способом организуется фундированное множество оказывается удобно использовать при работе с массивами.
-
В касестве примера рассм. программу, которая выч. реверсирование массива.
+
В качестве примера рассмотрим программу, которая вычисляет реверсирование массива.
-
Допустьим, есть вх. массив x: N[10]. Есть промеж. переменные y : N[10], i : N. Домен вых. переменных: z : N[10].
+
Допустим, есть входной массив x: N[10]. Есть промежуточные переменные y : N[10], i : N. Домен выходных переменных: z : N[10].
-
Вообще, это делается в одно присв.. Но мы простым путём не пойдём и нарис. программу с циклом:
+
Вообще, это делается в одно присваивание. Но мы простым путём не пойдём и нарисуем программу с циклом:
START:
START:
Строка 96: Строка 92:
(y[0-i, y[i]], i+1) z &larr; y
(y[0-i, y[i]], i+1) z &larr; y
-
Теперь необх. сформю спецификацию:
+
Теперь необходимо сформулировать спецификацию:
* Предусловие: &phi; &equiv; true
* Предусловие: &phi; &equiv; true
* Постусловие: &psi; &equiv; &forall; i &isin; {0..9}: z[i] = x[9-i]
* Постусловие: &psi; &equiv; &forall; i &isin; {0..9}: z[i] = x[9-i]
Строка 102: Строка 98:
Ш1. Выберем точку сечения: i.
Ш1. Выберем точку сечения: i.
-
Ш2. На втором шаге необх. сформ. инд. утверждение: &forall; j &isin; N: 0 &le; j &le; i &rArr; (y[j]=x[9-j])&and;(y[9-j]=x[j])
+
Ш2. На втором шаге необходимо сформулировать индуктивное утверждение: &forall; j &isin; N: 0 &le; j &le; i &rArr; (y[j]=x[9-j])&and;(y[9-j]=x[j])
-
Ш3. Необх. сформ. усл. вериф. для всех базовых путей. &forall; x &forall; j &isin; N 0 &le; j &le; 0 &rarr; x[j] = x[9-j] &and; x[9-j]=x[j]. Условие зап. корр., но оно не явл. истиной. То есть инв., который мы выбрали, явл. не совсем корр., поск на 1 проходе он не вып. Соотв., нам надо подкорр. эжтот инв., чтобы он действ. описывал точку сечения, или передвинуть точку сечения. Но лектор предл. подпр. инв. На самом деле, 0 &le; j '''<''' i. Соотв., теперь, кода мы модиф. инвариант, левая часть импл. становится ложью и импл. становится истиной. Посмотрим на след. базовый путь. Рассм.п базовы йпуть, который нач. с т. с., проходит итерацию цикла и в неё возвр.: &forall; x &forall; y &forall; i: (&forall;j &isin; N, 0 &le; j < i &rArr; y[j] = x[9-j] &and; y[9-j]=x[j]) &and; i < 5 &rarr; (&forall; j &isin; N 0 &le; j < i+1 &rArr; y'[j] = x[9-j] &and; y'[9-j]=x[j]), y' = a(y, i, y[9-i], 9-i, y[i]). Это не есть тожд. истина. В данном случае, когда мы пис. инв., мы бкзусл .написали, что для частиЮ, которую мы прошли, перест. произошла, но мы забыли важный момент: конец массива сод. неизм. массив x. Именно это знание и необх. отразить. Необх. написать, что для i <= j < 9-i y[j]=x[j]. Тогда слева появится конъюнкция и это тогда действ. будет тожд. истина.
+
Ш3. Необходимо сформулировать условия верификации для всех базовых путей. &forall; x &forall; j &isin; N 0 &le; j &le; 0 &rarr; x[j] = x[9-j] &and; x[9-j]=x[j]. Условие записано корректно, но оно не является истиной. То есть инвариант, который мы выбрали, является не совсем корректным, поскольку на 1 проходе он не выполняется. Соответственно, нам надо подкорректировать этот инвариант, чтобы он действительно описывал точку сечения, или передвинуть точку сечения. Но было предложено подправить инвариант. На самом деле, 0 &le; j '''<''' i. Соответственно, теперь, кода мы модифицируем инвариант, левая часть импликации становится ложью и импликация становится истиной. Посмотрим на следующий базовый путь. Рассмотрим базовый путь, который начинается с т. с., проходит итерацию цикла и в неё возвращается: &forall; x &forall; y &forall; i: (&forall;j &isin; N, 0 &le; j < i &rArr; y[j] = x[9-j] &and; y[9-j]=x[j]) &and; i < 5 &rarr; (&forall; j &isin; N 0 &le; j < i+1 &rArr; y'[j] = x[9-j] &and; y'[9-j]=x[j]), y' = a(y, i, y[9-i], 9-i, y[i]). Это не есть тождественная истина. В данном случае, когда мы писали инвариант, мы безусловно написали, что для части, которую мы прошли, перестановка произошла, но мы забыли важный момент: конец массива содержит неизменённый массив x. Именно это знание и необходимо отразить. Необходимо написать, что для i <= j < 9-i y[j]=x[j]. Тогда слева появится конъюнкция и это тогда действительно будет тождественная истина.
-
Тем самым лектор зотел проилл. момент, что когда пишете инв., не забывайте вносить вещи, которые как бы очевидны. Это же отн. к огр. на обл. значений перем.
+
Когда пишете инварианты, не забывайте вносить вещи, которые как бы очевидны. Это же относится к ограничениям на область значений переменных.
Ссылки:
Ссылки:

Текущая версия


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

В следующий раз консультация. Потом коллоквиум.

Фундированное множество. Что такое частично упорядоченное множество, мы помним. Фундирование —- частично упорядоченное, в котором не существует бесконечно упорядоченной последовательности: (w, -<), в котором не существует бесконечно убывающей последовательности

Пример:

+----------------------------------------+
| START:                                 |
| (y_1, y_2) ← (0_λ, x_1)    |
+----------------------------------------+
               |                    
+----------->  Vi---------------------------+ F
|          (----------------)               |
|   +------(  y_2 ≥ x_2  )               HALT:
|   |      (----------------)               (z_1, z_2) ← (y_1, y_2)
|   V
+-(y_1, y_2) ← (y_1+1, y_2-x_2)


Шаг 1. Точка сечения. На этом же шаге выбирается индуктивное утверждение q_i(-x-, -y-), которые обычно совпадают с ..., которые выбираются при методе доказательства частично корректности

Шаг 2. Мы должны выбрать оценочную функцию. Нам надо выбрать фундированное множество (w, -<), и для каждой точки сечения задать оценочную функцию u_i(-x-, -y-): D_-x- × D_-y- → w

Шаг 3. Условие завершимости. На котором для каждого промежуточного базового пути должны выписать условие завершимости, которое выглядит следующим образом: ∀-x-, ∀-y- q_i(-x-, -y-) ∧ R_α(-x-, -y-) ⇒ (u_i(-x-, -y-) >- u_j(-x-, r_α(-x-, -y-))). Неформальное объяснение: если в начальной точке сечения выберем инварианты и пойдём по пути α, то когда придём в конец, то оценочная функция даст нам значение строго меньшее, чем оценочная функция в начале. Тем самым у нас уменьшится значение функции, и, поскольку множество фундированное, мы не сможем бесконечно ходить по базовым путям и в конце концов выйдем на завершающий оператор.

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

Какие есть нюансы:

  1. То, что при определении оценочных функций и фундированных множеств необходимо показывать, что оценочная функция определена корректно. Что это значит: посмотрим на примере: у нас был инвариант определён следующего вида: q_i(-x-, -y-) = (x_1 = y_1 x_2 + y_2) ∧ (y_2 ≥ 0) ∧ (x_2 > 0). Оценочную функцию, когда доказывали, выбирали u_i(-x-, -y-) = y_2. При этом в качестве фундированного множества мы выбирали просто множество натуральных чисел. Когда говорится о том, что необходимо показать корректность, говорится о том, что в каждой точке сечения там, где мы определили u_i, у нас фактически выполняется следствие условие, условия корректности определения оценочной функции, которое говорит, что для любых x, y, для которых выполнен инвариант точки сечения, оценочная функция действ. явл. значение, принадлежащее фундированному множеству: ∀ -x-, ∀ -y- q_i(-x-, -y-) ⇒ u_i(-x-, -y-) ∈ w. Соответственно, когда определяют оценочную. функцию, необходимо также формировать условие корректности определения оценочной функции, и именно это влечёт второй нюанс, который состоит в том, что
  2. Эти инвар. q_i иногда отличаются от инвариантов, используемых в методе доказательства частичной корректности, потому, что там необходимо добавить какой-то коньюнкт о том, что какая-то переменная больше нуля. А это означает, то, что если q_i у нас отличается от того, что используется на предыдущем шаге, то нам необходимо выписать все условия верификации, которые выписывали на осн .... . Поэтому лучше модифицировать доказательство, чтобы два раза не выписывать очень похожие условия.

Опять же, существует теорема, которая утверждает корректность этого метода:

Теорема. Если у нас выбрана программа P и некий входной предикат φ, то после выполнения всех трёх шагов метода, у нас будет следовать завершимость программы, заданной своей блок-схемой, на входном предикате φ.

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

Выбираем точку, выбираем индуктивное утверждение q_i, затем выбираем фундированное множество, совпадающее с множеством натуральных чисел, определяющих точки и записываем условие корректности этой точки сечения, оно выглядит достаточно очевидно, поскольку в индуктивном утверждении есть y_2 ≥ 0, поэтому принадлежность множества значений функции очевидно. После этого .... прохождение по циклу из точки сечения i в точку сечения i выглядит очевидно:

i-i: ∀ -x- ∀ -y- (x_1 = y_1 x_2 + y_2) ∧ (y_2 ≥ 0) ∧ (x_2 > 0) ∧ (y_2 ≥ x_2) ⇒ y_2 > y_2 - x_2

Несложно видеть, что данное условие завершимости является корректным, поскольку (x_2 > 0) ∧ (y_2 ≥ x_2), и из этого следует y_2 > y_2 - x_2.

Мы с помощью метода индуктивных утверждений доказали частичную корректность программы ({φ} P {ψ}), с помощью метода фундированных множеств доказали завершимость (<φ> P <T>) , из этого след. полная корректность относительно спецификации, заданной предикатами φ и ψ: <φ> P <ψ>

Далее введём определение эквивалентности программ относительно предиката φ, задающего область ... значений программ. Прежде всего, программы P_1, P_2 характеризуются 3 доменами: D^1_-x-, D^1_-y-, D^1_-z- (домены входных, промежуточных, выходных переменных), аналогичные домены есть у второй программы. Программы сравнимы, если у них совпадают домены входных и выходных данных.

Опр. P_1 сравнима с P_2, если D^1_-x- = D^2_-x-, D^1_-z- = D^2_-z-

Соответственно, P_1 ~ P_2 относительно φ: D^1_-x- → {T, 1}, если для ∀ -x- ∈ D_-x- при условии, что выполнен предикат φ(-x-) ⇒ вычисления совпадают: M[P_1](-x-) = M[P_2](-x-). M[P] возвращают либо значение из выходного домена, либо ω, если вычисление не завершается.

Рассмотрение программ с массивами.

Если мы попробуем добавить в наши существующие методы верификации работу с массивами, то в блок-схемах фактически появляется некий новый тип переменных, называемый массивы некоторой фиксированной размерности, которые могут участвовать во всех выражениях, определениях функций, припис. к условным операторам, операторам присваивания, начальному, завершающему оператору. Собственно говоря, можно считать, сильно нового ничего не появляется. Наиболее интересный аспект получается связан с необходимостью контролировать невыход за границы массива при индекс его элементами. Если у нас где-то встретилось выражение x[i+j], а x — массив целых чисел размерности 10, то для доказательства корректности программы необходимо будет показывать, что в этом выражении i+j лежит в диапазоне между 0 и 10, то есть, является корректным индексом, чтобы программа выполнялась также корректно.

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

Формальные модификации метода Флойда, которые порт. для работы с массивом можно задать как две операции и аксиомы работы с ними:

  • x: Nat[N]
  • c(x,i): Nat[N] × [x, N-1] → Nat
  • a(x, i_1, n_1, ..., i_n, n_k): Nat[N](×[0,N-1]×Nat)^{1..N} → Nat[N]

для этих операций достаточны аксиомы:

  • ∀x ∀i ∈ [0, N-1] (i_1 ≠ i) ∧ ... (i_k ≠ i) ⇒ c(a(x, i_1, n_1, ..., i_k, n_k), i) = c(x_i, i)
  • ∀ x ∀ i (i=i_j) ⇒ c(a(x, i_1, n_1, ..., i_k, n_k), i) = n_j

Для метода индуктивных утверждений у нас осталось всё то же самое:

  • Ш1.
  • Ш2.
  • Ш3. Добавляем условие корректности, связанное с невыходом за границы массива. Условие корректности определяется для всех операторов всех видов, кроме join. Для всех операторов, в которых встречается индекс некоего массива: x[y], необходимо ∀ путей, начинающихся во всех точках сечения i и заканчивающихся в операторе n (i-n), на котором нет других точек сечения, необходимо сформулировать условие корректности: ∀ -x- &forall -y- p_i(-x-, -y-) ∧ R_α(-x-, -y-) ⇒ 0 ≤ y < N. Если говорить более формально, то в качестве индекса используется f(-x-, -y-), соответственно, если писать формально, то надо писать f(-x-, r_α(-y-)). Соответственно, аналогично требование для путей, которые начинаются в начальном операторе: в любом операторе, в котором есть разыменование, в любом пути, в котором есть начальный оператор, и который не содержит точек сечения, будет аналог. сформируем выражение: ∀ -x- φ(-x-) ∧ R'_α(-x-) ⇒ 0 ≤ f('x', r_α(-x-)) < N

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

В качестве примера рассмотрим программу, которая вычисляет реверсирование массива.

Допустим, есть входной массив x: N[10]. Есть промежуточные переменные y : N[10], i : N. Домен выходных переменных: z : N[10]. Вообще, это делается в одно присваивание. Но мы простым путём не пойдём и нарисуем программу с циклом:

START:
(y, i) ← (x, 0)
       |<---+
       |-i  |
  T    V    |    F
+-----i<5 -------------------+
|           |                 |
|           |                 |
V           |                 V
(y[i], y[9-i], i) ←    HALT:
(y[0-i, y[i]], i+1)         z ← y

Теперь необходимо сформулировать спецификацию:

  • Предусловие: φ ≡ true
  • Постусловие: ψ ≡ ∀ i ∈ {0..9}: z[i] = x[9-i]

Ш1. Выберем точку сечения: i.

Ш2. На втором шаге необходимо сформулировать индуктивное утверждение: ∀ j ∈ N: 0 ≤ j ≤ i ⇒ (y[j]=x[9-j])∧(y[9-j]=x[j])

Ш3. Необходимо сформулировать условия верификации для всех базовых путей. ∀ x ∀ j ∈ N 0 ≤ j ≤ 0 → x[j] = x[9-j] ∧ x[9-j]=x[j]. Условие записано корректно, но оно не является истиной. То есть инвариант, который мы выбрали, является не совсем корректным, поскольку на 1 проходе он не выполняется. Соответственно, нам надо подкорректировать этот инвариант, чтобы он действительно описывал точку сечения, или передвинуть точку сечения. Но было предложено подправить инвариант. На самом деле, 0 ≤ j < i. Соответственно, теперь, кода мы модифицируем инвариант, левая часть импликации становится ложью и импликация становится истиной. Посмотрим на следующий базовый путь. Рассмотрим базовый путь, который начинается с т. с., проходит итерацию цикла и в неё возвращается: ∀ x ∀ y ∀ i: (∀j ∈ N, 0 ≤ j < i ⇒ y[j] = x[9-j] ∧ y[9-j]=x[j]) ∧ i < 5 → (∀ j ∈ N 0 ≤ j < i+1 ⇒ y'[j] = x[9-j] ∧ y'[9-j]=x[j]), y' = a(y, i, y[9-i], 9-i, y[i]). Это не есть тождественная истина. В данном случае, когда мы писали инвариант, мы безусловно написали, что для части, которую мы прошли, перестановка произошла, но мы забыли важный момент: конец массива содержит неизменённый массив x. Именно это знание и необходимо отразить. Необходимо написать, что для i <= j < 9-i y[j]=x[j]. Тогда слева появится конъюнкция и это тогда действительно будет тождественная истина.

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

Ссылки:


Формальная спецификация и верификация программ


Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14


Календарь

Сентябрь
03 10 17 24
Октябрь
01 08 15 22 29
Ноябрь
12 19 26
Декабрь
03 17
Семинары

01 02 03 04 05 06


Календарь

Сентябрь
01 08 15 22 29
Октябрь
06

Оформление задач|Проведение экзамена


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы