Shelekhov V. Verification of a predicate heapsort program using inverse transformations // # 16, 2020
