Учебное пособие по методам Флойда, страница 7
Описание файла
PDF-файл из архива "Учебное пособие по методам Флойда", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 7 страницы из PDF
Если спецификация не указана, считается,что она содержит тождественно истинные предусловие и постусловие. Если в функции указанное условие может быть выполнено,обоснуйте это.a) void swap(int *x, int *y) {int t = *x;*x = *y;*y = t;}непосредственно в этой функции происходитразыменование нулевого указателя.b) long list_sum(struct node_t *list) {long sum = 0L; struct_node_t *p = list;while (p != 0) {sum += p->value;p = p->next;}return sum;}сумма элементов списка из одного элемента большезаглавного элемента.552 Практикум по методам ФлойдаВданномразделеприводитсябольшоечислозадачнадоказательство полной корректности блок-схем.2.1 Ещё один пример доказательства полнойкорректностиSTART:( y1, y2 ) ( x1, x2 )Fy1 y2T( y1, y2 ) ( y2, y1 )FTy1 0HALT:z y2( y1, y2 ) ( rem(y2, y1), y1 )Рисунок 6.
Блок-схема программы вычисления наибольшего общего делителя.Нарисунке6представленаблок-схемапрограммынадмножеством переменных V, вычисляющая наибольший общийделитель. Множество переменных V = {x1, x2, y1, y2, z} состоит издвух входных, двух промежуточных и одной выходной переменных.Доменом всех переменных является множество целых чисел.56Операторrem(y1, y2)обозначаетостатокприцелочисленномделении y1 на y2.Необходимоотносительнодоказатьвходногополнуюпредикатакорректность (x1 0)∧блок-схемы(x2 0)ивыходного предиката ( z НОД(x1, x2) ).START:( y1, y2 ) ( x1, x2 )Fy1 y2BT( y1, y2 ) ( y2, y1 )CFAy1 0( y1, y2 ) ( rem(y2, y1), y1 )THALT:z y2Рисунок 7.
Блок-схема вычисления НОД с точкой сеченияРешение:Для доказательства корректности программы нам будут полезныследующие свойства наибольшего общего делителя:Утверждение 1. Если натуральное число a не делится безостатка на натуральное число b, то НОД(a, b) = НОД(rem(a,b), b).Утверждение 2. Если натуральное число a делится нанатуральное число b, то НОД(a, b) = b.571. Доказательство частичной корректности программы.Выберем точку сечения программы наШаг 1.
Точки сечения.переходе,выходящемизнижнегоусловногооператораипомеченном символом F. На рисунке 7 эта точка сечения помеченасимволом A. Эта точка сечения разбивает единственный цикл,имеющийся в программе, и поэтому определять другие точкисечения не требуется.Шаг 2. Индуктивные утверждения.Поставим в соответствиеединственной точке сечения индуктивное утверждениеp(x1, x2, y1, y2) = (0 y1 y2) ∧ (НОД(x1, x2) =НОД(y1, y2)).Перечислим все базовые путиШаг 3.
Условия верификации.программы:1. START-B-HALT4. START-C-A2. START-C-HALT5. A-A3. START-B-AРассмотрим условия6. A-HALTверификации, соответствующиеэтимпутям.START-B-HALT x1 x2 (x1 0) ∧ (x2 0) ∧ (x1 x2) ∧ (x1 0) (x2 НОД(x1, x2))Предпосылкаявляетсяложной,таккакx1неможетодновременно равняться 0 и быть больше 0. Следовательно, данноеусловие верификации является истинным.START-C-HALTx1x2 (x1 0)∧ (x2 0)( x1 НОД(x1, x2) )58∧ (x1x2)∧ (x2 0)Опять предпосылка является ложной, так как x2 не можетодновременно равняться 0 и быть больше 0. Следовательно, данноеусловие верификации является истинным.START-B-A x1 x2 (x1 0) ∧ (x2 0) ∧ (x1 x2) ∧ (x1 0) (0 x1 x2)∧ (НОД(x1, x2) = НОД(x1, x2))START-C-A x1 x2 (x1 0) ∧ (x2 0) ∧ (x1 x2) ∧ (x2 0) (0 x2 x1) ∧(НОД(x1, x2) = НОД(x2, x1))A-A x1 x2 y1 y2 (x1 0) ∧ (x2 0) ∧ (0 y1 y2) ∧ (НОД(x1, x2) =НОД(y1, y2)) ∧ (rem(y2, y1) = 0) (0 rem(y2, y1) y1) ∧(НОД(x1, x2) = НОД(rem(y2, y1), y1))A-HALT x1 x2 y1 y2 (x1 0) ∧ (x2 0) ∧ (0 y1 y2) ∧ (НОД(x1, x2) =НОД(y1, y2)) ∧ (rem(y2, y1) = 0) ( y1 НОД(x1, x2) )2.
Доказательство завершимости программы.Шаг 1. Точки сечения. Выберем ту же точку сечения программы, что и в предыдущем случае. В качестве индуктивного утверждения выберем q(x1, x2, y1, y2) = (0 y1 y2), которое являетсяследствием индуктивного утверждения, использовавшегося ранее.Это мы сделаем для сокращения доказательства завершаемости: вопервых, не нужно повторно составлять условия верификации, а, вовторых, условия корректности и завершимости будут короче.
В качестве фундированного множества мы возьмем множество натуральных чисел с естественным отношением порядка.59Шаг2.Оценочныефункции.Поставимвсоответствиеединственной точке сечения оценочную функцию u(x1, x2, y1, y2) =y1. Значения этой переменной неотрицательны и убывают на каждой итерации. Осталось это показать формально.Сформулируем условие корректности определения оценочнойфункции: x1 x2 y1 y2 (x1 0) ∧ (x2 0) ∧ (0 y1 y2) (y1 > 0)Это условие является истинным.Шаг 3. Условия завершимости. Рассмотрим все промежуточныебазовые пути блок-схемы. В данном случае – это единственныйпуть A-A. Запишем для него условие завершимости: x1 x2 y1 y2 (x1 0) ∧ (x2 0) ∧ (0 y1 y2) ∧ (rem(y2, y1) =0) (y1 > rem(y2, y1))Это условия является истинным, так как при целочисленном делении одного положительного числа на другое остаток по определению меньше делителя.Шаг 4.
Условия успешности вычисления функций. В блок-схемеиспользуется операция rem(y2, y1), которая не определена приy1 = 0. Поэтому необходимо доказать, что всякий раз при вычислении этой операции будет соблюдено условие y1 ≠ 0. Для этого составим следующее условие корректности: x1 x2 y1 y2 (x1 0) ∧ (x2 0) ∧ (0 y1 y2) (y1 ≠ 0)Это условие также является истинным.Мы доказали частичную корректность относительно (, ) иуспешную завершаемость программы на .
Из этого по лемме 2следует полная корректность программы.602.2 Одинподходкпостроениюиндуктивныхутверждений и оценочных функцийОсновной сложностью данных задач является выбор подходящих индуктивных утверждений и оценочных функций.Индуктивные утверждения выбираются, исходя из семантикипрограммы, как инварианты на значение переменных в соответствующей точке. Эти инварианты должны быть достаточны для доказательства всех условий в методе индуктивных утверждений (и,при необходимости, в методе фундированных множеств).Для выбора индуктивных утверждений бывает полезно выписать значения всех промежуточных переменных в предполагаемойточке сечения для нескольких наборов входных данных.
Это можетподсказать зависимость между переменными и выразить её в видепредиката. Последующая проверка корректности выбранных утверждений выполняется при доказательстве сформулированных условий верификации, корректности и завершимости. Если какое-то изусловий не доказывается, то, как правило, становится видно, чтоименно необходимо изменить в индуктивном утверждении для исправления ситуации.Оценочные функции выбираются для обеспечения монотонногоубывания некоторой величины при каждом переходе по промежуточному базовому пути.Прокомментируем сказанное об индуктивных утверждениях напримере.
Требуется доказать частичную корректность блок-схемына рисунке 8 относительно входного предиката (x ≥ 0) и выходного предиката ( z x2 ). Домены всех переменных — целыечисла.61START:(y1, y2, y3, y4) ← (0, -1, 1, x)TAF0 ≤ y2 + y3 ≤ xFT(y1, y2) ← (y1 + y4, y2 + y3)y2 + y3 < 0(y3, y4) ← (- y3, -1)HALT:z ← y1Рисунок 8. К демонстрации метода построения индуктивых утвержденийВыберем точки сечения так, чтобы уменьшить число условийверификации. Для этого можно выбрать точку А, как это показанона рисунке 8, и обозначить индуктивное утверждение, приписанноеэтой точке, как p(x, y1, y2, y3, y4). Тогда мы должны подобрать такоевыражениедляпредикатаследующиеусловияp,чтобыверификациибыли(длявыполненысокращениявсезаписикванторы опущены):1.
x ≥ 0 p(x, 0, -1, 1, x)2. x ≥ 0 ∧ 0 ≤ y2 + y3 ≤ x ∧ p(x, y1, y2, y3, y4) p(x, y1 + y4, y2 + y3,y3, y4)3. x ≥ 0 ∧ y2 + y3 > x ∧ p(x, y1, y2, y3, y4) p(x, y1, y2, -y3, -1)4. x ≥ 0 ∧ y2 + y3 < 0 ∧ p(x, y1, y2, y3, y4) y1 = x2Самым простым индуктивным утверждением, инвариантом,является тождественно истинный инвариант. Проверим, может либытьp(x, y1, y2, y3, y4) T62При таком p первые три формулы истинны, а последняя ложна.Посмотрим контрпример для последней формулы, если p T, т.
е.подберем такие значения для переменных, при которых посылкаистинна, а заключение ложно. Например, контрпримером будуттакие значения: x = 0, y1 = 1, y2 = 0, y3 = -1, y4 = 0.Проанализируем, может ли такой контрпример реализоватьсяпри указанном х. Для этого достаточно выписывать вычислениепри этом значении переменной х. Получится, что, например, y1 вовсех конфигурациях равен 0, но не 1, как в контрпримере. Т.е.индуктивное утверждение p T не позволяет доказать последнююформулу, т. е. из него не следует, что y1 = x2. Проанализируем,какие инвариантные свойства обеспечит выполнение этого условия.Можно попытаться это определить, выписав разные вычисления.Можно сделать вывод, что y1 сначала возрастает, начиная с 0,увеличиваясь на х, а затем убывает до x2. Причем при возрастанииy3равен1,априубываниионравен-1.Тогдаможносформулировать такие следствия:y3 = 1 y1 = x (y2 + 1)y3 = -1 y1 = x2 + y2Тогда возьмем в качестве p такой предикат: (y3 = 1 y1 = x (y2 +1)) ∧ (y3 = -1 y1 = x2 + y2) и подставим его в написанные выше 4формулы:1.