Extending the Proof Obligation Generator (How to extend Rodin Tutorial)
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?".
We will study here, the case of the BNF proof obligation, which is described in the paper. This PO overrides the FIN proof obligation. Thus we will see here, how to :
- remove the FIN PO which is generated by default,
- add our new BNF PO.
Principles
1. To extend the proof obligation generator (POG) in order to add some proof obligations that one has to discharge, one has to define a proof obligation processor module using the extension point : org.eventb.core.pogModuleTypes.
2. Then , one has to set up a configuration involving those modules and giving them a hierachy. This is done exactly the same way as for creating a static checker configuration.
3. Finally, it is needed to add this POG configuration to the default one, so the proof obligation generation can be performed.
We want here to show how to generate one proof obligation. We will add the PO named BFN to ensure that the bound is a natural number or finite. It will be generated once for all for the machine taken into account. Moreover, this PO overrides the default FIN proof obligation which is generated if a convergent event (with the associated variant) is present in the model. If a probabilistic event is in the machine, we want to create our BFN PO, thus we have to remove the FIN PO.
In step 1, we will create a filter to remove the PO FIN if our machine contains a probabilistic event, and in the second step, we will explain how to create our PO BFN.
Step 1 : Removing a PO
To remove a PO, one has to create a filter module. This follows the same way as what is done for the static checker. After a small search in the package org.eventb.internal.core.pog.modules, we identify that the module responsible of creating the FIN PO is actually FwdMachineVariantModule. The goal is here to register our filter as a submodule of FwdMachineVariantModule that will prevent it to create the FIN PO.
The code is really simple... first one has to check if the model contains a probabilistic event, which means that we want to override the FIN PO that will be created by default, and then, in the filter, one has to search from the generated PO if one corresponds to FIN by searching inside PO names and reject it.
1. give the module an id (here finPORejectingModule),
2. a human readable name (here "Machine POG Filter FIN PO Rejecting Module"),
3. register a parent in the hierarchy of modules (here we used the variant POG module of the Event-B POG that creates the POG we want to suppress: org.eventb.core.fwdMachineVariantModule),
4. create a class for this module.(here we created the class fr.systerel.rodinextension.sample.pog.modules.FinPORejectingModule).
Step 2 : Adding POG modules =
From the extension point org.eventb.core.pogModuleTypes, create a processorModule extension to implement our first PO generation process using a POG processor :
As for a static checker module,
1. give the module an id (here fwdMachineBoundModule),
2. a human readable name (here "Machine POG Forward Bound Module"),
3. register a parent in the hierarchy of modules (here we used the machine POG module of the Event-B POG : org.eventb.core.machineModule),
4. create a class for this module.(here we created the class fr.systerel.rodinextension.sample.pog.modules.FwdMachineBoundModule).
