Metody formalne programowania: modelowanie jednego z podstawowych modułów ekspresu do kawy

• Specyfikacja formalna:
  Wykonaj specyfikację jednego z głównych modułów ekspresu do kawy (na przykład moduł przyjmowania pieniędzy lub wyboru napoju) z użyciem formalnego języka programowania według własnego wyboru. Do specyfikacji użyj odpowiednich konstrukcji.

• Testowanie jednostkowe:
  Zaprojektuj minimum 5 testów jednostkowych, które pokrywają główne scenariusze działania wybranego modułu (sprawdzenie poprawności wejścia, obsługa sytuacji błędnych itp.) i zapewnij ich pomyślne przejście.

• Weryfikacja formalna:
  Przeprowadź formalną weryfikację zrealizowanego modułu programowego za pomocą wybranego przez siebie języka specyfikacji formalnej, aby automatycznymi dowodami potwierdzić, że moduł działa zgodnie z określoną specyfikacją.

Wyniki powinny zawierać:

1. Raport, w którym zostanie opisane:

   • Wybraną logikę oraz kluczowe specyfikacje (warunki wstępne, warunki końcowe, inwarianty).

   • Fragmenty kodu z komentarzami, które wyjaśniają logikę realizacji.

   • Wyniki wykonania testów jednostkowych.

   • Wyniki weryfikacji formalnej (automatyczne dowody poprawności).

2. Instrukcję, która pozwala uruchomić projekt na swoim komputerze. Instrukcja powinna zawierać krótki opis konfiguracji środowiska, uruchamiania kodu oraz wykonywania testów.

3. Film demonstracyjny pokazujący działanie projektu. Wykonawca powinien nagrać demonstrację, którą będę mógł łatwo powtórzyć na swoim komputerze.

4. Sam program, który spełnia podane wymagania.