Лекции В.А. Захарова, страница 32

. . },Func = {+(2) , −(2) },Pred = {=(2) , >(2) , <(2) }while ¬(x = y )doif x > ythen x ⇐ x − yelse y ⇐ y − xfiodИМПЕРАТИВНЫЕ ПРОГРАММЫОперационная семантика императивных программСемантика задает смысл (значение) синтаксическихконструкций (слов, формул, программ и пр.).Значением императивной программы является отношениевход–выход между входными данными и результатомвычисления.Отношение вход–выход программы определяется при помощиотношения переходов между состояниями вычисленияпрограммы.Состояние вычисления программы определяется двумякомпонентами — состоянием управления и состояниемданных .ИМПЕРАТИВНЫЕ ПРОГРАММЫОпределение (состояния вычисления)Пусть Var — это множество переменных, а GTerm — этомножество основных термов сигнатуры σ.Оценкой переменных (состоянием данных) будем называтьвсякое отображение (подстановку) θ : Var → GTerm.Состоянием управления будем называть всякую программу, атакже специальный символ ∅.Состоянием вычисления будем называть всякую пару hπ, θi, гдеπ — состояние управления, а θ — оценка переменных.Запись Stateσ будет обозначать множество всевозможныхсостояний вычислений сигнатуры σ.ИМПЕРАТИВНЫЕ ПРОГРАММЫОпределение (отношения переходов)Пусть I — это интерпретация сигнатуры σ.Тогда отношение переходов для императивных программ — этобинарное отношение −→I на множестве состояний вычисленияStateσ , удовлетворяющее следующим требованиям:ASS: hx ⇒ t, θi −→I h∅, {x/t}θi;COMP_∅: hπ1 ; π2 , θi −→I hπ2 , ηiтогда и только тогда, когда hπ1 , θi −→I h∅, ηi;COMP: hπ1 ; π2 , θi −→I hπ10 ; π2 , ηiтогда и только тогда, когда hπ1 , θi −→I hπ10 , ηi и π10 6= ∅;ИМПЕРАТИВНЫЕ ПРОГРАММЫОпределение (отношения переходов)IF_1: hif C then π1 else π2 fi, θi −→I hπ1 , θiтогда и только тогда, когда I |= C θ;IF_0: hif C then π1 else π2 fi, θi −→I hπ2 , θiтогда и только тогда, когда I 6|= C θ;WHILE_1: hwhile C do π od, θi −→I hπ; while C do π od, θiтогда и только тогда, когда I |= C θ;WHILE_0: hwhile C do π od, θi −→I h∅, θiтогда и только тогда, когда I 6|= C θ.Отношение переходов −→I определяет, как изменяетсясостояние вычисления за один шаг работы интерпретатораимперативных программ.ИМПЕРАТИВНЫЕ ПРОГРАММЫОпределение (вычисления программы)Пусть π0 — это императивная программа, θ0 — оценкапеременных.Частичным вычислением программы π0 на оценке переменныхθ0 в интерпретации I называется последовательность (конечнаяили бесконечная) состояний вычисленияhπ0 , θ0 i, hπ1 , θ1 i, .

. . , hπn−1 , θn−1 i, hπn , θn i, . . . ,в которой для любого n, n ≥ 1, выполняется отношениеhπn−1 , θn−1 i −→I hπn , θn i.Вычислением программы π0 на оценке переменных θ0 винтерпретации I называется всякое частичное вычисление,которое нельзя продолжить.ИМПЕРАТИВНЫЕ ПРОГРАММЫПримерПусть I — интерпретация сигнатуры σ = hConst, Func, Predi:Const = {0, 1, 2, .

. . , }, Func = {+(2) , −(2) },Pred = {=(2) , >(2) , <(2) },предметной областью которой является множествонатуральных чисел N0 с обычными арифметическимиоперациями и отношениями.Рассмотрим вычисление программыπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x fi odна оценке переменных θ0 = {x/4, y /6}.ИМПЕРАТИВНЫЕ ПРОГРАММЫπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x fi odθ0 = {x/4, y /6}Примерhπ0 , {x/4, y /6}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x fi ; π0 , {x/4, y /6}i↓Ihy ⇐ y − x; π0 , {x/4, y /6}i↓Ihπ0 , {x/4, y /6 − 4}iИМПЕРАТИВНЫЕ ПРОГРАММЫπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x fi odθ0 = {x/4, y /6}Примерhπ0 , {x/4, y /6−4}i↓Ihif x > y then x ⇐ x − y else y ⇐ y − x fi ; π0 , {x/4, y /6−4}i↓Ihx ⇐ x − y ; π0 , {x/4, y /6−4}i↓Ihπ0 , {x/4−(6−4), y /6−4}i↓Ih∅, {x/4−(6−4), y /6−4}iИМПЕРАТИВНЫЕ ПРОГРАММЫКак следует из определения, любое вычисление либо являетсябесконечной последовательностью, либо завершаетсясостоянием h∅, ηi.

