Шелехов Владимир Иванович (vshel@iis.nsk.su)

Институт систем информатики им. А.П. Ершова СО РАН

Представлен метод предикатного программирования в применении к известной программе инвертирования односвязных списков. Данная программа признана крайне трудной для дедуктивной верификации (verification challenge). Описываются построение и дедуктивная верификация предикатной программы инвертирования списка как объекта алгебраического типа. Эффективная императивная программа получена применением оптимизирующих трансформаций. Дедуктивная верификация предикатной программы на порядок проще верификации аналогичной императивной программы, использующей указатели.

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