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

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

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

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

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

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

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

Ссылки:

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