Program Logics Made Easy

In spite of the importance of Formal Methods for development of a reliable hard- and software this domain is not well acquainted to non-professionals. In particular, many students consider Formal Methods either too poor for their pure mathematics, either too pure for their poor mathematics. We suppose that a deficit of a popular papers on Formal Methods is the main reason for this ignorance. In the paper we would like to present in a popular (but mathematically sound) form a Program Logics tributary creek of a powerful stream called Formal Methods. From the application viewpoint, the paper is oriented on model checking of program logics in finite models. The basic ideas, definitions and theorems are illustrated by game examples usually presented as puzzles. Only some knowledge of propositional calculus, elementary set theory and theory of binary relations is prerequested