В последнем случае оценка η называетсярезультатом вычисления.Будем использовать запись −→∗I для обозначениярефлексивного и транзитивного замыкания отношенияпереходов −→I .Тогда оценка переменных η является результатом вычисленияпрограммы π на оценке переменных θ в интерпретации I в томи только том случае, когда выполняется отношениеhπ, θi −→∗I h∅, ηi.ЗАДАЧА ВЕРИФИКАЦИИ ПРОГРАММНеформальная постановка.Программа π считается (частично ) корректной , если длялюбых начальных данных, удовлетворяющих определенномуусловию ϕ, результат вычисления (если вычислениезавершается) удовлетворяет определенному условию ψ.Ограничение ϕ, которое налагается на начальные данные,называется предусловием , а требование ψ, которому должныудовлетворять результаты вычисления, называетсяпостусловием программы.Задача верификации программы π заключается в проверкечастичной корректности программы π относительно заданногопредусловия ϕ и заданного постусловия ψ.ЗАДАЧА ВЕРИФИКАЦИИ ПРОГРАММФормальная постановка.Расширим множество формул логики предикатов, введя врассмотрение в качестве формул выражения новогоспециального вида.ОпределениеТриплетом Хоара (тройкой Хоара) называется всякоевыражение видаϕ{π}ψ,где ϕ, ψ — формулы логики предикатов,а π — императивная программа.Обозначим HTσ множество триплетов Хоара сигнатуры σ.ЗАДАЧА ВЕРИФИКАЦИИ ПРОГРАММВыполнимость триплетов Хоара в интерпретацияхопределяется так:I |= ϕ{π}ψ⇐⇒для любых оценок переменных θ, η,если I |= ϕθ и hπ, θi −→∗I h∅, ηi,то I |= ψη.Определение (частичной корректности программы)Пусть ϕ, ψ — формулы логики предикатов, а π — императивнаяпрограмма.Программа π называется частично корректной в интерпретацииI относительно предусловия ϕ и постусловия ψ, если триплетϕ{π}ψ выполним в интерпретации I , т.

