Метод формальной верификации программ для виртуальной лаборатории «Машина Поста»

Abstract

Introduction: The symbolic method of formal program verification is an effective way to evaluate students’ practical skills automatically, especially for tasks with an unsolvable set of correct answers, which significantly simplifies the development of evaluation software. Purpose: Developing a new method of formal program verification using symbolic evaluation approach for the programs written for Post Machine virtual laboratory. Results: A new method of formal verification of programs written for Post Machine virtual laboratory using symbolic evaluation approach has been developed. The basic principles and examples of programs for Post Machine as well as methods for their symbolic formalization are discussed. Various tasks of running mathematical operations on numbers presented in unary code were considered, i.e. incrementation, addition, multiplication, break point, transfer to a different machine configuration, etc. The considered tasks are sufficient for the students to form basic practical skills in making algorithms. Symbolic representation of students’ answers simplifies the development of evaluation tools of the virtual laboratory, making it possible to monitor the formation of students’ practical skills automatically. A concept of embedding the presented method of formal program verification into the available online educational platforms is presented. Practical relevance: The developed method of formal verification of programs written for Post Machine is used to evaluate students’ practical skills in making algorithms. It can simplify the development of virtual laboratories by reducing the costs of forming test sets used to evaluate the students’ answers.