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

Тогдаa ϕ означает «Агент a знает, что ϕ верно».C ϕ означает «Все агенты знают, что ϕ верно».Специальные разновидности эпистемических логикприменяются для описания и проверки требованийбезопасности сетевых протоколов.МОДАЛЬНЫЕ ЛОГИКИТемпоральные логикиТемпоральные (временные) логики применяются для описанияи исследования причинно-следственных зависимостей,развивающихся во времени.Модальный оператор означает «всегда»,а оператор ♦ — «когда-нибудь».Семантика темпоральных логик существенно зависит от тойматематической модели, которая используется для описанияфеномена времени.

В самом общем случае в качестве моделивремени можно взять любое частично упорядоченноемножество. Элементы этого множества соответствуютразличным моментам времени.В качестве темпоральных моделей могут выступать любыемодели Крипке, построенные на основе частичноупорядоченных шкал. Разные отношения частичного порядкапорождают разные темпоральные логики.МОДАЛЬНЫЕ ЛОГИКИТемпоральные логикиПоскольку вычисление — это процесс, развивающийся вовремени, состояния которого находятся впричинно-следственной связи друг с другом, темпоральныелогики используются для спецификации и верификациипрограмм. Наиболее широкое распространение получили дверазновидности темпоральных логик.Логика линейного времени LTLШкала Крипке для LTL (L inear T emporal L ogics) — этонатуральный ряд с естественным отношением порядка N, ≤.

0 y? 1 ? -2 y &? 3y6? 4y6? y6%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTL 0 y? 1 ? -2 y p, ¬qp, ¬q&? 3y6p, q? 4y6p, ¬q? yp, ¬q6%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTLI , 0 |= p,I , 0 |= q, 0 y? 1 ? -2 y p, ¬qp, ¬q&? 3y6p, qI , 0 |= ♦q? 4y6p, ¬q? yp, ¬q6%r r rМОДАЛЬНЫЕ ЛОГИКИЛогика линейного времени LTLI , 0 |= p,I , 0 |= q, 0 y? 1 ? -2 y p, ¬qp, ¬q&?3yp, q6I , 0 |= ♦q?4yp, ¬q6?yp, ¬q6%r r rПрименение LTL для верификации моделей программ болееподробно будет обсуждаться в последующих лекциях.МОДАЛЬНЫЕ ЛОГИКИТемпоральные логикиВ других темпоральных логиках время — это ветвящаясяструктура; в каждый момент времени может быть несколькоальтернатив дальнейшего развития событий.yHHHyHH?y@yHHj yH@@@@Ry@@y?y@@R y@?yy?yМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLТемпоральные логики такого вида называются логикамиветвящегося времени (BTL, Branching Time Logics).Одной из логик ветвящегося времени является логика деревьеввычислений (CTL, Computational Tree Logic), используемая дляспецификации и верификации распределенных программ имикроэлектронных схем.В логике CTL имеются темпоральные операторы двух типов —универсальные и экзистенциальные.∀,∀♦,∃,∃♦.Тип темпорального оператора указывет на то, будет ливыполнимость формулы проверяться на всех ветвях древесноймодели или только на одной ветви.МОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLПусть I = S, R, ξ — древесная модель Крипке для логикиCTL, s0 ∈ S — одно из состояний модели.

ТогдаI , s0 |= ∀ϕ ⇐⇒в каждом состоянии s, достижимом из состояния s0 , верноI , s |= ϕ;I , s0 |= ∃ϕ ⇐⇒существует ветвь, исходящая из состояния s0 , в каждомсостоянии s которой верно I , s |= ϕ;I , s0 |= ∀♦ϕ ⇐⇒в каждой ветви, исходящей из состояния s0 , есть состояние s, вкотором верно I , s |= ϕ;I , s0 |= ∃♦ϕ ⇐⇒существует ветвь, исходящая из состояния s0 , в одном изсостоянии s которой верно I , s |= ϕ.МОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∀ps0s6yp = trueHHHHHs1 HH s2p = truej yp = trueHy@@@s3 ?s4s5@Ry@p = true yp = true yp = true@@@s7 ?s8s9 ?s10s11@?R y@yyyyyp = truep = truep = truep = truep = truep = trueМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∃ps0s6yyp = trueHHHHHs1 HH s2j yp = trueHy@@@s3 ?s4s5@Ry@yp = true y@@@s7 ?s8s9 ?s10s11@?R y@yyyyp = trueМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∀♦ps0s1yHHHHHHH s2j yH@@ys3 ?p = true ys4p = true@s5@Ry@y@@s6ys7 ?y@s8@R y@s9 ?ys10yp = trues11?yp = trueМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLI , s0 |= ∃♦ps0s1yHHHHHHH s2j yH@@ys3 ?ys4@s5@Ry@y@@s6ys7 ?yp = true@s8@R y@s9 ?ys10ys11?yМОДАЛЬНЫЕ ЛОГИКИЛогика деревьев вычислений CTLФормулы CTL можно использовать для формальнойспецификации многих интересных свойств поведения программ∀ ∃♦ Restart:на любом этапе функционирования системы можноосуществить ее перезапуск;∀ (Request → ∀♦ Response):когда бы ни был послан запрос, рано или поздно на негообязательно поступит отклик.МОДАЛЬНЫЕ ЛОГИКИА как проверить,что вычисления программудовлетворяют заданным спецификациям?И можно ли эту проверкуавтоматизировать?КОНЕЦ ЛЕКЦИИ 18-19.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.

