DEDUCTIVE VERIFICATION AND OPTIMIZATION OF THE PREDICATE PROGRAM FOR STRING CONCATENATION
Shelekhov Vladimir · System Informatics · 2018
System Informatics (Системная информатика), No. 12 (2018) 61 УДК 004.05 Дедуктивная верификация и оптимизация предикатной программы конкатенации строк Шелехов В.И.(Институт систем информатики СО РАН, Новосибирский государственный университет) Дедуктивная верификация намного проще и быстрее для предикатных программ, чем для аналогичных императивных программ.Для любой программы на языке Си можно построить эквивалентную предикатную программу, провести её дедуктивную верификацию, применить к ней набор оптимизирующих трансформаций и в результате получить исходную программу на языке Си.Данный метод иллюстрируется для известной библиотечной программы конкатенации строк strcat.Описывается построение, дедуктивная верификация и оптимизирующая трансформация предикатной программы конкатенации строк как объектов алгебраического типа «список» в языке предикатного программирования.Разработан аппарат сканирования списков и новый метод кодирования списков через массивы.Анализируется возможность применения технологии предикатного программирования для дедуктивной верификации программ на языке Си.