A comparative study of insertion sorting algorithm verification

Autor:	Dongchen Jiang, Miao Zhou
Rok vydání:	2017
Předmět:	Insertion sort Sorting algorithm Correctness Index (economics) Computer science Formal specification Data_FILES Arithmetic Value (mathematics)
Zdroj:	2017 IEEE 2nd Information Technology, Networking, Electronic and Automation Control Conference (ITNEC).
DOI:	10.1109/itnec.2017.8284998
Popis:	Focusing on the impact different ways of formalization have on the according verifications of sorting algorithm, this paper presents the formal specifications of insertion sort, and verifies its functional correctness using Isabelle/HOL. For the formalization, the value-based method and the index-based method are compared, which turns out that the index-based method is more suitable for verification in various aspects.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::10b266ffdd4102136ef136664e4f7e87 https://doi.org/10.1109/itnec.2017.8284998 Zobrazit plný text záznamu