Презентация 16 (Лекции), страница 4
Описание файла
Файл "Презентация 16" внутри архива находится в папке "Лекции". PDF-файл из архива "Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 6 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 4 страницы из PDF
Необходимо уметь проверять истинность формул логикипредикатов в заданной (обычно “естественной”арифметической) интерпретацииАвтоматическая проверкаправильности программА полна ли система правил логики Хоара, и можно ли с еёпомощью автоматически проверять корректность императивныхпрограмм?Нет, и проблема возникает не одна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.