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

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

Описывается трансформация программы memweight из библиотеки ОС Linux, устраняющая указатели. Далее программа трансформируется на язык предикатного программирования P. Для предикатной программы, полученной в результате серии упрощающих трансформаций, строится спецификация и проводится дедуктивная верификация. Для упрощения верификации в рамках спецификации строится модель внутреннего состояния исполняемой программы. Верификация программы memweight реализована в системе автоматического доказательства Why3.

DOI10.31144/si.2307-6410.2020.n16.p103-136
УДК004.05
Номер № 16,
Страницы103-136
Файл tumurovshelehov.pdf (968.31 КБ)
Библиографическая ссылка
Тумуров Э.Г., Шелехов В.И. Трансформация, спецификация и верификация программы вычисления числа элементов множества, представленного в виде битовой шкалы // Системная информатика, 2020. – № 16. – С. 103-136. – DOI: https://doi.org/10.31144/si.2307-6410.2020.n16.p103-136.