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 (i.e. proof obligations are generated for a model which is sound).
The question addressed here is : " Which are the conditions under which the model is correct for proof obligation generation? ".

Step1

In our case of probabilistic reasoning, the following conditions are checked for a model containing probabilistic events :

1. The variant V (declared as usual) is either of the type integer or some set.
2. There is exactly one bound for a model where the probabilistic converge is proved. The bound element B must be of the same type as the declared variant.
3. Every probabilistic event must be refined by a probabilistic event.
4. The result of merging a probabilistic event and a convergent event is a probabilistic event.

We can face two sorts of situations during the static checking :

1. we encounter a problem which doesn't affect the PO generation : this leads to a warning.
2. we encounter a problem which affects the PO generation : this leads to an error.

Step2

<prev: Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)

^up: How to extend Rodin Tutorial (Index)