е.I |= ϕ{π}ψ .ЛОГИКА ХОАРАКак же доказать частичную корректность программы?Попробуем построить систему правил вывода, аналогичныхправилам вывода для семантических таблиц.Такую систему предложил в 1968 г. Хоар. Правила выводаХоара имеют видΦ,ΨΦ,ϕΦΦ,,Ψ1 , Ψ2 ϕ, Ψ, ψгде Φ, Ψ, Ψ1 , Ψ2 — триплеты Хоара,ϕ, ψ — формулы логики предикатов.ЛОГИКА ХОАРАПравила вывода ХоараASS:ϕ{x/t} {x ⇐ t} ϕ,trueCONS:ϕ{π}ψ,ϕ → ϕ0 , ϕ0 {π}ψ 0 , ψ 0 → ψCOMP:ϕ{π1 ; π2 }ψ,ϕ{π1 }χ, χ{π2 }ψIF:ϕ {if C then π1 else π2 fi} ψ,(ϕ&C ) {π1 } ψ, (ϕ&¬C ) {π2 } ψWHILE:ϕ {while C do π od} (ϕ&¬C ).(ϕ&C ) {π} ϕЛОГИКА ХОАРАОпределение вывода в логике ХоараВывод в логике Хоара триплета Φ0 = ϕ0 {π0 } ψ0 — этокорневое дерево,ЛОГИКА ХОАРАОпределение вывода в логике ХоараВывод в логике Хоара триплета Φ0 = ϕ0 {π0 } ψ0 — этокорневое дерево,y@y@@Ry@@@? @@Ryyy?y?yyЛОГИКА ХОАРАОпределение вывода в логике ХоараВывод в логике Хоара триплета Φ0 = ϕ0 {π0 } ψ0 — этокорневое дерево, вершинами которого служат триплеты иформулы логики предикатов и при этомΦyjyΦ0@@@R yΦ@1@@? @@ϕyyΦ3 R yϕ21?ϕy3?yϕ4ΦyiЛОГИКА ХОАРАОпределение вывода в логике ХоараВывод в логике Хоара триплета Φ0 = ϕ0 {π0 } ψ0 — этокорневое дерево, вершинами которого служат триплеты иформулы логики предикатов и при этом1) корнем дерева является триплет Φ0 ;ΦyjyΦ0@@@R yΦ@1@@? @@ϕyyΦ3 R yϕ21?ϕy3?yϕ4ΦyiЛОГИКА ХОАРАОпределение вывода в логике Хоара2)из вершины Φi исходят дуги в вершину Φj⇐⇒Φi — правило табличного вывода;ΦjΦyiΦyjyϕ3?yΦ 0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12yϕ4?ЛОГИКА ХОАРАОпределение вывода в логике Хоара2)из вершины Φi исходят дуги в вершину Φj⇐⇒Φi — правило табличного вывода;ΦjΦyiΦyjϕ3?yyΦ 0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12ϕ4?yЛОГИКА ХОАРАОпределение вывода в логике Хоара2)из вершины Φ1 исходят дуги в вершины ϕ1 , Φ3 , ϕ2⇐⇒Φ1— правило табличного вывода;ϕ1 , Φ3 , ϕ2ΦyiΦyj?yϕ3yΦ 0@@@Ry@Φ1@@? @@ϕyyΦ3 R yϕ21?yϕ4ЛОГИКА ХОАРАОпределение вывода в логике Хоара3) листьями дерева являются формулы логики предикатов.ΦyjyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12?yϕ3?yϕ4ΦyiЛОГИКА ХОАРАОпределение вывода в логике ХоараВывод триплета Φ0 = ϕ0 {π0 } ψ0 в логике Хоара называетсяуспешным в интерпретации I , если дерево вывода являетсяконечным, и все его листовые вершины — это истинные винтерпретации I формулы логики предикатов.ЛОГИКА ХОАРАПримерПокажем, что программаπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x fi odправильно вычисляет наибольший общий делитель двухположительных целых чисел.Для этого необходимо сформулировать предусловие ϕ0 ипостусловие ψ0 , соответствующее этому требованию, ипостроить успешный вывод триплета ϕ0 {π0 } ψ0 в логикеХоара.ЛОГИКА ХОАРАПримерДля удобства обозначений введем некоторые вспомогательныеформулы:DIV (x, z) :∃u (u × z = x),GCD(x, y , z) : DIV (x, z) & DIV (y , z) &∀u (DIV (x, u)&DIV (y , u) → (u ≤ z)).Тогдаϕ0 (x, y , z) : (x > 0) & (y > 0) & GCD(x, y , z),ψ0 (x, z) :z = x.π0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x fi od(x > 0)&(y > 0)&GCD(x, y , z) {π0 } z = x|{z} yPPPPPPϕ0 (x,y ,z))yϕ0 (x, y , z) → ϕ0 (x, y , z)PPqyϕ0 (x, y , z)&¬¬(x = y ) → (z = x)?yϕ0 (x, y , z) {π0 } ϕ0 (x, y , z)&¬¬(x = y )?yϕ0 (x, y , z)&¬(x = y ){if x > y thenPx ⇐ x −y else y ⇐ y −x fi}ϕ0 (x, y , z) PPPPPyPPqyϕ0 (x, y , z)&¬(x = y )&¬(x > y ){y ⇐ y −x}ϕ0 (x, y , z)ϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z)Левая ветвьϕ0 (x, y , z)&¬(x = y )&(x > y ){x ⇐ x −y }ϕ0 (x, y , z)PPyPPPPPqP)yϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z)yϕ0 (x, y , z) → ϕ0 (x, y , z)?yϕ0 (x − y , y , z){x ⇐ x −y }ϕ0 (x, y , z)ASS?ytrueПравая ветвьϕ0 (x, y , z)&¬(x = y )&¬(x > y ){x ⇐ y −x}ϕ0 (x, y , z)PPyPPPPPqP)yϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z)yϕ0 (x, y , z) → ϕ0 (x, y , z)?yϕ0 (x, y − x, z){y ⇐ y −x}ϕ0 (x, y , z)ASS?ytrueЛОГИКА ХОАРАПримерПокажем, что построенный вывод в логике Хоара являетсяуспешным для стандартной арифметической интерпретацииI0 = hDI0 = {0, 1, 2, .

. . }, {+, −, ×}, <, >, =, ≥, ≤i.Для этого достаточно установить истинность в интерпретацииI0 всех формул, стоящих в листьях построенного вывода.1. I0 |= ϕ(x, y , z) → ϕ(x, y , z)Очевидно.2. I0 |= ϕ0 (x, y , z)&¬¬(x = y ) → (z = x), т. е.I0 |= (x > 0)&(y > 0)&(x = y )&GCD(x, y , z) → (z = x).Верно.ЛОГИКА ХОАРАПример3. I0 |= ϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z), т. е.I0 |= (x > 0)&(y > 0)&(x > y )&GCD(x, y , z) →→ (x − y > 0)&(y > 0)&GCD(x − y , y , z).Верно.4.