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

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

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


Завантажити (pdf)