Теормин (2006) (1162014), страница 6

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 6)

Тройкой Хоара называется формула вида {ϕ } < Π > {ψ } , где ϕ ,ψ - формулы, аП – программа, причем если на входе программы П выполняется утверждение ϕ , то на еевыходе выполняется отношение ψ . Формула ϕ называется предусловием, формула ψ постусловием.Определение.

Программа П называется частично корректной относительно предусловия ϕи постусловия ψ , если общезначима формула {ϕ } < Π > {ψ } . Эту общезначимость следуетпонимать следующим образом: для любой допустимой интерпретации I и любого наборазначений свободных переменных {α1 , α 2 ,..., α n } ∈ Varϕ ∪ Varψ из выполнимости формулы ϕ( I |= ϕ[d1 , d 2 ,..., d n ] ) будет следовать, что после завершения программы П переменныепримут значения d '1 , d '2 ,..., d 'n , причем формула ψ будет выполнима на данных значенияхпеременных ( I |= ψ [d1 , d 2 ,..., d n ] ).Определим модельный язык программирования:П ::=||||(x = t)П1, П2if A then П1 else П2 fiwhile A do П1 odeps,Где х – переменная, t – терм Пi – программы, А – атом, eps – пустота.F1 , F2 ,..., Fn, причемF0выражения в верхней части правила называются предпосылками, выражение в нижней частиправила называется заключением.

Семантика правила вывода такова: если истиннымпредпосылки, то истинно и заключения.Определение. Правилом вывода называется фигура следующего вида:Рассмотрим следующую систему правил:ϕ → ϕ '1 ,{ϕ '1} < Π > {ϕ '2 }, ϕ 2 → ϕ '2(ослабления)1. 1{ϕ1} < Π > {ϕ 2 }2.{ }ϕ →ψ x t(присваивания){ϕ} < x:= t > {ψ }{ϕ} < Π1 > {χ },{χ } < Π 2 > {ψ }3.(последовательного соединения){ϕ} < Π1 ; Π 2 > {ψ }{ϕ & A} < Π1 > {ψ },{ϕ & ¬A} < Π 2 > {ψ }4.(ветвления){ϕ & A} < if_A_then_Π1_else_Π 2 _fi > {ψ }23Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru){χ inv & A} < Π >, χ inv & ¬A → ψ , ϕ → χ inv(итерации; χ inv называется инвариантом{ϕ} < while_A_do_Π > {ψ }оператора итерации, для проверки правильности работы цикла требуется его найти)6. {ϕ} < eps > {ϕ } (аксиома)5.Система таких правил называется PVS (Prototype Verification System) и позволяет упрощатьпроверку правильности программ.4.4.

Логики знанийРассмотрим мультиагентную систему (сложную систему, принимающую решения)A1 , A2 ,..., An программ-агентов. При этом принятие решения может опираться на то, чтознают или не знают другие участники процесса принятия решений.Определение. Модальным оператором называется оператор , который выражаетотношение уверенности (необходимости).

Его семантика такова:яϕ означает «я знаю, что формула ϕ истинна».Вопрос общезначимости формулыϕ → ϕ - вопрос непротиворечивости базы знаний.яВопрос общезначимости формулы ϕ →ϕ - вопрос полноты базы знаний.я4.5. Динамическая логика (логика программ)Синтаксис динамической логики состоит из двух частей:ПрограммыФормулыA = {a1 , a2 ,..., an } - набор базовых действийP = {ϕ1 , ϕ2 ,..., ϕn } - набор базовых условий(операторов)(пропозиционных переменных)1) a ∈ A - программа;1) ϕ ∈ P - формула;2) Π1 , Π 2 - программа;2) ϕ1 & ϕ2 , ϕ1 ∨ ϕ2 , ϕ1 → ϕ2 , ¬ ϕ - формулы;3) Π1 || Π 2 - программа (|| 3) если П – программа, то [Π ]ϕ - формула.недетермированный выбор);4) (Π i ) * - программа;5) ϕ ? - программа (тест; ϕ - формула).Пример: выражение {ϕ } <if A then П1 else П2 fi > {ψ } , записанное в терминах логикиХоара, в терминах динамической логики будет выглядеть как ϕ → [( A ?, Π1 ) + (¬A ?, Π 2 )]ψ .24.

Характеристики

Список файлов ответов (шпаргалок)