Презентация 16 (1131941), страница 4
Текст из файла (страница 4)
Необходимо уметь проверять истинность формул логикипредикатов в заданной (обычно “естественной”арифметической) интерпретацииАвтоматическая проверкаправильности программА полна ли система правил логики Хоара, и можно ли с еёпомощью автоматически проверять корректность императивныхпрограмм?Нет, и проблема возникает не однаI. Необходимо уметь проверять истинность формул логикипредикатов в заданной (обычно “естественной”арифметической) интерпретацииУвы, этого автоматически сделать нельзя(теорема Гёделя о неполноте)Автоматическая проверкаправильности программII.
При построении вывода “из ниоткуда” возникают новыеформулыАвтоматическая проверкаправильности программII. При построении вывода “из ниоткуда” возникают новыеформулыИмеющихся в распоряжении предикатов может бытьнедостаточно для выбора подходящих формул:INF:COMP:{ϕ} π {ψ}ϕ → ϕ0 , {ϕ0 } π {ψ 0 } , ψ 0 → ψ{ϕ} π1 ; π2 {ψ}{ϕ} π1 {χ} , {χ} π2 {ψ}Автоматическая проверкаправильности программII. При построении вывода “из ниоткуда” возникают новыеформулыИмеющихся в распоряжении предикатов может бытьнедостаточно для выбора подходящих формул:INF:COMP:{ϕ} π {ψ}ϕ → ϕ0 , {ϕ0 } π {ψ 0 } , ψ 0 → ψ{ϕ} π1 ; π2 {ψ}{ϕ} π1 {χ} , {χ} π2 {ψ}Но если набор предикатов подобран удачно, то для программбез циклов можно описать алгоритм построения“оптимальных” формулАвтоматическая проверкаправильности программII. При построении вывода “из ниоткуда” возникают новыеформулыИмеющихся в распоряжении предикатов может бытьнедостаточно для выбора подходящих формул:INF:COMP:{ϕ} π {ψ}ϕ → ϕ0 , {ϕ0 } π {ψ 0 } , ψ 0 → ψ{ϕ} π1 ; π2 {ψ}{ϕ} π1 {χ} , {χ} π2 {ψ}Но если набор предикатов подобран удачно, то для программбез циклов можно описать алгоритм построения“оптимальных” формул(слабейшее предусловие и сильнейшее постусловие)(weakest precondition, strongest postcondition)Автоматическая проверкаправильности программIII.
Даже если найдены алгоритмы построения слабейшегопредусловия и сильнейшего постусловия, остаётся трудностьобработки оператора цикла: while C do π odАвтоматическая проверкаправильности программIII. Даже если найдены алгоритмы построения слабейшегопредусловия и сильнейшего постусловия, остаётся трудностьобработки оператора цикла: while C do π odЕдинственное правило, позволяющее верифицировать этотоператор:WHILE:{ϕ} while C do π od {ϕ&¬C }{ϕ&C } π {ϕ}Автоматическая проверкаправильности программIII. Даже если найдены алгоритмы построения слабейшегопредусловия и сильнейшего постусловия, остаётся трудностьобработки оператора цикла: while C do π odЕдинственное правило, позволяющее верифицировать этотоператор:WHILE:{ϕ} while C do π od {ϕ&¬C }{ϕ&C } π {ϕ}Для применения этого правила требуется предварительно найтиподходящую формулу ϕ — инвариант циклаАвтоматическая проверкаправильности программIII.
Даже если найдены алгоритмы построения слабейшегопредусловия и сильнейшего постусловия, остаётся трудностьобработки оператора цикла: while C do π odЕдинственное правило, позволяющее верифицировать этотоператор:WHILE:{ϕ} while C do π od {ϕ&¬C }{ϕ&C } π {ϕ}Для применения этого правила требуется предварительно найтиподходящую формулу ϕ — инвариант циклаОбычно основная трудность автоматической верификациипрограмм — это генерация инварианта циклаКонец лекции 16.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
