THE PREDICATE TRANSFORMER AND ITS APPLICATION IN INTRODUCTION TO PROGRAMMING COURSES

Abstract

Current article is dedicated to sharing the authors’ experience in applying the predicate transformer in synthesizing (extaraction) totally correct programmes in introduction to programming courses. The training was delivered in two Bulgarian universities: Sofia University „St Kliment Ohridski” and Burgas Free University. A brief overview of known approaches to programme verification is presented, in addition some problems are analyzed and suggestions for improving the results of education in programming through using formal methods are discussed. The method for programme synthesis under discussion is based on a special function called weakest precondition. It was adapted according to the goals of education in programming based on C++. Methodologies of verification and synthesis of operators for condition and for cycle (while) are formulated. An example is used to show the application of the defined methodology, as well as the use of some techniques for defining the loop invariant. What is argued is the use of project-based approach in this education. Analysis of this approach is presented.