id: 06664342
dt: j
an: 2016f.01352
au: SimiÄ‡, Danijela
ti: Using small-step refinement for algorithm verification in computer science
education.
so: Int. J. Technol. Math. Educ. 22, No. 4, 155-162 (2015).
py: 2015
pu: Research Information Ltd, Burnham, Bucks
la: EN
cc: P20 R40
ut: computer science; verification of algorithms; correctness; proof assistant
ci:
li: http://www.researchinformation.co.uk/time/contents/timecont.php
ab: Summary: Stepwise program refinement techniques can be used to simplify
program verification. Programs are better understood since their main
properties are clearly stated, and verification of rather complex
algorithms is reduced to proving simple statements connecting
successive program specifications. Additionally, it is easy to analyse
similar algorithms and to compare their properties within a single
formalization. Usually, formal analysis is not done in the educational
setting due to complexity of verification and a lack of tools and
procedures to make comparison easy. Verification of an algorithm should
not only give a correctness proof, but also better understanding of an
algorithm. If the verification is based on a small step program
refinement, it can become simple enough to be demonstrated within the
university-level computer science curriculum. In this paper we
demonstrate this and give a formal analysis of two well- known
algorithms (Selection Sort and Heap Sort) using the proof assistant
Isabelle/HOL and program refinement techniques.
rv: