Formal methods of programming: modeling one of the main modules of the coffee machine

• Formal Specification:
  Implement the specification of one of the main modules of the coffee machine (for example, the payment acceptance module or drink selection module) using a formal programming language of your choice. Use appropriate constructs for the specification.

• Unit Testing:
  Design at least 5 unit tests that cover the main scenarios of the chosen module (input correctness checks, error handling, etc.) and ensure their successful execution.

• Formal Verification:
  Conduct formal verification of the implemented software module using the formal specification language of your choice to automatically prove that the module operates according to the specified requirements.

The results should include:

1. A report that describes:

   • The chosen logic and key specifications (preconditions, postconditions, invariants).

   • Code snippets with comments explaining the implementation logic.

   • The results of the unit tests.

   • The results of the formal verification (automatic correctness proofs).

2. An instruction that allows running the project on your PC. The instruction should include a brief description of setting up the environment, running the code, and executing the tests.

3. A demonstration video showing the project in action. The performer should record a demonstration that I can easily replicate on my computer.

4. The program itself that meets the specified requirements.