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

0 коммент.

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

Похожие записи

Добавить комментарий