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

. .Вычисление программы π на оценке θ в интерпретации I — этомаксимальная по длине трасса π на θ в IРезультат конечного вычисления программы π на оценке θ винтерпретации I — это оценка последней пары этого вычисленияИмперативные программыОперационная семантика императивных программТрасса программы π на оценке θ в интерпретации I — этопоследовательность состояний вычисления видаhπ, θi →I hπ1 , θ1 i →I hπ2 , θ2 i →I . . .Вычисление программы π на оценке θ в интерпретации I — этомаксимальная по длине трасса π на θ в IРезультат конечного вычисления программы π на оценке θ винтерпретации I — это оценка последней пары этого вычисленияИными словами, если hπ, θi →∗I h∅, ηi, то η — результатвычисления π на θ в I(→∗I — транзитивное замыкание отношения →I )Императивные программыПримерПусть: π: while x > 0 do x ⇐ x − 1 od;θ = {x/1};I — “естественная” арифметическая интерпретацияИмперативные программыПримерПусть: π: while x > 0 do x ⇐ x − 1 od;θ = {x/1};I — “естественная” арифметическая интерпретацияТогда вычисление π на θ в I выглядит так:hwhile x > 0 do x ⇐ x − 1 od, {x/1}iПояснение:Императивные программыПримерПусть: π: while x > 0 do x ⇐ x − 1 od;θ = {x/1};I — “естественная” арифметическая интерпретацияТогда вычисление π на θ в I выглядит так:hwhile x > 0 do x ⇐ x − 1 od, {x/1}iIhx ⇐ x − 1; while x > 0 do x ⇐ x − 1 od, {x/1}iПояснение:(x > 0) {x/1} = (1 > 0)I |= (1 > 0)Императивные программыПримерПусть: π: while x > 0 do x ⇐ x − 1 od;θ = {x/1};I — “естественная” арифметическая интерпретацияТогда вычисление π на θ в I выглядит так:hwhile x > 0 do x ⇐ x − 1 od, {x/1}iIhx ⇐ x − 1; while x > 0 do x ⇐ x − 1 od, {x/1}iIh∅; while x > 0 do x ⇐ x − 1 od, {x/1 − 1}iПояснение:{x/x − 1} {x/1} = {x/1 − 1}Императивные программыПримерПусть: π: while x > 0 do x ⇐ x − 1 od;θ = {x/1};I — “естественная” арифметическая интерпретацияТогда вычисление π на θ в I выглядит так:hwhile x > 0 do x ⇐ x − 1 od, {x/1}iIhx ⇐ x − 1; while x > 0 do x ⇐ x − 1 od, {x/1}iIh∅; while x > 0 do x ⇐ x − 1 od, {x/1 − 1}iIhwhile x > 0 do x ⇐ x − 1 od, {x/1 − 1}iПояснение:Императивные программыПримерПусть: π: while x > 0 do x ⇐ x − 1 od;θ = {x/1};I — “естественная” арифметическая интерпретацияТогда вычисление π на θ в I выглядит так:hwhile x > 0 do x ⇐ x − 1 od, {x/1}iIhx ⇐ x − 1; while x > 0 do x ⇐ x − 1 od, {x/1}iIh∅; while x > 0 do x ⇐ x − 1 od, {x/1 − 1}iIhwhile x > 0 do x ⇐ x − 1 od, {x/1 − 1}iIh∅, {x/1 − 1}iПояснение:(x > 0) {x/1 − 1} = (1 − 1 > 0)I 6|= (1 − 1 > 0)Императивные программыПримерПусть: π: while x > 0 do x ⇐ x − 1 od;θ = {x/1};I — “естественная” арифметическая интерпретацияТогда вычисление π на θ в I выглядит так:hwhile x > 0 do x ⇐ x − 1 od, {x/1}iIhx ⇐ x − 1; while x > 0 do x ⇐ x − 1 od, {x/1}iIh∅; while x > 0 do x ⇐ x − 1 od, {x/1 − 1}iIhwhile x > 0 do x ⇐ x − 1 od, {x/1 − 1}iIh∅, {x/1 − 1}iПояснение:{x/1 − 1} — результат вычисленияЗадача верификации программА как определить, правильно ли работает программа?Задача верификации программА как определить, правильно ли работает программа?Неформально:Программа частично корректна, если для любых начальныхданных,удовлетворяющихзаданномупредусловиюϕ,её вычисление либо бесконечно, либо имеет результат,удовлетворяющий заданному постусловию ψЗадача верификации программА как определить, правильно ли работает программа?Неформально:Программа частично корректна, если для любых начальныхданных,удовлетворяющихзаданномупредусловиюϕ,её вычисление либо бесконечно, либо имеет результат,удовлетворяющий заданному постусловию ψПрограмма корректна, еслиIIона частично корректналюбое её вычисление на начальных данных,удовлетворяющих предусловию ϕ, конечноЗадача верификации программА как определить, правильно ли работает программа?Неформально:Программа частично корректна, если для любых начальныхданных,удовлетворяющихзаданномупредусловиюϕ,её вычисление либо бесконечно, либо имеет результат,удовлетворяющий заданному постусловию ψПрограмма корректна, еслиIIона частично корректналюбое её вычисление на начальных данных,удовлетворяющих предусловию ϕ, конечноЗадача верификации императивных программ состоит впроверке корректности или частичной корректности программыотносительно заданных предусловия и постусловияЗадача верификации программА как определить, правильно ли работает программа?Формально:Предусловие ϕ и постусловие ψ — это формулы логикипредикатов, а π — императивная программаЗадача верификации программА как определить, правильно ли работает программа?Формально:Предусловие ϕ и постусловие ψ — это формулы логикипредикатов, а π — императивная программаТребование корректности π относительно ϕ, ψ записывается ввиде триплета Хоара (или тройки Хоара):{ϕ} π {ψ}Задача верификации программА как определить, правильно ли работает программа?Формально:Предусловие ϕ и постусловие ψ — это формулы логикипредикатов, а π — императивная программаТребование корректности π относительно ϕ, ψ записывается ввиде триплета Хоара (или тройки Хоара):{ϕ} π {ψ}Триплет Хоара {ϕ} π {ψ} выполним в интерпретации I{ϕ} π {ψ}), если для любых оценок θ, η верно:если I |= ϕ и hπ, θi →∗I h∅, ηi, то I |= ψη(I |=Задача верификации программА как определить, правильно ли работает программа?Формально:Предусловие ϕ и постусловие ψ — это формулы логикипредикатов, а π — императивная программаТребование корректности π относительно ϕ, ψ записывается ввиде триплета Хоара (или тройки Хоара):{ϕ} π {ψ}Триплет Хоара {ϕ} π {ψ} выполним в интерпретации I{ϕ} π {ψ}), если для любых оценок θ, η верно:если I |= ϕ и hπ, θi →∗I h∅, ηi, то I |= ψη(I |=Программа π частично корректна в интерпретацииотносительно предусловия ϕ и постусловия ψ, еслиI |= {ϕ} π {ψ}IЗадача верификации программКак же доказать частичную корректность программы?Задача верификации программКак же доказать частичную корректность программы?Можно придумать систему правил вывода, аналогичнуюправилам табличного вывода для логики предикатовЗадача верификации программКак же доказать частичную корректность программы?Можно придумать систему правил вывода, аналогичнуюправилам табличного вывода для логики предикатовПравила такой системы1 могут иметь следующий вид:ΦΦΦΦ,,,Ψ1ϕΨ1 , Ψ2ϕ, Ψ1 , ψ(ϕ, ψ ∈ Form; Φ, Ψ1 , Ψ2 — триплеты Хоара)1Хоар, 1968Задача верификации программКак же доказать частичную корректность программы?Можно придумать систему правил вывода, аналогичнуюправилам табличного вывода для логики предикатовПравила такой системы1 могут иметь следующий вид:ΦΦΦΦ,,,Ψ1ϕΨ1 , Ψ2ϕ, Ψ1 , ψ(ϕ, ψ ∈ Form; Φ, Ψ1 , Ψ2 — триплеты Хоара)Содержательно эти правила прочитываются так:триплет Φ выполним⇔выполнимо всё, что находится под чертой в правиле1Хоар, 1968Логика ХоараВот эти правила:SKIP:{ϕ} ∅ {ϕ}trueINF:COMP:IF:WHILE:ϕ→AS:{ϕ {x/t}} x ⇐ t {ϕ}true{ϕ} π {ψ}{ψ 0 } , ψ 0 → ψϕ0 , {ϕ0 } π{ϕ} π1 ; π2 {ψ}{ϕ} π1 {χ} , {χ} π2 {ψ}{ϕ} if C then π1 else π2 fi {ψ}{ϕ&C } π1 {ψ} , {ϕ&¬C } π2 {ψ}{ϕ} while C do π od {ϕ&¬C }{ϕ&C } π {ϕ}Логика ХоараВывод триплета {ϕ} π {ψ} — это дерево следующего вида:Логика ХоараВывод триплета {ϕ} π {ψ} — это дерево следующего вида:Iвершины размечены триплетами и формуламиЛогика ХоараВывод триплета {ϕ} π {ψ} — это дерево следующего вида:IIвершины размечены триплетами и формуламикорень помечен триплетом {ϕ} π {ψ}Логика ХоараВывод триплета {ϕ} π {ψ} — это дерево следующего вида:IIIвершины размечены триплетами и формуламикорень помечен триплетом {ϕ} π {ψ}потомки вершины определяются так же, как и в дереветабличного вывода для логики предикатовЛогика ХоараВывод триплета {ϕ} π {ψ} — это дерево следующего вида:IIIIвершины размечены триплетами и формуламикорень помечен триплетом {ϕ} π {ψ}потомки вершины определяются так же, как и в дереветабличного вывода для логики предикатовлистья помечены формуламиЛогика ХоараВывод триплета {ϕ} π {ψ} — это дерево следующего вида:IIIIвершины размечены триплетами и формуламикорень помечен триплетом {ϕ} π {ψ}потомки вершины определяются так же, как и в дереветабличного вывода для логики предикатовлистья помечены формуламиУспешный вывод триплета {ϕ} π {ψ} в интерпретации I — этоконечный вывод, листья которого размечены толькоформулами, истинными в IЛогика ХоараПример: алгоритм ЭвклидаЛогика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odЛогика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odПусть эта программа работает в “естественной” арифметическойинтерпретации IЛогика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odПусть эта программа работает в “естественной” арифметическойинтерпретации IУбедимся, что в результате работы в переменную x будетзаписан наиболее общий делитель чисел x, yЛогика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odПусть эта программа работает в “естественной” арифметическойинтерпретации IУбедимся, что в результате работы в переменную x будетзаписан наиболее общий делитель чисел x, yВведём такие сокращения:Логика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odПусть эта программа работает в “естественной” арифметическойинтерпретации IУбедимся, что в результате работы в переменную x будетзаписан наиболее общий делитель чисел x, yВведём такие сокращения:div (x, z): ∃u (z · u = x)Логика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odПусть эта программа работает в “естественной” арифметическойинтерпретации IУбедимся, что в результате работы в переменную x будетзаписан наиболее общий делитель чисел x, yВведём такие сокращения:div (x, z): ∃u (z · u = x)gcd(x, y , z): div (x, z)&div (y , z)&∀u (div (x, u)&div (y , u) → (u ≤ z))Логика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odПусть эта программа работает в “естественной” арифметическойинтерпретации IУбедимся, что в результате работы в переменную x будетзаписан наиболее общий делитель чисел x, yВведём такие сокращения:div (x, z): ∃u (z · u = x)gcd(x, y , z): div (x, z)&div (y , z)&∀u (div (x, u)&div (y , u) → (u ≤ z))ϕ(x, y , z): (x > 0)&(y > 0)&gcd(x, y , z)Логика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odПусть эта программа работает в “естественной” арифметическойинтерпретации IУбедимся, что в результате работы в переменную x будетзаписан наиболее общий делитель чисел x, yВведём такие сокращения:div (x, z): ∃u (z · u = x)gcd(x, y , z): div (x, z)&div (y , z)&∀u (div (x, u)&div (y , u) → (u ≤ z))ϕ(x, y , z): (x > 0)&(y > 0)&gcd(x, y , z)ψ(x, z): x = zЛогика ХоараПример: алгоритм ЭвклидаРассмотрим такую программу π:while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi odПусть эта программа работает в “естественной” арифметическойинтерпретации IУбедимся, что в результате работы в переменную x будетзаписан наиболее общий делитель чисел x, yВведём такие сокращения:div (x, z): ∃u (z · u = x)gcd(x, y , z): div (x, z)&div (y , z)&∀u (div (x, u)&div (y , u) → (u ≤ z))ϕ(x, y , z): (x > 0)&(y > 0)&gcd(x, y , z)ψ(x, z): x = zПроверим соотношение I |= {ϕ(x, y , z)} π {ψ(x, z)}, построивуспешный вывод последнего триплетаЛогика Хоараπ: while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi od{ϕ(x, y , z)} π {ψ(x, z)}Логика Хоараπ: while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi od{ϕ(x, y , z)} π {ψ(x, z)}ϕ(x, y , z) → ϕ(x, y , z)ϕ(x, y , z)&¬(x 6= y ) → (x = z){ϕ(x, y , z)} π {ϕ(x, y , z)&¬(x 6= y )}Логика Хоараπ: while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi od{ϕ(x, y , z)} π {ψ(x, z)}ϕ(x, y , z) → ϕ(x, y , z)ϕ(x, y , z)&¬(x 6= y ) → (x = z){ϕ(x, y , z)} π {ϕ(x, y , z)&¬(x 6= y )}{ϕ(x, y , z)&(x 6= y )} if x > y then x ⇐ x − y else y ⇐ y − x fi {ϕ(x, y , z)}Логика Хоараπ: while x 6= y do if x > y then x ⇐ x − y else y ⇐ y − x fi od{ϕ(x, y , z)} π {ψ(x, z)}ϕ(x, y , z) → ϕ(x, y , z)ϕ(x, y , z)&¬(x 6= y ) → (x = z){ϕ(x, y , z)} π {ϕ(x, y , z)&¬(x 6= y )}{ϕ(x, y , z)&(x 6= y )} if x > y then x ⇐ x − y else y ⇐ y − x fi {ϕ(x, y , z)}{ϕ(x, y , z)&(x 6= y )&(x > y )} x ⇐ x − y {ϕ(x, y , z)}(∗){ϕ(x, y , z)&(x 6= y )&¬(x > y )} y ⇐ y − x {ϕ(x, y , z)}(∗∗)Логика Хоара(∗){ϕ(x, y , z)&(x 6= y )&(x > y )} x ⇐ x − y {ϕ(x, y , z)}Логика Хоара(∗){ϕ(x, y , z)&(x 6= y )&(x > y )} x ⇐ x − y {ϕ(x, y , z)}ϕ(x, y , z) → ϕ(x, y , z)ϕ(x, y , z)&(x 6= y )&(x > y ) → ϕ(x − y , y , z){ϕ(x − y , y , z)} x ⇐ x − y {ϕ(x, y , z)}Логика Хоара(∗){ϕ(x, y , z)&(x 6= y )&(x > y )} x ⇐ x − y {ϕ(x, y , z)}ϕ(x, y , z) → ϕ(x, y , z)ϕ(x, y , z)&(x 6= y )&(x > y ) → ϕ(x − y , y , z){ϕ(x − y , y , z)} x ⇐ x − y {ϕ(x, y , z)}trueЛогика Хоара(∗∗){ϕ(x, y , z)&(x 6= y )&¬(x > y )} y ⇐ y − x {ϕ(x, y , z)}Логика Хоара(∗∗){ϕ(x, y , z)&(x 6= y )&¬(x > y )} y ⇐ y − x {ϕ(x, y , z)}ϕ(x, y , z) → ϕ(x, y , z)ϕ(x, y , z)&(x 6= y )&¬(x > y ) → ϕ(x, y − x, z){ϕ(x, y − x, z)} y ⇐ y − x {ϕ(x, y , z)}Логика Хоара(∗∗){ϕ(x, y , z)&(x 6= y )&¬(x > y )} y ⇐ y − x {ϕ(x, y , z)}ϕ(x, y , z) → ϕ(x, y , z)ϕ(x, y , z)&(x 6= y )&¬(x > y ) → ϕ(x, y − x, z){ϕ(x, y − x, z)} y ⇐ y − x {ϕ(x, y , z)}trueЛогика Хоара(∗∗){ϕ(x, y , z)&(x 6= y )&¬(x > y )} y ⇐ y − x {ϕ(x, y , z)}ϕ(x, y , z) → ϕ(x, y , z)ϕ(x, y , z)&(x 6= y )&¬(x > y ) → ϕ(x, y − x, z){ϕ(x, y − x, z)} y ⇐ y − x {ϕ(x, y , z)}trueВсе формулы в листьях построенного дерева истинны ввыбранной интерпретации IЛогика ХоараТеорема корректностиДля любой интерпретации I и любого правила выводалогики ХоараΦΦΦΦ,,,Ψ1ϕΨ1 , Ψ2ϕ, Ψ1 , ψесли I |= Ψ1 , I |= Ψ2 , I |= ϕ, I |= ψ, то I |= ΦЛогика ХоараТеорема корректностиДля любой интерпретации I и любого правила выводалогики ХоараΦΦΦΦ,,,Ψ1ϕΨ1 , Ψ2ϕ, Ψ1 , ψесли I |= Ψ1 , I |= Ψ2 , I |= ϕ, I |= ψ, то I |= ΦДоказательство.Очевидно (по определению)Логика ХоараТеорема корректностиДля любой интерпретации I и любого правила выводалогики ХоараΦΦΦΦ,,,Ψ1ϕΨ1 , Ψ2ϕ, Ψ1 , ψесли I |= Ψ1 , I |= Ψ2 , I |= ϕ, I |= ψ, то I |= ΦДоказательство.Очевидно (по определению)СледствиеЕсли существует успешный вывод триплета {ϕ} π {ψ} винтерпретации I, то программа π частично корректна вI относительно предусловия ϕ и постусловия ψЛогика ХоараТеорема корректностиДля любой интерпретации I и любого правила выводалогики ХоараΦΦΦΦ,,,Ψ1ϕΨ1 , Ψ2ϕ, Ψ1 , ψесли I |= Ψ1 , I |= Ψ2 , I |= ϕ, I |= ψ, то I |= ΦДоказательство.Очевидно (по определению)СледствиеЕсли существует успешный вывод триплета {ϕ} π {ψ} винтерпретации I, то программа π частично корректна вI относительно предусловия ϕ и постусловия ψТаким образом, построив успешный табличный вывод впоследнем примере, мы доказали частичную корректностьреализации алгоритма ЭвклидаАвтоматическая проверкаправильности программА полна ли система правил логики Хоара, и можно ли с еёпомощью автоматически проверять корректность императивныхпрограмм?Автоматическая проверкаправильности программА полна ли система правил логики Хоара, и можно ли с еёпомощью автоматически проверять корректность императивныхпрограмм?Нет, и проблема возникает не однаАвтоматическая проверкаправильности программА полна ли система правил логики Хоара, и можно ли с еёпомощью автоматически проверять корректность императивныхпрограмм?Нет, и проблема возникает не однаI.