Abstract
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 analyze similar algorithms and to compare their properties
within a single formalization. Usually, formal analysis is not done
in 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 correctness proof, but also better
understanding of an algorithm. If the verification is based on 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 proof assistant Isabelle/HOL and program refinement
techniques.