Ещё одни лекции В.А. Захарова, страница 33

е.I |= ϕ{π}ψ .ЛОГИКА ХОАРАКак же доказать частичную корректность программы?Попробуем построить систему правил вывода, аналогичныхправилам вывода для семантических таблиц.Такую систему предложил в 1968 г. Хоар. Правила выводаХоара имеют видΦ,ΨΦ,ϕΦΦ,,Ψ1 , Ψ2 ϕ, Ψ, ψгде Φ, Ψ, Ψ1 , Ψ2 — триплеты Хоара,ϕ, ψ — формулы логики предикатов.ЛОГИКА ХОАРАПравила вывода ХоараASS:ϕ{x/t} {x ⇐ t} ϕ,trueCONS:ϕ{π}ψ,ϕ → ϕ , ϕ {π}ψ , ψ → ψ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@@R y@@@@?Ry@yy?y?yyЛОГИКА ХОАРАОпределение вывода в логике ХоараВывод в логике Хоара триплета Φ0 = ϕ0 {π0 } ψ0 — этокорневое дерево, вершинами которого служат триплеты иформулы логики предикатов и при этомΦyjyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12?ϕy3?yϕ4ΦyiЛОГИКА ХОАРАОпределение вывода в логике ХоараВывод в логике Хоара триплета Φ0 = ϕ0 {π0 } ψ0 — этокорневое дерево, вершинами которого служат триплеты иформулы логики предикатов и при этом1) корнем дерева является триплет Φ0 ;ΦyjyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12?ϕy3?yϕ4ΦyiЛОГИКА ХОАРАОпределение вывода в логике Хоара2)из вершины Φi исходят дуги в вершину Φj⇐⇒Φi — правило табличного вывода;ΦjΦyiΦyj?ϕ3yyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12yϕ4?ЛОГИКА ХОАРАОпределение вывода в логике Хоара2)из вершины Φi исходят дуги в вершину Φj⇐⇒Φi — правило табличного вывода;ΦjΦyiΦyj?ϕ3yyΦ0@@@R yΦ@1@@@?ϕR yϕyyΦ3 @12yϕ4?ЛОГИКА ХОАРАОпределение вывода в логике Хоара2)из вершины Φ1 исходят дуги в вершины ϕ1 , Φ3 , ϕ2⇐⇒Φ1— правило табличного вывода;ϕ1 , Φ3 , ϕ2ΦyiΦyj?yϕ3yΦ0@@@R y@Φ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 yϕ0 (x,y ,z)PPPPPP)yϕ0 (x, y , z) → ϕ0 (x, y , z)PqPyϕ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) PPPPPPqPyyϕ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))yPPyPPϕ0 (x, y , z)&¬(x = y )&(x > y ) →→ ϕ0 (x − y , y , z)PPPqPyϕ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)PPy)yϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z)PPPPPqPyϕ0 (x, y , z) → ϕ0 (x, y , z)?yϕ0 (x, y − x, z){y ⇐ y −x}ϕ0 (x, y , z)ASS?ytrueЛОГИКА ХОАРАПримерПокажем, что построенный вывод в логике Хоара являетсяуспешным для стандартной арифметической интерпретацииI0 = DI0 = {0, 1, 2, .

. . }, {+, −, ×}, <, >, =, ≥, ≤.Для этого достаточно установить истинность в интерпретации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.

I0 |= ϕ0 (x, y , z)&¬(x = y )&¬(x > y ) →→ ϕ0 (x, y − x, z), т. е.I0 |= (x > 0)&(y > 0)&(y > x)&GCD(x, y , z) →→ (x > 0)&(y − x > 0)&GCD(x, y − x, z).Верно.5. I0 |= true.Очевидно.Таким образом, все листовые формулы вывода истинны винтерпретации I0 . Значит, вывод триплета ϕ0 {π0 } ψ0 являетсяуспешным выводом в интерпретации I0 .ЛОГИКА ХОАРАТеорема корректностиДля любой интерпретации I и для любого правила выводалогики ХоараΦ,ΨΦ,ϕесли I |= Ψ,I |= ϕ,то I |= Φ.Φ,Ψ1 , Ψ2I |= Ψ1 ,I |= Ψ2 ,Φ,ϕ, Ψ, ψ⎧⎨ I |= ϕ,I |= Ψ,⎩I |= ψ,Доказательство.Рассмотрим поочередно все правила вывода логики Хоара.ЛОГИКА ХОАРАДоказательство.ПравилоASS:ϕ{x/t} {x ⇐ t} ϕ.trueПокажем, что в любой интерпретации I верноI |= ϕ{x/t} {x ⇐ t} ϕ.(∗)Пусть θ — произвольная оценка переменных, и пустьI |= ϕ{x/t}θ.Тогда согласно операционной семантике императивныхпрограмм имеется единственное вычислениеx ⇐ t, θ −→I ∅, η,и при этом η = {x/t}θ.Очевидно, I |= ϕη, и это доказывает (∗).ЛОГИКА ХОАРАДоказательство.Для остальных правил доказательство корректностипроводится по той же схеме, но более изощренно.Попробуйте завершить доказательство самостоятельно.Следствие.Если триплет ϕ{π}ψ имеет успешный в интерпретации I вывод,то программа π частично корректна в интерпретации Iотносительно предусловия ϕ и постусловия ψ.В частности, это означает, что исследованная нами программавычисления наибольшего общего частично корректна варифметической интерпретации I0 .АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММКак автоматизировать верификацию программ?Для этого нужно выяснить1.

