1. Доказательство корректности императивных программ с помощью логики Хоара

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2017Семинар 1Логика ХоараКорректность программСоглашение по умолчаниюВ условиях всех упражнений неявно подразумевается добавка“в естественной арифметической интерпретациинад целыми числами (Iar )”Упражнение 1Построить вычисление императивной программы на заданнойоценке переменныхx := z;while x < z doif x%2 thenx := 3 ∗ x + 1elsex := x/2fiodОценка переменных:1. {x/15, y/4, z/1}2. {x/3, y/1, z/0}Упражнение 2Является ли программаIчастично корректнойIтотально корректнойотносительно заданных триплетом предусловия и постусловия?{true}{true}{false}{false}{true}{x = 50}{false}{y = 50}x := 100x := 100x := 100x := 100x := 100x := 100x := 100x := 100{true}{false}{true}{false}{x = 100}{x = 50}{x = 50}{y = 50}Упражнение 2Является ли программаIчастично корректнойIтотально корректнойотносительно заданных триплетом предусловия и постусловия?{true}{true}{false}{false}{x > 3}{x > 3}{x < 3}{x < −3}while x 6= 0 do x := x − 1 odwhile x 6= 0 do x := x − 1 odwhile x 6= 0 do x := x − 1 odwhile x 6= 0 do x := x − 1 odwhile x 6= 0 do x := x − 1 odwhile x 6= 0 do x := x − 1 odwhile x 6= 0 do x := x − 1 odwhile x 6= 0 do x := x − 1 od{true}{false}{true}{false}{x = 0}{x > −5}{x = 0}{x = 5}Упражнение 2Является ли программаIчастично корректнойIтотально корректнойотносительно заданных триплетом предусловия и постусловия?{true} x := E(E — произвольное выражение){x = E }Массивы в программахIA[t] — терм, обозначающий t-й элемент массива AIпеременные программы делятся на целочисленные имассивныеIкаждая массивная переменная A встречается только втермах вида A[t]Iникакая целочисленная переменная x не можетобразовывать терм x[t]Iтерм вида A[t] может быть записан в левой частиприсваиванияIоценкой переменных программы определяются значениявсех целочисленных переменных, а также значения.

. . , A[−2], A[−1], A[0], A[1], A[2], . . .для каждой массивной переменной AIотношение переходов для присваивания A[t] := t 0 ,определяется естественным образомУпражнение 3Записать в виде предусловия и постусловия требованиекорректности программы, записанное на естественном языке1. программа записывает в переменную prod произведениезначений x и y2. программа записывает в переменные quo, rem частное иостаток от деления положительного значения x наположительное значение y3.

программа меняет местами значения переменных x, y4. программа записывает в переменную m максимальное иззначений s[0 : n − 1]5. программа разворачивает задом наперёд совокупностьзначений s[0 : n − 1]Новое обозначение: s[t1 , t2 ] — это совокупность значений(s[t1 ], s[t1 + 1], . . . , s[t2 ])Упражнение 4Вычислить слабейшее предусловие для заданных программы ипостусловияx := x + 10 {x = 7}x := x + 10 {true}x := x + 10 {false}x := x + 10 {x = x + 10}x := x + 10; y := x + y {x = A & y = B}if x = y then x := 7 else x := x + y + 2 fi{x = A & y = B & z = C}a[1] := x {∀i (0 ≤ i & i ≤ n → a[i] < 7)}a[y] := x {a[3] = 7}Упражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:x := x + 1;y := y + 1Требования: если значения переменных x, y совпадали довыполнения программы, то будут совпадать и послевыполненияУпражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:z := x;x := y;y := zТребования: значения переменных x, y меняются местамиУпражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:x := 1;a[1] := 2;a[x] := xТребования: в переменную a[1] записывается единицаУпражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:x := 0;while a[x] 6= 0 dox := x + 1odТребования: если на входе верно a[0 : 1] = (1, 0), то послевыполнения программы значения a[0] и a[1] не изменяются, икроме того, a[x] = 0Упражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:x := 2;while a[x] 6= 0 dox := x + 1odТребования: если на входе верно a[0 : 1] = (1, 0), то послевыполнения программы значения a[0] и a[1] не изменяются, икроме того, a[x] = 0Упражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:quo := 0; rem := x;while rem ≥ y dorem := rem − y;quo := quo + 1odТребования: в переменную quo записывается частное, а впеременную rem — остаток от деления неотрицательногозначения x на неотрицательное значение yУпражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:quo := 0; rem := x;while rem ≥ y dorem := rem − y;quo := quo + 1odТребования: в переменную quo записывается частное, а впеременную rem — остаток от деления неотрицательногозначения x на положительное значение yНемного о тотальной корректностиДля обоснования тотальной корректности частично корректнойпрограммы достаточно доказать, что для любой оценкипеременных, удовлетворяющей предусловию, число витковкаждого цикла при выполнении программы конечноДля этого достаточно для каждого цикла предоставитьограничивающую функцию (bound function), то есть выражениеE , удовлетворяющее двум условиям:Iпосле выполнения одного витка цикла значение выраженияE обязательно уменьшаетсяIзначение выражения E перед каждой проверкой условияцикла ограничено снизу константой, зависящей только отоценки переменных перед началом выполнения циклаНемного о тотальной корректностиПримерОграничивающей функцей для циклаwhile x < 0 do x := x + 1 odи произвольной оценки переменных перед началом выполненияцикла является выражение −x:Iзначение −x уменьшается на единицу после каждого виткациклаIследующий виток цикла выполняется только при условииx < 0, то есть −x > 0, а значит, значение −x передкаждой проверкой условия цикла ограничено снизузначением max(x0 , 0), где x0 — оценка переменной x передначалом выполнения циклаУпражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:pr := 0; cou := y;while cou > 0 dopr := pr + x;cou := cou − 1odТребования: в переменную pr записывается произведениенеотрицательных значений x, yУпражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:x := 0; y := 1; cou := n;while cou > 0 doh := y;y := x + y;x := h;cou := cou − 1odТребования: в переменную x записывается n-е числоФибоначчи, n ≥ 0Упражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:i := 1; m := s[0];while i < n doif s[i] < m thenm := s[i]fi;i := i + 1odТребования: в переменную m записывается максимальное иззначений s[0 : n − 1], n ≥ 1Новое обозначение: if C then π fi — это сокращение дляif C then π else ∅ fiУпражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:sum := 0; i := 0;while i < n dosum := sum + s[i];i := i + 1odТребования: в переменную sum записывается сумма значенийs[0 : n − 1], n ≥ 1Упражнение 5Доказать частичную корректность и проверить тотальнуюкорректность программы относительно заданных требованийПрограмма:i := 0;while 2 ∗ i < n − 1 doy := s[i];s[i] := s[n − i − 1];s[n − i − 1] := y;i := i + 1odТребования: массив s[0 : n − 1] разворачивается задомнаперёд, n ≥ 1ChallengeДоказать тотальную корректность программы,правильная работа которой — этосортировка совокупности значений s[0 : n − 1], n ≥ 1,по неубываниюПрограмма:i := n − 1;while i > 0 dok := i; j := i − 1;while j ≥ 0 doif s[j] > s[k] thenk := jfi;j := j − 1od;y := s[k]; s[k] := s[i]; s[i] := y;i := i − 1od.