Презентация 16 (Лекции), страница 2

строго описать требования, предъявляемые к программеФормальная верификация“Любая нетривиальная программасодержит хотя бы одну ошибку”автор неизвестенПравильная программа ошибок не содержитА как проверить, что программа не содержит ошибок?Программа без ошибок работает в точности так, как от неётребуетсяА как убедиться, что программа делает в точности то, что отнеё требуется?Для этого надо:1. строго описать требования, предъявляемые к программе2. проверить соблюдение этих требований для всехвычислений программыФормальная верификацияТребования к вычислениям программы, записанные накаком-либо формальном языке, — это формальнаяспецификация программыФормальная верификацияТребования к вычислениям программы, записанные накаком-либо формальном языке, — это формальнаяспецификация программыПроверка соблюдения этих требований с помощью формальныхметодов — это формальная верификацияФормальная верификацияТребования к вычислениям программы, записанные накаком-либо формальном языке, — это формальнаяспецификация программыПроверка соблюдения этих требований с помощью формальныхметодов — это формальная верификацияЕсли в качестве языка спецификации программ выбратькакой-либо логический язык, то для проверки правильностипрограммы можно будет использовать логические методыФормальная верификацияТребования к вычислениям программы, записанные накаком-либо формальном языке, — это формальнаяспецификация программыПроверка соблюдения этих требований с помощью формальныхметодов — это формальная верификацияЕсли в качестве языка спецификации программ выбратькакой-либо логический язык, то для проверки правильностипрограммы можно будет использовать логические методыПопробуем описать такие язык и метод для императивныхпрограммИмперативные программыНачнём с формальных синтаксиса и семантики императивныхпрограммИмперативные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовИмперативные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовПрисваивание имеет вид x ⇐ t(x ∈ Var, t ∈ Term)Императивные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовПрисваивание имеет вид x ⇐ tУсловие — это формула без кванторов(x ∈ Var, t ∈ Term)Императивные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовПрисваивание имеет вид x ⇐ tУсловие — это формула без кванторовПрограмма определяется так:(x ∈ Var, t ∈ Term)Императивные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовПрисваивание имеет вид x ⇐ tУсловие — это формула без кванторовПрограмма определяется так:I∅ — это пустая программа(x ∈ Var, t ∈ Term)Императивные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовПрисваивание имеет вид x ⇐ tУсловие — это формула без кванторовПрограмма определяется так:II∅ — это пустая программаприсваивание — это программа(x ∈ Var, t ∈ Term)Императивные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовПрисваивание имеет вид x ⇐ t(x ∈ Var, t ∈ Term)Условие — это формула без кванторовПрограмма определяется так:III∅ — это пустая программаприсваивание — это программаπ1 ; π2 — это программа(π1 , π2 — программы)Императивные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовПрисваивание имеет вид x ⇐ t(x ∈ Var, t ∈ Term)Условие — это формула без кванторовПрограмма определяется так:IIII∅ — это пустая программаприсваивание — это программаπ1 ; π2 — это программа(π1 , π2 — программы)if C then π1 else π2 fi — это программа(C — условие)Императивные программыНачнём с формальных синтаксиса и семантики императивныхпрограммСинтаксис императивных программБудем отталкиваться от сигнатуры (Const, Func, Pred) логикипредикатовПрисваивание имеет вид x ⇐ t(x ∈ Var, t ∈ Term)Условие — это формула без кванторовПрограмма определяется так:IIIII∅ — это пустая программаприсваивание — это программаπ1 ; π2 — это программа(π1 , π2 — программы)if C then π1 else π2 fi — это программа(C — условие)while C do π od — это программаИмперативные программыОперационная семантика императивных программЗначение программы — это вычисляемая ей функцияпреобразования входных данных в выходные данныеИмперативные программыОперационная семантика императивных программЗначение программы — это вычисляемая ей функцияпреобразования входных данных в выходные данныеВычисление этой функции состоит в изменении текущегосостояния данных и смене состояний управленияпрограммыИмперативные программыОперационная семантика императивных программЗначение программы — это вычисляемая ей функцияпреобразования входных данных в выходные данныеВычисление этой функции состоит в изменении текущегосостояния данных и смене состояний управленияпрограммыСостояние управления — это любая программаИмперативные программыОперационная семантика императивных программЗначение программы — это вычисляемая ей функцияпреобразования входных данных в выходные данныеВычисление этой функции состоит в изменении текущегосостояния данных и смене состояний управленияпрограммыСостояние управления — это любая программаСостояние данных — это подстановка(оценка данных)θ : Var → GTerm(GTerm — множество всех основных термов)Императивные программыОперационная семантика императивных программЗначение программы — это вычисляемая ей функцияпреобразования входных данных в выходные данныеВычисление этой функции состоит в изменении текущегосостояния данных и смене состояний управленияпрограммыСостояние управления — это любая программаСостояние данных — это подстановка(оценка данных)θ : Var → GTerm(GTerm — множество всех основных термов)Состояние вычисления — это пара hπ, θi, где π — состояниеуправления, а θ — состояние данныхИмперативные программыОперационная семантика императивных программЗначение программы — это вычисляемая ей функцияпреобразования входных данных в выходные данныеВычисление этой функции состоит в изменении текущегосостояния данных и смене состояний управленияпрограммыСостояние управления — это любая программаСостояние данных — это подстановка(оценка данных)θ : Var → GTerm(GTerm — множество всех основных термов)Состояние вычисления — это пара hπ, θi, где π — состояниеуправления, а θ — состояние данныхState — множество всех состояний вычисленияИмперативные программыОперационная семантика императивных программРабота программы π в интерпретации I описывается отношениемпереходов →I на множестве State:Императивные программыОперационная семантика императивных программРабота программы π в интерпретации I описывается отношениемпереходов →I на множестве State:Ihx ⇐ t, θi →I h∅, {x/t} θiИмперативные программыОперационная семантика императивных программРабота программы π в интерпретации I описывается отношениемпереходов →I на множестве State:Ihx ⇐ t, θi →I h∅, {x/t} θiIhif C then π1 else π2 fi, θi →I hπ1 , θi(I |= C θ)Императивные программыОперационная семантика императивных программРабота программы π в интерпретации I описывается отношениемпереходов →I на множестве State:Ihx ⇐ t, θi →I h∅, {x/t} θiIhif C then π1 else π2 fi, θi →I hπ1 , θi(I |= C θ)Ihif C then π1 else π2 fi, θi →I hπ2 , θi(I 6|= C θ)Императивные программыОперационная семантика императивных программРабота программы π в интерпретации I описывается отношениемпереходов →I на множестве State:Ihx ⇐ t, θi →I h∅, {x/t} θiIhif C then π1 else π2 fi, θi →I hπ1 , θi(I |= C θ)Ihif C then π1 else π2 fi, θi →I hπ2 , θi(I 6|= C θ)Ihwhile C do π od, θi →I hπ; while C do π od, θi (I |= C θ)Императивные программыОперационная семантика императивных программРабота программы π в интерпретации I описывается отношениемпереходов →I на множестве State:Ihx ⇐ t, θi →I h∅, {x/t} θiIhif C then π1 else π2 fi, θi →I hπ1 , θi(I |= C θ)Ihif C then π1 else π2 fi, θi →I hπ2 , θi(I 6|= C θ)Ihwhile C do π od, θi →I hπ; while C do π od, θi (I |= C θ)Ihwhile C do π od, θi →I h∅, θi(I 6|= C θ)Императивные программыОперационная семантика императивных программРабота программы π в интерпретации I описывается отношениемпереходов →I на множестве State:Ihx ⇐ t, θi →I h∅, {x/t} θiIhif C then π1 else π2 fi, θi →I hπ1 , θi(I |= C θ)Ihif C then π1 else π2 fi, θi →I hπ2 , θi(I 6|= C θ)Ihwhile C do π od, θi →I hπ; while C do π od, θi (I |= C θ)Ihwhile C do π od, θi →I h∅, θiIhπ1 ; π2 , θi →I hπ10 ; π2 , ηi(I 6|= C θ)(hπ1 , θi →I hπ10 , ηi)Императивные программыОперационная семантика императивных программРабота программы π в интерпретации I описывается отношениемпереходов →I на множестве State:Ihx ⇐ t, θi →I h∅, {x/t} θiIhif C then π1 else π2 fi, θi →I hπ1 , θi(I |= C θ)Ihif C then π1 else π2 fi, θi →I hπ2 , θi(I 6|= C θ)Ihwhile C do π od, θi →I hπ; while C do π od, θi (I |= C θ)Ihwhile C do π od, θi →I h∅, θiIhπ1 ; π2 , θi →I hπ10 ; π2 , ηiIh∅; π, θi →I hπ, θi(I 6|= C θ)(hπ1 , θi →I hπ10 , ηi)Императивные программыОперационная семантика императивных программТрасса программы π на оценке θ в интерпретации I — этопоследовательность состояний вычисления видаhπ, θi →I hπ1 , θ1 i →I hπ2 , θ2 i →I .

. .Императивные программыОперационная семантика императивных программТрасса программы π на оценке θ в интерпретации I — этопоследовательность состояний вычисления видаhπ, θi →I hπ1 , θ1 i →I hπ2 , θ2 i →I . . .Вычисление программы π на оценке θ в интерпретации I — этомаксимальная по длине трасса π на θ в IИмперативные программыОперационная семантика императивных программТрасса программы π на оценке θ в интерпретации I — этопоследовательность состояний вычисления видаhπ, θi →I hπ1 , θ1 i →I hπ2 , θ2 i →I .