Лекции 12-23. Математическая логика (после колка) (1161871), страница 16
Текст из файла (страница 16)
. . , 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. 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 |= ϕ,Φ,Ψ1 , Ψ2I |= Ψ1 ,I |= Ψ2 ,Φ,ϕ, Ψ, ψ I |= ϕ,I |= Ψ,I |= ψ,то I |= Φ.Доказательство.Рассмотрим поочередно все правила вывода логики Хоара.ЛОГИКА ХОАРАДоказательство.ПравилоASS:ϕ{x/t} {x ⇐ t} ϕ.trueПокажем, что в любой интерпретации I верноI |= ϕ{x/t} {x ⇐ t} ϕ.(∗)Пусть θ — произвольная оценка переменных, и пустьI |= ϕ{x/t}θ.Тогда согласно операционной семантике императивныхпрограмм имеется единственное вычислениеhx ⇐ t, θi −→I h∅, ηi,и при этом η = {x/t}θ.Очевидно, I |= ϕη, и это доказывает (∗).ЛОГИКА ХОАРАДоказательство.Для остальных правил доказательство корректностипроводится по той же схеме, но более изощренно.Попробуйте завершить доказательство самостоятельно.Следствие.Если триплет ϕ{π}ψ имеет успешный в интерпретации I вывод,то программа π частично корректна в интерпретации Iотносительно предусловия ϕ и постусловия ψ.В частности, это означает, что исследованная нами программавычисления наибольшего общего частично корректна варифметической интерпретации I0 .АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММКак автоматизировать верификацию программ?Для этого нужно выяснить1.
Полна ли система правил вывода логики Хоара?2. Существует ли алгоритм построения успешного вывода?АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММВопрос о полноте правил вывода Хоара.На самом деле, здесь не один а три вопроса.1. Верно ли, что для каждой интерпретации I существуетсистема правил вывода, позволяющая для каждого триплетаΦ = ϕ{π}ψ построить успешный вывод Φ в интерпретации I идоказать его успешность в случае I |= Φ?Ответ отрицательный .
Следует из теоремы Геделя о неполноте.АВТОМАТИЧЕСКАЯ ПРОВЕРКАПРАВИЛЬНОСТИ ПРОГРАММВопрос о полноте правил вывода Хоара.2. Верно ли, что для каждой интерпретации I существуетсистема правил вывода, позволяющая для каждого триплетаΦ = ϕ{π}ψ построить успешный вывод Φ в интерпретации I(но не гарантирующая доказательства его успешности) вслучае I |= Φ?Ответ отрицательный .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
