Редактирование: МФСП, 08 лекция (от 22 октября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 67: | Строка 67: | ||
* ∀ x ∀ i (i=i_j) ⇒ c(a(x, i_1, n_1, ..., i_k, n_k), i) = n_j | * ∀ x ∀ i (i=i_j) ⇒ c(a(x, i_1, n_1, ..., i_k, n_k), i) = n_j | ||
- | Для метода | + | Для метода индукционных утверждений у нас осталось всё то же самое: |
* Ш1. | * Ш1. | ||
* Ш2. | * Ш2. | ||
- | * Ш3. | + | * Ш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: | START: | ||
Строка 92: | Строка 92: | ||
(y[0-i, y[i]], i+1) z ← y | (y[0-i, y[i]], i+1) z ← y | ||
- | Теперь | + | Теперь необх. сформю спецификацию: |
* Предусловие: φ ≡ true | * Предусловие: φ ≡ true | ||
* Постусловие: ψ ≡ ∀ i ∈ {0..9}: z[i] = x[9-i] | * Постусловие: ψ ≡ ∀ i ∈ {0..9}: z[i] = x[9-i] | ||
Строка 98: | Строка 98: | ||
Ш1. Выберем точку сечения: i. | Ш1. Выберем точку сечения: i. | ||
- | Ш2. На втором шаге | + | Ш2. На втором шаге необх. сформ. инд. утверждение: ∀ j ∈ N: 0 ≤ j ≤ i ⇒ (y[j]=x[9-j])∧(y[9-j]=x[j]) |
- | Ш3. | + | Ш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]. Тогда слева появится конъюнкция и это тогда действ. будет тожд. истина. |
- | + | Тем самым лектор зотел проилл. момент, что когда пишете инв., не забывайте вносить вещи, которые как бы очевидны. Это же отн. к огр. на обл. значений перем. | |
Ссылки: | Ссылки: |