DOI: 10.17587/prin.12.127-139

УДК: 004.05

Методы трансформации и дедуктивной верификации программы инвертирования списков

В. И. Шелехов, канд. тех. наук, зав. лаб., vshel@iis.nsk.su, Институт систем информатики им. А. П. Ершова СО РАН, Новосибирский государственный университет

На примере программы инвертирования односвязных списков исследуются методы трансформации и дедуктивной верификации функций библиотеки ОС Linux. Исходная программа трансформируется с языка Си на язык cP без указателей. Далее программа преобразуется на язык функционального программирования WhyML. Рассмотрено три варианта дедуктивной верификации программы инвертирования односвязных списков в рамках системы автоматического доказательства Why3.

Ключевые слова: дедуктивная верификация, трансформации программ, функциональное программирование, предикатное программирование, алгебраический тип данных, односвязный список, операционная система Linux

Стр. 127–139