Abstract:

Increasing software’s complexity leads to augmentation of the quantity of errors in it, leading to increased losses. We can give a lot of examples of errors in the software, causing disruption of network infrastructure, destruction of a spacecraft, even human casualties, etc. This leads to high expenses for software companies to verify the correctness of the software being developed. In response to all that, and to build well-trained software professionals, there is an increase in application of formal methods in training by the universities, training software professionals.

The article presents the authors’ experience in applying of formal methods of program verification and synthesis of totally correct programmes in introduction to programming courses in some Bulgarian universities.

A brief overview of known approaches and tools for programme verification and synthesis of totally correct programs used in courses introduction to programming, object-oriented programming and data structures is presented. Education on the subject is based on axiomatic semantics. The techniques of weakest precondition, design by contract, class invariant, proving theorems and consistency check are used.

Some problems are analyzed and suggestions for improving the results of education in programming through using formal methods are discussed.

The choice of the Project Based Approach in teaching disciplines in the area is motivated.

Keywords:

Programming, Verification, Formal Verification Methods, Program Synthesis, Predicate Transformer.