Abstract:

The article presents the applying formal program verification methods during the first years of programming education, specialty Computer Science at Sofia University. What is described are the main stages of education which includes training in verification of: procedural programming (as part of the course Introduction to Programming); object-oriented programs (as part of the course Object-Oriented Programming) and abstract data types (as part of the course Data Structures and Programming). The goals, approaches used and verification tools are given for all stages of education. The results are analyzed and presented.
Education on the subject is based on axiomatic semantics and uses the techniques of design by contract, class invariant, proving theorems and consistency check. Particular attention is paid to a specially developed, for educational purposes, approach for verification of procedural and object-oriented programs, based on generalized nets (structures similar to Petri’s nets). The approach executes separated verification of the functions and procedural program which uses them. It also performs separated verification of the classes and the object-oriented program which executes their member functions. The verification of the functions and member functions of the classes is performed through formulating and proving theorems via the HOL theorem proving system. Applying the “design by contract” concept, specifications are developed to describe the relations between procedural programs functions, or between member functions of the classes of the object oriented programs, in a form of sequences of correct calls. The consistency check is done by designing and parallel executing of generalized net models of the specifications and of the programs to be verified.

Keywords:

Programming, Object-Oriented Programming, Data structures, Verification, Formal Verification Methods, Generalized nets, Modeling, Education.