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

Аннотация

Введение: формальная верификация программ в символьном виде позволяет в автоматическом режиме осуществлять оценку практических навыков обучающихся при наличии неразрешимого множества верных ответов, что существенно облегчает разработку программных компонентов, используемых для оценки. Цель: разработка нового метода формальной верификации программ в символьном виде для виртуальной лаборатории «Машина Поста». Результаты: разработан новый метод формальной верификации программ в символьном виде для виртуальной лаборатории «Машина Поста». Сформулированы основные принципы и примеры формирования программ для машины Поста и методы их символьной формализации. Рассмотрены различные задачи использования математических операций с представленными на ленте машины числами в унарном коде, в частности: прибавление единицы к числу, сложение и умножение двух чисел, остановка работы программы в определенной конфигурации ленты машины, переход к новой конфигурации машины от первоначально заданной. Рассмотренных задач достаточно для формирования у обучающихся базовых практических навыков алгоритмизации, а символьное представление решения таких задач позволит упростить разработку оценивающих средств виртуальной лаборатории «Машина Поста» и осуществлять контроль формирования данных навыков в автоматическом режиме. Представлена концепция внедрения разработанного метода верификации программ в уже существующие обучающие информационные системы. Практическая значимость: разработанный метод формальной верификации программ для виртуальной лаборатории «Машина Поста» позволяет осуществлять оценку практических навыков алгоритмизации задач у обучающихся и упростить разработку виртуальных лабораторий путем уменьшения затрат на формирование тестовых наборов данных для проведения оценивающих мероприятий.