APPLYING DEDUCTIVE VERIFICATION TO BACHELOR DEGREE COURSES IN PROGRAMMING

A great number of theories, algorithms, methods and techniques of formal verification can be found in the literature. They identify three main approaches: deductive verification, equivalence checking and model checking. Chronologically, deductive verification appeared first, and it is also the most suitable for the educational purposes of introductory courses in programming. By applying it, certain system properties can be proved, such as partial and total correctness, completion of the execution, etc. To this end, the system and the property are translated into formulae of first or higher order, then a theorem prover is applied to verify the property.

This article presents its authors’ experience in applying deductive verification to the following courses: Introduction to Programming, Object-Oriented Programming and Data Structures and Programming for students of specialty Informatics and Computer Sciences in two Bulgarian universities. The usefulness of training in the field is motivated. A brief introduction of the used theories, techniques and tools is presented, as well as the process of education itself. The approaches to education are also commented: through examples, project-based and e-learning. The results are analyzed.