Сопровождение контроля соответствия программ и моделей формальным спецификациям задач

Пустоваров В.І.

Предложены механизмы автоматизации доказательного объектно-ориентированного программирования задач по спецификациям на базе контроля семантической корректности взаимных превращений кодов программ и спецификаций. Через эти механизмы обосновано использование аналитического типа данных, который можно встроить в языков и систем программирования. Предложенный подход позволяет автоматизировать доказательные преобразование кодов и спецификаций в системах автоматизации программирования и моделирования для задач формальной верификации и синтеза кодов.


Загрузить (pdf)