NotesFAQContact Us
Search Tips
Peer reviewed Peer reviewed
Direct linkDirect link
ERIC Number: EJ1088262
Record Type: Journal
Publication Date: 2015
Pages: 8
Abstractor: As Provided
ISSN: ISSN-1744-2710
Using Small-Step Refinement for Algorithm Verification in Computer Science Education
Simic, Danijela
International Journal for Technology in Mathematics Education, v22 n4 p155-162 2015
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.
Research Information Ltd. Grenville Court, Britwell Road, Burnham, Buckinghamshire, SL1 8DF, UK. Tel: +44-1628-600499; Fax: +44-1628-600488; e-mail:; Web site:
Publication Type: Journal Articles; Reports - Research
Education Level: N/A
Audience: N/A
Language: English
Sponsor: N/A
Authoring Institution: N/A
Grant or Contract Numbers: N/A