Полна ли система правил вывода логики Хоара?2. Существует ли алгоритм построения успешного вывода?АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММВопрос о полноте правил вывода Хоара.На самом деле, здесь не один а три вопроса.1. Верно ли, что для каждой интерпретации I существуетсистема правил вывода, позволяющая для каждого триплетаΦ = ϕ{π}ψ построить успешный вывод Φ в интерпретации I идоказать его успешность в случае I |= Φ?Ответ отрицательный . Следует из теоремы Геделя о неполноте.АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММВопрос о полноте правил вывода Хоара.2. Верно ли, что для каждой интерпретации I существуетсистема правил вывода, позволяющая для каждого триплетаΦ = ϕ{π}ψ построить успешный вывод Φ в интерпретации I(но не гарантирующая доказательства его успешности) вслучае I |= Φ?Ответ отрицательный .

Базовые предикаты сигнатуры σ могутбыть недостаточно выразительными для представления всехтех отношений между переменными программы, которыенужны для построения успешного вывода.В результате не найдется нужных формул ϕ , ψ дляприменения правилаϕ{π}ψCONS:.ϕ → ϕ , ϕ {π}ψ , ψ → ψАВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММВопрос о полноте правил вывода Хоара.3. Верно ли, что для некоторых интерпретаций I существуетсистема правил вывода Хоара, которая позволяет для каждоготриплета Φ = ϕ{π}ψ построить успешный вывод Φ винтерпретации I в случае I |= Φ?Ответ положительный . Достаточно, чтобы для любого циклаπ = while C do π od существовал такой терм tπ , что длялюбой оценки переменных θ значение терма tπ θ равно n + 1тогда и только тогда, когда цикл π в вычислении π, θсовершает n итераций.АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММЧто нужно для построения успешного вывода?Необходимо иметь эффективный прувер для проверкиистинности формул в разных интерпретациях:I |= ϕ ..CONS:ϕ{π}ψ,ϕ → ϕ , ϕ {π}ψ , ψ → ψпоскольку неясно, какие формулы ϕ , ψ нужно выбирать вкаждом случае.АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММСтратегия вывода в логике Хоара.ОпределениеПусть заданы интерпретация I , императивная программа π ипостусловие ψ.

Тогда формула ϕ0 называется слабейшимпредусловием (weakest postcondition) для программы π ипостусловия ψ, если I |= ϕ0 {π}ψ,1.2. для любой формулы ϕ, если I |= ϕ{π}ψ, то I |= ϕ → ϕ0 .Слабейшее предусловие для программы π и постусловия ψусловимся обозначать wpr (π, ψ).АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММКакая польза от слабейшего предусловия?ТеоремаI |= ϕ{π}ψ ⇐⇒I |= wpr (π, ψ){π}ψ,I |= ϕ → wpr (π, ψ).Таким образом, задача построения успешного вывода сводитсяк задаче вычисления wpr (π, ψ).АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММА как вычислять слабейшее предусловие?Теоремаwpr (x ⇐ t, ψ) = ψ{x/t},wpr (π1 ; π2 , ψ) = wpr (π1 , wpr (π2 , ψ)),wpr (if C then π1 else π2 fi, ψ) =C &wpr (π1 , ψ) ∨ ¬C &wpr (π2 , ψ),ДоказательствоСамостоятельно.Таким образом, для многих операторов (программ) слабейшеепредусловие вычисляется автоматически.АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММНеужели все так просто?Увы, нет.

Главную трудность представляет оператор циклаwhile C do π od. Единственный способ верифицировать этотоператор — это воспользоваться производным правилом:WHILE-GEN:ϕ {while C do π od} (ψ).ϕ → χ, (χ&C ) {π} χ, (χ&¬C ) → ψЭто правило требует введения вспомогательной формулы χ,которая называется инвариантом цикла . Инвариант циклазависит от программы π и условия C .Автоматическая генерация инвариантов цикла — это ключеваязадача в решении проблемы автоматической верификациипрограмм.КОНЕЦ ЛЕКЦИИ 20.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.