Верификация программы преобразования строки в целое число

Верификация программы преобразования строки в целое число
Язык статьиРусский
Аннотация

Описывается дедуктивная верификация программы kstrtoul на языке Си из библиотеки ОС Linux. Программа kstrtoul реализует вычисление целого числа, представленного в виде последовательности литер. Чтобы упростить верификацию, применяются трансформации замены операций с указателями эквивалентными действиями без указателей. Программа преобразуется на язык предикатного программирования. Конструируется модель внутреннего состояния программы как часть спецификации программы. Дедуктивная верификация проведена в системах Why3 и Coq.

DOI10.31144/si.2307-6410.2020.n17.p43-90
УДК004.05
Номер № 17,
Страницы43-90
Файл shelekhov_0.pdf (1.38 МБ)
Библиографическая ссылка
Шелехов В.И. Верификация программы преобразования строки в целое число // Системная информатика, 2020. – № 17. – С. 43-90. – DOI: https://doi.org/10.31144/si.2307-6410.2020.n17.p43-90.