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

Verification of a predicate heapsort program using inverse transformations

Article's language
Russian
Abstract
Deductive verification of the classical J.Williams heapsort algorithm for objects of an arbitrary type was conducted. In order to simplify verification, non-trivial transformations, replacing pointer arithmetic operators by an array element constructs, were applied. The program was translated to the predicate programming language. Deductive verification of the program in the tools Why3 and Coq appears to be complicated and time consuming.
UDK
Pages
75-102
File
shelekhov.pdf979.56 KB
Number