Верификация предикатной программы пирамидальной сортировки с применением обратных трансформаций

Проводится дедуктивная верификация алгоритма классической пирамидальной сортировки Дж. Вильямса, реализованного программой sort на языке Си в библиотеке ОС Linux. Сортировка реализуется для объектов произвольного типа. Чтобы упростить верификацию, применяются нетривиальные трансформации, заменяющие арифметические операции с указателями явными элементами сортируемого массива. Программа преобразуется на язык предикатного программирования. Конструируются спецификации предикатной программы. Дедуктивная верификация в системах Why3 и Coq оказалась сложной и трудоемкой.