Difference between revisions of "Extending the Proof Obligation Generator (How to extend Rodin Tutorial)"

From Event-B
Jump to navigationJump to search
imported>Tommy
m (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...)
 
imported>Tommy
m
Line 3: Line 3:
 
=== In this part ===
 
=== 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.
+
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 ===
 
=== Principles ===

Revision as of 16:55, 30 August 2010

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