Rodin Handbook





 

3.4 Proving

In Section 3.2.7, we learned what proof obligations are generated by Rodin from an Event-B model. We validate the model by discharging proof obligations. This is what we call proving.

\includegraphics[width=7mm]{img/tick_64.png}

In this chapter we will:

  • Explain proof rules

  • Explain tactics

  • Explain and describe provers

  • Explain reasoners

  • Describe how to perform automatic and manual proving

  • Purge proofs for maintenance

  • Simplify proofs for maintenability and storage