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

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

Версия 19:28, 2 октября 2010

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

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

Фундированное множество. Что такое частично упорядоченное множество, мы помним. Фундирование —- частично упорядоченное, в котором не существует бесконечно упорядоченной последовательности: (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]. Тогда слева появится конъюнкция и это тогда действ. будет тожд. истина.

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

Ссылки:

• Аналитическая верификация