Extending the Proof Obligation Generator (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 create proof obligations to discharge for the machines relatively to our extensions for Probabilistic Reasoning and after having statically checked the machines. The latter operation is the first part of the proof obligation generation as the proof obligation generator takes statically checked files in input. One will notice that the provided architecture for static checking is really similar to the one for proof obligation generation. Thus, it can be useful for the reader to understand well the previous part of this tutorial, as we will not repeat all the ideas shared by the both processes. The question here is "What needs to be mathematically proved with those newly added elements in hands?".

Principles

<prev: Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)

^up: How to extend Rodin Tutorial (Index)