Лекция 20. Правильные программы. Императивные программы. Задача верификации программ... (1161890)

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

Текст из файла

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

Абсолютно точная проверкаправильности программ.1. Как заставить программистов писать формальные спецификации?2. Возможность автоматизации построения логическоговывода.2. Как заставить прувер работать эффективно?И, тем не менее, попробуем...ИМПЕРАТИВНЫЕ ПРОГРАММЫОпределим синтаксис и семантику императивных программ.Пусть задана сигнатура σ = hConst, Func, Predi, в которойопределно множество термов 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 > 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, .

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

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций