Исследовательская группа
Лаборатория языковых инструментов
Синтез императивных программ, использующих кучу
September 30
Аннотация: Темой доклада является дедуктивный подход к синтезу императивных программ с указателями по декларативной спецификации, выраженной в логике разделения (расширении логики Хоара). Декларативная спецификация представляет из себя пару утверждений - предусловие и постусловие - которые описывают состояния кучи до и после исполнения синтезируемой программы.
В ходе доклада мы обсудим систему синтеза
императивных программ, представленную в виде набора правил вывода, а
также рассмотрим несколько вопросов реализации этой системы.
Докладчик: Петр Лозов