A dual pivot quicksort (DPQS) algorithm performs substantially better than other sorting algorithms in the Java Development Kit (JDK). Beckert B. et al. had constructed the specification of the DPQS algorithm in the JML language. It had been successfully proved correct using the deductive verification engine KeY. Predicate programming has the essential advantages against imperative programming. Deductive verification of a predicate program is approximately 4 times faster than deductive verification of the analogous imperative program. Application of the special optimizing transformations to a predicate program results in the equivalent effective imperative program compared in efficiency with manually programmed. In the current paper, the construction and deductive verification of the DPQS predicate program using the interactive prover PVS is described. Deductive verification of the DPQS predicate program has been made within a week. An effective Java program has been obtained by applying program transformations to the DPQS predicate program. It's comparison with the DPQS algorithm in the JDK is in our plans.
|Журнал||CEUR Workshop Proceedings|
|Состояние||Опубликовано - 1 янв 2018|
|Событие||20th Conference Scientific Services and Internet, SSI 2018 - Novorossiysk-Abrau, Российская Федерация|
Продолжительность: 17 сен 2018 → 22 сен 2018