Формальные методы программирования: моделирование одного из основных модулей кофейного аппарата

• Формальная спецификация:
  Выполните спецификацию одного из основных модулей кофейного аппарата (например, модуль приема средств или выбора напитка) с использованием формального языка программирования на ваш выбор. Для спецификации используйте соответствующие конструкции.

• Юнит-тестирование:
  Спроектируйте минимум 5 юнит-тестов, которые покрывают основные сценарии работы выбранного модуля (проверка корректности ввода, обработка ошибочных ситуаций и т.д.) и обеспечьте их успешное прохождение.

• Формальная верификация:
  Проведите формальную верификацию реализованного программного модуля с помощью выбранного вами языка формальной спецификации, чтобы автоматическими доказательствами подтвердить, что модуль работает согласно заданной спецификации.

Результаты должны содержать:

1. Отчет, в котором будет описано:

   • Выбранную логику и ключевые спецификации (предусловия, постусловия, инварианты).

   • Фрагменты кода с комментариями, которые объясняют логику реализации.

   • Результаты выполнения юнит-тестов.

   • Результаты формальной верификации (автоматические доказательства корректности).

2. Инструкцию, которая позволяет запустить проект на своем ПК. Инструкция должна содержать короткое описание настройки окружения, запуска кода и выполнения тестов.

3. Демонстрационное видео с показом работы проекта. Исполнитель должен записать демонстрацию, которую я смогу легко повторить на своем компьютере.

4. Саму программу, которая соответствует приведенным требованиям.