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

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

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

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

Результати повинні містити:

1. Звіт, в якому буде описано:

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

   • Фрагменти коду з коментарями, які пояснюють логіку реалізації.

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

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

2. Інструкцію, що дозволяє запустити проект на своєму ПК. Інструкція повинна містити короткий опис налаштування середовища, запуску коду та виконання тестів.

3. Демонстраційне відео з показом роботи проекту. Виконавець має записати демонстрацію, яку я зможу легко повторити на своєму комп’ютері.

4. Сама програма, що відповідає наведеним вимогам.