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 an 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 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.
Introduction
There are many tools for automated program verification. Many of early results in mechanical
program verification were carried out by Boyer and Moore using their theorem prover. Today,
verification uses SMT solvers [
Proving full functional correctness of a program has been and still is a great challenge for fully
automated systems, and for this purpose, usually an interactive approach is applied. Formalized mathematics
and interactive theorem provers (sometimes referred to as proof assistants) have made great progress in
recent years. Many classical mathematical theorems have been formally proved and proof assistants have
been intensively used in hardware and software verification. Theorem provers that are most commonly
used for program verification nowadays are Isabelle [
Using program verification within computer science education. Program verification is usually considered to be too hard and long process that acquires good mathematical background. A verification of a program is performed using mathematical logic. Having the specification of an algorithm inside the logic, its correctness can be proved again by using the standard mathematical apparatus (mainly induction and equational reasoning). These proofs are commonly complex and the reader must have some knowledge about mathematical logic. The reader must be familiar with notions such as satisfiability, validity, logical consequence, etc. Any misunderstanding leads into a loss of accuracy of the verification. These formalizations have a common disadvantage, they are too complex to be understood by students, and this discourages students most of the time. Therefore, programmers and their educators rather use traditional (usually trial-and-error) methods.
However, many authors claim that nowadays education lacks the formal approach and it is clear why
many advocate in using proof assistants [
Verification helps to point out what are the requirements and conditions that an algorithm satisfies (pre-conditions, post-conditions and invariant conditions) and then to apply this knowledge during programming. This would help both students and educators to better understand input and output specification and the relations between them.
Though a program might work in general, it can happen that it does not work for some inputs and students must be able to detect these situations and to create software that works properly for all inputs.
It is suitable to separate the abstract algorithm from its specific implementation. Students can compare properties of different implementations of the same algorithms, to see the benefits of one approach or another. Also, it is possible to compare different algorithms for the same purpose (for example, for searching element, sorting, etc.) and this could help in overall understanding of algorithm construction techniques. Therefore, lessons learned from formal verification of an algorithm can improve someones style of programming.
Modularity and refinement. The most used languages today are those who can easily be compiled into efficient code. Using heuristics and different data types makes code more complex and seems like a perplex mixture to novices of many new notions, definitions, concepts. These techniques and methods in programming makes programs more efficient but are rather hard to be intuitively understood. On the other hand, modularity is a highly accepted principle in nowadays programming. Adhering to this principle enables programmer to easily maintain the code.
The best way to apply modularity on program verification and to make verification flexible enough to
add new capabilities to the program keeping current verification intact is program refinement. Program
refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete
(low-level) executable program. It starts from the abstract level, describing only the requirements for
input and output. Implementation is obtained at the end of the verification process (often by means of
code generation [
It is possible to verify different implementations for some part of the program, discussing the benefits of one approach or another.
It can be easily proved that these different implementation share some same properties which are proved before splitting into two directions.
It is easy to maintain the code and the verification. Usually, whenever the implementation of the program changes, the correctness proofs must be adapted to these changes, and if refinement is used, it is not necessary to rewrite the entire verification, just add or change a small part of it. Using refinement approach makes an algorithm suitable for a case study in teaching. Properties and specifications of the program are clearly stated and it helps teachers and students better to teach or understand them.
We claim that the full potential of refinement comes only when it is applied stepwise, and in many small steps. If the program is refined in many steps, and data structures and algorithms are introduced one-by-one, then proving the correctness between the successive specifications becomes easy. Abstracting and separating each algorithmic idea and each data-structure that is used to give an efficient implementation of an algorithm is a very important task in programmer education.
As an example of using small step refinement, in this paper we analyze two widely known algorithms, Selection Sort and Heap Sort. There are many reasons why we decided to use them.
They are largely studied in different contexts and they are studied in almost all computer science curricula.
They belong to the same family of algorithms and they are good example for illustrating the refinement techniques. They are a nice example of how one can improve on a same idea by introducing more efficient underlying data-structures and more efficient algorithms.
Their implementation uses different programming constructs: loops (or recursion), arrays (or lists), trees, etc. We show how to analyze all these constructs in a formal setting.
There are many formalizations of sorting algorithms that are done both automatically or interactively and they undoubtedly proved that these algorithms are correct. In this paper we are giving a new approach in their verification, that insists on formally analyzing connections between them, instead of only proving their correctness (which has been well established many times). Our central motivation is that these connections contribute to deeper algorithm understanding much more than separate verification of each algorithm.
The paper gives a clear picture of central ideas relevant for verification by means of small step refinement. We give all definitions, but some proofs and implementations are omitted, and can be found in Isabelle/HOL formalization1. 2