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

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

Язык статьи
Русский
Аннотация
Проводится дедуктивная верификация алгоритма классической пирамидальной сортировки Дж. Вильямса, реализованного программой sort на языке Си в библиотеке ОС Linux. Сортировка реализуется для объектов произвольного типа. Чтобы упростить верификацию, применяются нетривиальные трансформации, заменяющие арифметические операции с указателями явными элементами сортируемого массива. Программа преобразуется на язык предикатного программирования. Конструируются спецификации предикатной программы. Дедуктивная верификация в системах Why3 и Coq оказалась сложной и трудоемкой.
УДК
Страницы
75-102
Файл
shelekhov.pdf979.56 КБ
Номер