Супроводження контролю відповідності програм і моделей формальним специфікаціям задач
Пустоваров В.І.
Запропоновано механізми автоматизації доказового об’єктно-орієнтованого програмування задач за специфікаціями на базі контролю семантичної коректності взаємних перетворень кодів програм та специфікацій. Через ці механізми обґрунтовано використання аналітичного типу даних, який можна вбудувати до мов і систем програмування. Запропонований підхід дозволяє автоматизувати доказові перетворення кодів і специфікацій в системах автоматизації програмування і моделювання для задач формальної верифікації та синтезу кодів.
