Трансформация, спецификация и верификация программы вычисления числа элементов множества, представленного в виде битовой шкалы

Трансформация, спецификация и верификация программы вычисления числа элементов множества, представленного в виде битовой шкалы

Язык статьи
Русский
Аннотация
Описывается трансформация программы memweight из библиотеки ОС Linux, устраняющая указатели. Далее программа трансформируется на язык предикатного программирования P. Для предикатной программы, полученной в результате серии упрощающих трансформаций, строится спецификация и проводится дедуктивная верификация. Для упрощения верификации в рамках спецификации строится модель внутреннего состояния исполняемой программы. Верификация программы memweight реализована в системе автоматического доказательства Why3.
УДК
Страницы
103-136
Файл
Номер