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

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