Extending the Static Checker (How to extend Rodin Tutorial)

<prev: Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)

^up: How to extend Rodin Tutorial (Index)

In this part

We will see how to add rules to statically check the machines after our extension. The Static Checker is one dedicated part of the Proof Obligation generation process. In fact, we have to be sure before creating Proof Obligations, that the model is correctly expressed.

Step2

<prev: Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)

^up: How to extend Rodin Tutorial (Index)