Лаборатория языковых инструментов

Аннотация: Темой доклада является дедуктивный подход к синтезу императивных программ с указателями по декларативной спецификации, выраженной в логике разделения (расширении логики Хоара). Декларативная спецификация представляет из себя пару утверждений - предусловие и постусловие - которые описывают состояния кучи до и после исполнения синтезируемой программы.

В ходе доклада мы обсудим систему синтеза императивных программ, представленную в виде набора правил вывода, а также рассмотрим несколько вопросов реализации этой системы.

Докладчик: Петр Лозов