Логика программы – предикат, истинный на значениях переменных тогда и только тогда, когда некоторое исполнение программы завершается с этими значениями. Для программ с хорошей логикой (без циклов типа while и указателей) определяется формула тотальной корректности. Теорема тождества спецификации и программы вводит более простую формулу корректности, применимую для однозначных спецификаций. Разработана система правил доказательства корректности для различных видов операторов программы. Генерация и доказательство формул корректности проводится проще, чем для верификации по методу Хоара. Правила доказательства корректности применимы также для программного синтеза.
| Файл с полным текстом: | Shelekhov_prlogic.pdf |
| Файл презентации: | Pres_Shelekhov.pdf |