Редактирование: МФСП, 08 лекция (от 22 октября)

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

Версия от 08:28, 28 января 2009; 212.192.248.201 (Обсуждение)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

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

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

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

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

Шаг 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;, то когда приддём в конец, то оценочная функция даст на знач. строго меньшее, чем оценосчная функция в начале. Тем самым у нас уменьш. знач. функции, и, поск. мн-во фундированное, мы не сможем юеск. зодить по базовым путям и в конце уконцов выйдем на заверш. оператор.

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

Какие есть ньюансы: 
# То, что при опр. оценочных функций и фунир. мн-ве неоюбх. показывать, что оценоч. функция опр. корректно. Что это значит: посм. на примере: у нас был инвар. определён следующего вида: 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 у нас отл. от того, что исп. на пред. шаге, то нам необх. вып. все усл. вериф., которые выпис. на осн .... . Поэтому лучше модиф. доказ., чтобы два разане выпис очень похожие условия.

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

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

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

Выбир точку, выбир индуктивное утв. 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

Несложно видеть, что данное усл. завершимости явл. корректным, поск. (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_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 относитлеьно &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, то есть, явл. корр. индексом, чтобы программа вып. также корректно.

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

Cajhv/ vjlba/ vtnjlf Akjqlf? rjnjhst gjnh/ lkz hf,jns c vfccbdjv/ Gthtl 'nbv лектор хотел бы сказать, что товарищ МакКарти можно задать как две операции и аксиомы работы с ними:
* x: Nat[N]
* 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]
Этих опер. дост. Аксиомы, соотв., такие:
* &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

Для метода инд. утверждение у нас ост. всё то же самое:

* Ш1. 
* Ш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

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

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

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

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

Теперь необх. сформю спецификацию:
* Предусловие: &phi; &equiv; true
* Постусловие: &psi; &equiv; &forall; i &isin; {0..9}: z[i] = x[9-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])

Ш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]. Тогда слева появится конъюнкция и это тогда действ. будет тожд. истина.

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

Ссылки:
* [http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/Lecture-Analytical%20Verification.doc Аналитическая верификация]

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://libesyr.so/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_08_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_22_%D0%BE%D0%BA%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29