ЗахаровЛекция 20.Правильные программы.Императивные программы.Задача верификации программ.Логика Хоара.Автоматическая проверкаправильности программ.ПРАВИЛЬНЫЕ ПРОГРАММЫКакая компьютерная программа считается хорошей?Та, которая работаетПРАВИЛЬНО и эффективно .А какая программа считается правильной?Правильной считается та программа, которая выполняет вточности то, что от нее требуется.А как убедиться, что программа выполняет то, что отнее требуется?Для этого нужно1. Описать строго (формально) требования правильностивычислений;2. Проверить, что все вычисления программы удовлетворяютэтим требованиям.ПРАВИЛЬНЫЕ ПРОГРАММЫОписание требований правильности функционированияпрограммы называется спецификацией программы.Проверка соблюдения вычислениями программы требованийправильности функционирования называется верификациейпрограммы.Если спецификации программ записать на формальномлогическом языке и строго определить операционнуюсемантику программ, то для доказательства правильностипрограмм можно использовать методы математической логики(логический вывод).ПРАВИЛЬНЫЕ ПРОГРАММЫФормальная верификация программПреимуществаПроблемы1.

Абсолютно точная проверкаправильности программ.1. Как заставить программистов писать формальные спецификации?2. Возможность автоматизации построения логическоговывода.2. Как заставить прувер работать эффективно?И, тем не менее, попробуем...ИМПЕРАТИВНЫЕ ПРОГРАММЫОпределим синтаксис и семантику императивных программ.Пусть задана сигнатура σ = Const, Func, Pred, в которойопределно множество термов Term и множество атомарныхформул Atom.Условимся, что ⇐ — это служебный символ, непринадлежащий сигнатуре σ.Определениеприсваивание ::= «переменная» ⇐ «терм»условие::= «атом» | (¬условие ) |(условие & условие ) | (условие ∨ условие )программа::= присваивание |программа ; программа |if «условие» then программа else программа fi |while условие do программа odИМПЕРАТИВНЫЕ ПРОГРАММЫПримерПрограмма вычисления наибольшего общего делителя двухнатуральных чисел.Const = {0, 1, 2, .

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

. . , πn−1 , θn−1 , πn , θn , . . . ,в которой для любого n, n ≥ 1, выполняется отношениеπn−1 , θn−1 −→I πn , θn .Вычислением программы π0 на оценке переменных θ0 винтерпретации I называется всякое частичное вычисление,которое нельзя продолжить.ИМПЕРАТИВНЫЕ ПРОГРАММЫПримерПусть I — интерпретация сигнатуры σ = Const, Func, Pred: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}Примерπ0 , {x/4, y /6}↓Iif x > y then x ⇐ x − y else y ⇐ y − x fi ; π0 , {x/4, y /6}↓Iy ⇐ y − x; π0 , {x/4, y /6}↓Iπ0 , {x/4, y /6 − 4}ИМПЕРАТИВНЫЕ ПРОГРАММЫπ0 : while ¬(x = y )do if x > y then x ⇐ x − y else y ⇐ y − x fi odθ0 = {x/4, y /6}Примерπ0 , {x/4, y /6−4}↓Iif x > y then x ⇐ x − y else y ⇐ y − x fi ; π0 , {x/4, y /6−4}↓Ix ⇐ x − y ; π0 , {x/4, y /6−4}↓Iπ0 , {x/4−(6−4), y /6−4}↓I∅, {x/4−(6−4), y /6−4}ИМПЕРАТИВНЫЕ ПРОГРАММЫКак следует из определения, любое вычисление либо являетсябесконечной последовательностью, либо завершаетсясостоянием ∅, η.

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