Учебное пособие по методам Флойда, страница 8
Описание файла
PDF-файл из архива "Учебное пособие по методам Флойда", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 8 страницы из PDF
x ≥ 0 (1 = 1 0 = x (-1 + 1)) ∧ (1 = -1 0 = x2 + (-1))2. x ≥ 0 ∧ 0 ≤ y2 + y3 ≤ x ∧ (y3 = 1 y1 = x (y2 + 1)) ∧ (y3 = -1 y1= x2 + y2) (y3 = 1 y1 + y4 = x (y2 + y3 + 1)) ∧ (y3 = -1 y1+ y4 = x2 + y2 + y3)633. x ≥ 0 ∧ y2 + y3 > x ∧ (y3 = 1 y1 = x (y2 + 1)) ∧ (y3 = -1 y1 =x2 + y2) (-y3 = 1 y1 = x (y2 + 1)) ∧ (-y3 = -1 y1 = x2 +y2)4. x ≥ 0 ∧ y2 + y3 < 0 ∧ (y3 = 1 y1 = x (y2 + 1)) ∧ (y3 = -1 y1 =x2 + y2) y1 = x2Первая формула истинна, т. к.
истинно следствие.Проведемэквивалентноепреобразованиевторойформулы,разбив ее на три случая:2а. y3 = 1 (x ≥ 0 ∧ 0 ≤ y2 + 1 ≤ x ∧ y1 = x (y2 + 1) y4 = x)2б. y3 = -1 (x ≥ 0 ∧ 0 ≤ y2 - 1 ≤ x ∧ y1 = x2 + y2 y4 = -1)2в. y3 ≠ 1 ∧ y3 ≠ -1 (x ≥ 0 ∧ 0 ≤ y2 + y3 ≤ x T)Формулы 2a и 2б опровержимы: для 2а достаточно взять y4 неравным х, а для 2б взять y4 не равным -1. Посмотрев еще раз нарассмотренные только что вычисления, можно заметить, что,действительно, при y3 = 1 выполнено, что y4 = x, а при y3 = -1выполнено, что y4 = -1. Тогда рассмотрим в качестве p такойпредикат:(y3 = 1 y1 = x (y2 + 1) ∧ y4 = x) ∧ (y3 = -1 y1 = x2 + y2 ∧ y4 =-1)Подставим его в указанные выше 4 формулы:1.
x ≥ 0 (1 = 1 0 = x (-1 + 1) ∧ x = x) ∧ (1 = -1 0 = x2 +(-1) ∧ x = -1)2. x ≥ 0 ∧ 0 ≤ y2 + y3 ≤ x ∧ (y3 = 1 y1 = x (y2 + 1) ∧ y4 = x) ∧ (y3= -1 y1 = x2 + y2 ∧ y4 = -1) (y3 = 1 y1 + y4 = x (y2 + y3+ 1) ∧ y4 = x) ∧ (y3 = -1 y1 + y4 = x2 + y2 + y3 ∧ y4 = -1)643. x ≥ 0 ∧ y2 + y3 > x ∧ (y3 = 1 y1 = x (y2 + 1) ∧ y4 = x) ∧ (y3 =-1 y1 = x2 + y2 ∧ y4 = -1) (-y3 = 1 y1 = x (y2 + 1) ∧ -1= x) ∧ (-y3 = -1 y1 = x2 + y2 ∧ -1 = -1)4. x ≥ 0 ∧ y2 + y3 < 0 ∧ (y3 = 1 y1 = x (y2 + 1) ∧ y4 = x) ∧ (y3 = -1 y1 = x2 + y2 ∧ y4 = -1) y1 = x2Первая формула, очевидно, истинна.
Вторую формулу разобьемна три формулы, как это было сделано ранее:2а. y3=1 (x ≥ 0 ∧ 0 ≤ y2 + 1 ≤ x ∧ y1 = x (y2 + 1) ∧ y4 = x y4=x)2б. y3=-1 (x ≥ 0 ∧ 0 ≤ y2 - 1 ≤ x ∧ y1 = x2 + y2 ∧ y4 = -1 y4= -1)2в. y3 ≠ 1 ∧ y3 ≠ -1 (x ≥ 0 ∧ 0 ≤ y2 + y3 ≤ x T)Все три формулы истинны. Сделаем теперь то же с третьейформулой:3а. y3 = 1 (x ≥ 0 ∧ y2 + 1 > x ∧ y1 = x (y2 + 1) ∧ y4 = x y1 =x2 + y2)3б.
y3 = -1 (x ≥ 0 ∧ y2 -1 > x ∧ y1 = x2 + y2 ∧ y4 = -1 y1 = x(y2 + 1) ∧ -1 = x)3в. y3 ≠ 1 ∧ y3 ≠ -1 (x ≥ 0 ∧ y2 + y3 > x T)Формула 3а опровержима, контрпример: x = 3, y1 = 15, y2 = 4, y3= 1, y4 = 3. Анализируем вычисление при x = 3. Получаем, что y2не может принимать значение 4, т. к. он не должен быть больше х.Если добавить в индуктивное утверждение условие y2 ≤ x, тоформулы 3а и 3б становятся истинными. Формула 3в осталасьистинной.
Тем самым, предлагаем в качестве нового индуктивногоутверждения следующее:65y2 ≤ x ∧ (y3 = 1 y1 = x (y2 + 1) ∧ y4 = x) ∧ (y3 = -1 y1 = x2 + y2∧ y4 = -1)Подставляем в условия верификации:1. x ≥ 0 -1 ≤ x ∧ (1 = 1 0 = x (-1 + 1) ∧ x = x) ∧ (1 = -1 0 = x2 -1 ∧ x = -1)2. x ≥ 0 ∧ 0 ≤ y2 + y3 ≤ x ∧ y2 ≤ x ∧ (y3 = 1 y1 = x (y2 + 1) ∧ y4 =x) ∧ (y3 = -1 y1 = x2 + y2 ∧ y4 = -1) y2 + y3 ≤ x ∧ (y3 = 1 y1 + y4 = x (y2 + y3 + 1) ∧ y4 = x) ∧ (y3 = -1 y1 + y4 = x2 +y2 + y3 ∧ y4 = -1)3. x ≥ 0 ∧ y2 + y3 > x ∧ y2 ≤ x ∧ (y3 = 1 y1 = x (y2 + 1) ∧ y4 = x) ∧(y3 = -1 y1 = x2 + y2 ∧ y4 = -1) y2 ≤ x ∧ (-y3 = 1 y1 = x(y2 + 1) ∧ -1 = x) ∧ (-y3 = -1 y1 = x2 + y2 ∧ -1 = -1)4. x ≥ 0 ∧ y2 + y3 < 0 ∧ y2 ≤ x ∧ (y3 = 1 y1 = x (y2 + 1) ∧ y4 = x) ∧(y3 = -1 y1 = x2 + y2 ∧ y4 = -1) y1 = x2Первые три формулы истинны.
Четвертую формулу разобьем натри подформулы:4а. y3 = 1 (x ≥ 0 ∧ y2 < -1 ∧ y2 ≤ x ∧ y1 = x (y2 + 1) ∧ y4 = x y1= x2)4б. y3 = -1 (x ≥ 0 ∧ y2 < 1 ∧ y2 ≤ x ∧ y1 = x2 + y2 ∧ y4 = -1 y1= x2)4в. y3 ≠ 1 ∧ y3 ≠ -1 (x ≥ 0 ∧ y2 + y3 < 0 ∧ y2 ≤ x y1 = x2)Формула 4а ложна, контрпример: x = 2, y1 = -2, y2 = -2, y3 = 1,y4 = 2. Но этот контрпример не реализуется при вычислении х = 2,т. к.
y2 не может быть равен -2, он должен быть больше или равен-1.Формула4бложнадажепривыполнениитолькочтонайденного условия для y2, контрпример: x = 2, y1 = 3, y2 = -1, y3 =-1, y4 = -1. В этом вычислении при y3 = -1 y2 не может быть равен66-1. Формула 4в ложна, т. к. всегда можно подобрать значение y1, неравное x2, контрпример: x = 0, y1 = 1, y2 = 0, y3 = -2, y4 = 0. Этотпример не реализуется, т. к. y3 не может равняться -2: из анализавычислений следует, что y3 всегда равно 1 или -1. Объединяявышесказанное,составляемновыйвариантиндуктивногоутверждения:-1 ≤ y2 ≤ x ∧ ((y3 = 1 ∧ y1 = x (y2 + 1) ∧ y4 = x) (y3 = -1 ∧ y1 = x2 +y2 ∧ y4 = -1 ∧ y2 ≥ 0))Подставим это индуктивное утверждение в 4 формулы:1. x ≥ 0 -1 ≤ -1 ≤ x ∧ ((1 = 1 ∧ 0 = x (-1 + 1) ∧ x = x) (1 = -1∧ 0 = x2 - 1 ∧ x = -1 ∧ -1 ≥ 0))2.
x ≥ 0 ∧ 0 ≤ y2 + y3 ≤ x ∧ -1 ≤ y2 ≤ x ∧ ((y3 = 1 ∧ y1 = x (y2 + 1) ∧ y4= x) (y3 = -1 ∧ y1 = x2 + y2 ∧ y4 = -1 ∧ y2 ≥ 0)) -1 ≤ y2 + y3≤ x ∧ ((y3 = 1 ∧ y1 + y4 = x (y2 + y3 + 1) ∧ y4 = x) (y3 = -1 ∧ y1+ y4 = x2 + y2 + y3 ∧ y4 = -1 ∧ y2 + y3 ≥ 0))3. x ≥ 0 ∧ y2 + y3 > x ∧ -1 ≤ y2 ≤ x ∧ ((y3 = 1 ∧ y1 = x (y2 + 1) ∧ y4 =x) (y3 = -1 ∧ y1 = x2 + y2 ∧ y4 = -1 ∧ y2 ≥ 0)) -1 ≤ y2 ≤ x ∧((-y3 = 1 ∧ y1 = x (y2 + 1) ∧ -1 = x) (-y3 = -1 ∧ y1 = x2 + y2 ∧-1 = -1 ∧ y2 ≥ 0))4.
x ≥ 0 ∧ y2 + y3 < 0 ∧ -1 ≤ y2 ≤ x ∧ ((y3 = 1 ∧ y1 = x (y2 + 1) ∧ y4 =x) (y3 = -1 ∧ y1 = x2 + y2 ∧ y4 = -1 ∧ y2 ≥ 0)) y1 = x2Все формулы истинны, подходящее индуктивное утверждениенайдено.2.3 Задачи на метод индуктивных утвержденийВо всех следующих задачах нужно доказать частичную корректность блок-схемы при помощи метода индуктивных утверждений67относительно спецификации (, ).
Доменом всех переменных являются целые числа.2.3.1 Блок-схема на рисунке 9, (x) = (x ≥ 0), (x, z) = (z ≥ 0).START:(y1, y2) ← (x, 0)(y1, y2) ← (y1 + x + y2, (y2 + 1) * x + y1* y1)(y1, y2) ← (y2, y1 * x)Fy1 < x + y2THALT:z ← y1 + y2Рисунок 9. Рисунок к задаче2.3.2 Блок-схема на рисунке 10, (x) = (x > 0), (x, z) = (z > 0).START:y1 ← xFTy1 < 0HALT:z ← y1y1 ← -10Рисунок 10. Рисунок к задаче2.3.3 Блок-схема на рисунке 10, (x) = (x < 0), (x, z) = (z < 0).682.3.4 Блок-схема на рисунке 11, (x1, x2) = (x1 > x2), (x1, x2, z1, z2)= (z1 – x1 = z2 – x2).START:(y1, y2) ← (x1- x2, 0)FTy1 * y 2 < x2HALT:(z1, z2) ← (y1, y2)y1 ← y1 * y2 - x2(y1 , y2) ← (y1 + 2x1, y1 + x1 + x2)Рисунок 11.
Рисунок к задаче2.3.5 Блок-схема на рисунке 12, (x) = (x ≥ 0), (x, z) = (z = x2).START:(y1, y2, y3) ← (x, 1, 1)Ty1 > 0Fy1 ← y1 + xy1 ← y1 - y3y3 ← y2 - y3Ty3 > 0y2 ← y2 - 1y1 < y2 + xFy2 ← y2 - 1TFHALT:z ← y1 + y2 + 1Ty2 < -2xРисунок 12. Рисунок к задаче69F2.3.6 Блок-схема на рисунке 13, (x) = (x ≥ 0), (x, z) = (z2 ≤ x <(z + 1)2).START:(y1, y2, y3) ← (0, 0, 1)y2 ← y2 + y3TFy2 > xHALT:z ← y1(y1 , y3) ← (y1 + 1, y3 + 2)Рисунок 13. Рисунок к задаче2.4 Задачи на метод фундированных множествВо всех задачах доменом всех переменных является множествоцелых чисел. Доказательство проводить при помощи методафундированных множеств.702.4.1 Доказать,чтоблок-схеманарисунке14всегдазавершается.START:y1 ← 0TFy1 > xHALT:z ← y1y1 ← y1 + 2Рисунок 14.
Рисунок к задаче2.4.2 Доказать, что блок-схема на рисунке 15 завершается привсех неотрицательных значениях входной переменной х.START:(y1, y2) ← (0, 1)y2 ← 1 - y2Ty1 = xFTHALT:z ← y1 + y2y1 ← y1 + 2Рисунок 15. Рисунок к задаче71y2 = 1Fy1 ← y1 - 12.4.3 Доказать, что блок-схема на рисунке 16 завершается привсех неотрицательных значениях входной переменной х.START:(y1, y2) ← (0, 0)FTy1 = xFy1 ← y1 + 1y2 = xTHALT:z ← y1 + y2(y1 , y2) ← (0, y2 + 1)Рисунок 16. Рисунок к задаче2.4.4 Доказать, что блок-схема на рисунке 17 завершается привсех неотрицательных значениях входной переменной х.START:(y1, y2) ← (x, 1)FTy1 = 0HALT:z ← y1 + y2(y1 , y2) ← (y2 - y1, -y2)Рисунок 17.
Рисунок к задаче722.4.5 Доказать, что блок-схема на рисунке 18 завершается привсех значениях входной переменной х>0.START:(y1, y2, y3, y4) ← (x, 1, x-1, x)TFy1 = 0(y2 , y4) ← (-y2, y4 - 1)(y1 , y3) ← (y1 - y2, y3 - y2)y4 = 0(y1 , y3) ← (y2∙ y4, y1 - y2)FTHALT:z ← y1 + y2Рисунок 18. Рисунок к задаче2.4.6 Доказать, что блок-схема на рисунке 19 завершается привсех неотрицательных значениях входной переменной х.START:(y1, y2) ← (0, 1)Ty1 = хFy2 ← -хFy1 = 0Ty1 ← y1 + y2HALT:z ← y1 + y2Рисунок 19. Рисунок к задаче732.4.7 Доказать, что блок-схема на рисунке 20 завершается привсех положительных значениях входной переменной х.START:(y1, y2) ← (1, 1)(y1 , y2) ← (y1 + y2, 1)TFy1 ≥ хy2 ← -хFy1 = 0y1 ← y1 + y2THALT:z ← y1 + y2Рисунок 20. Рисунок к задаче2.4.8 Доказать, что блок-схема на рисунке 21 завершается привсех неотрицательных значениях входной переменной х.START:(y1, y2) ← (x, 0)FTy1 = 0(y1 , y2) ← (y1 - 1, y1 + y2)Ty2 = 0HALT:z ← y1 + y2Рисунок 21.
Рисунок к задаче74F(y1 , y2) ← (y1 + y2, y2 - 1)2.4.9 Доказать,чтоблок-схеманарисунке22всегдазавершается.START:(y1, y2) ← (x, x)FTy1 > 1THALT:z ← y1 + y2y2 * y2 < y1(y1 , y2) ← (y1 - 1, y1*y2 + 1)Рисунок 22. Рисунок к задаче75Fy2 ← y2 - 22.5 Общие задачи2.5.1 Доказать полную корректность программы относительно входного предиката (x 0) ∧ (x ⋮ 3) ивыходного предиката ( 3z x2 ) при помощи методов Флойда.
Доменом всех переменных являетсямножество целых чисел.START:( y1, y2, y3) ( 0, 0, 0 )Fy3 ≥ x( y1, y2, y3) ( y1+y3+4, y2+5, y3+3 )76THALT:z 2y1- y22.5.2 Доказать полную корректность програм-START:( y1, y2, y3 ) ( 0, 0, 1 )мы относительно входного предиката (x 0) ивыходного предиката ( z2 x (z + 1)2 ). Доменом всех переменных является множество целыхчисел.y2 y2 + y3F( y1, y3 ) ( y1+1, y3 + 2 )77y2 xTHALT:z y12.5.3 Доказать полную корректность программы относительно входного предиката (x 0) и выходногопредиката ( z (2x)! ) при помощи методов Флойда.
