Extending the Proof Obligation Generator (How to extend Rodin Tutorial)

From Event-B
Revision as of 16:52, 30 August 2010 by imported>Tommy (New page: {{Navigation|Previous= Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial) | Up= How to extend Rodin Tutorial (Index) | Next= }} === In this part === We w...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

In this part

We will see how to proof obligations to discharge for machines after having added our extensions for Probabilistic Reasoning and 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 file 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.

Principles