Accessing Proof Obligations: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Mathieu m cat |
imported>Mathieu |
||
| (5 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
{{TOCright}} | |||
==File Types== | ==File Types== | ||
For each machine and each context there exists one of each of the following | For each machine and each context there exists one of each of the following roots: | ||
* | *IPSRoot: This root contains the statuses (IPSStatus) of the proof obligations. It is contained in a file with the extension .bps. | ||
* | *IPORoot: This root contains the sequents (IPOSequent) of the proof obligations. It is contained in a file with the extension .bpo. | ||
==The Connection== | ==The Connection between different root types== | ||
An | An IPSRoot, an IPORootand an IMachineRoot or IContextRoot are connected through the name. For example machine ''m0'' has IMachineRoot that is in file ''m0.bum'', IPSRoot in ''m0.bps'' and IPORoot in ''m0.bpo''. If one has any of these roots, one get the others though the functions <code>getMachineRoot()</code>, <code>getContextRoot()</code>, <code>getPSRoot()</code> and <code>getPORoot()</code>. | ||
If one has any of these | |||
==Accessing the sequents of an | ==Accessing the sequents of an IPORoot== | ||
*All sequents of '' | *All sequents of ''root'': <code>IPOSequent[] sequents = root.getSequents()</code> | ||
*A specific sequent (e.g. INITIALISATION/inv1/INV) of '' | *A specific sequent (e.g. INITIALISATION/inv1/INV) of ''root'': <code>IPOSequent sequent = root.getSequent("INITIALISATION/inv1/INV")</code> | ||
==Accessing the statuses of an | ==Accessing the statuses of an IPSRoot == | ||
*All statuses of '' | *All statuses of ''root'': <code>IPSStatus[] statuses = root.getStatuses()</code> | ||
*A specific status (e.g. INITIALISATION/inv1/INV) of '' | *A specific status (e.g. INITIALISATION/inv1/INV) of ''root'': <code>IPSStatus status = root.getStatus("INITIALISATION/inv1/INV")</code> | ||
==Finding the corresponding status to a given sequent== | ==Finding the corresponding status to a given sequent== | ||
*1. Find the | *1. Find the IPORoot that contains ''sequent'': <code>IPORoot poRoot = sequent.getParent;</code> | ||
*2. Find the matching | *2. Find the matching IPSRoot: <code>IPSRoot psRoot = poRoot.getPSRoot();</code> | ||
*3. Find the machting status: <code>IPSStatus status = | *3. Find the machting status: <code>IPSStatus status = psRoot.getStatus(sequent.getElementName);</code> | ||
==Finding the corresponding sequent to a given status== | ==Finding the corresponding sequent to a given status== | ||
Use the function <code>getPOSequent()</code> in IPSStatus | Use the function <code>getPOSequent()</code> in IPSStatus. | ||
==Accessing the proof obligations of a given machine or context== | ==Accessing the proof obligations of a given machine or context== | ||
*1. Find the machting | *1. Find the machting IPORoot for ''machine'' (IMachineRoot): <code>IPORoot poRoot = machine.getPORoot();</code> | ||
*2. Get all sequents: [[Accessing_Proof_Obligations# | *2. Get all sequents: [[Accessing_Proof_Obligations#Accessing_the_sequents_of_an_IPORoot | Accessing the sequents of an IPORoot]] | ||
*1. Find the machting IPSFile for ''machine'': <code>IPSFile psFile = machine.getPSFile();</code> | *1. Find the machting IPSFile for ''machine'': <code>IPSFile psFile = machine.getPSFile();</code> | ||
*3. For each sequent access the status with the same name in the | *3. For each sequent access the status with the same name in the IPSRoot: [[Accessing_Proof_Obligations#Accessing_the_statuses_of_an_IPSRoot | Accessing the statuses of an IPSRoot]] | ||
==The sources of a proof obligations== | ==The sources of a proof obligations== | ||
| Line 41: | Line 37: | ||
They can be accessed from the IPOSequent: <code>IPOSource[] sources = sequents[i].getSources();</code> | They can be accessed from the IPOSequent: <code>IPOSource[] sources = sequents[i].getSources();</code> | ||
An IPOSource can be an instance of IInvariant, ITheorem etc. | An IPOSource can be an instance of an element like IInvariant, ITheorem etc or it can be an IAction, IWitness or IGuard. | ||
==Finding all the proof obligations for a given Invariant== | ==Finding all the proof obligations for a given Invariant== | ||
| Line 49: | Line 45: | ||
[[Category:Developer documentation]] | [[Category:Developer documentation]] | ||
[[Category:Rodin Platform]] | [[Category:Rodin Platform]] | ||
[[Category:Proof]] | |||
Latest revision as of 12:53, 12 August 2009
File Types
For each machine and each context there exists one of each of the following roots:
- IPSRoot: This root contains the statuses (IPSStatus) of the proof obligations. It is contained in a file with the extension .bps.
- IPORoot: This root contains the sequents (IPOSequent) of the proof obligations. It is contained in a file with the extension .bpo.
The Connection between different root types
An IPSRoot, an IPORootand an IMachineRoot or IContextRoot are connected through the name. For example machine m0 has IMachineRoot that is in file m0.bum, IPSRoot in m0.bps and IPORoot in m0.bpo. If one has any of these roots, one get the others though the functions getMachineRoot(), getContextRoot(), getPSRoot() and getPORoot().
Accessing the sequents of an IPORoot
- All sequents of root:
IPOSequent[] sequents = root.getSequents() - A specific sequent (e.g. INITIALISATION/inv1/INV) of root:
IPOSequent sequent = root.getSequent("INITIALISATION/inv1/INV")
Accessing the statuses of an IPSRoot
- All statuses of root:
IPSStatus[] statuses = root.getStatuses() - A specific status (e.g. INITIALISATION/inv1/INV) of root:
IPSStatus status = root.getStatus("INITIALISATION/inv1/INV")
Finding the corresponding status to a given sequent
- 1. Find the IPORoot that contains sequent:
IPORoot poRoot = sequent.getParent; - 2. Find the matching IPSRoot:
IPSRoot psRoot = poRoot.getPSRoot(); - 3. Find the machting status:
IPSStatus status = psRoot.getStatus(sequent.getElementName);
Finding the corresponding sequent to a given status
Use the function getPOSequent() in IPSStatus.
Accessing the proof obligations of a given machine or context
- 1. Find the machting IPORoot for machine (IMachineRoot):
IPORoot poRoot = machine.getPORoot(); - 2. Get all sequents: Accessing the sequents of an IPORoot
- 1. Find the machting IPSFile for machine:
IPSFile psFile = machine.getPSFile(); - 3. For each sequent access the status with the same name in the IPSRoot: Accessing the statuses of an IPSRoot
The sources of a proof obligations
The sources of a proof obligations describe where that proof obligation comes from (e.g. Invariants, Events).
They can be accessed from the IPOSequent: IPOSource[] sources = sequents[i].getSources();
An IPOSource can be an instance of an element like IInvariant, ITheorem etc or it can be an IAction, IWitness or IGuard.
Finding all the proof obligations for a given Invariant
It is not possible to directly find the proof obligations for a given invariant or any other element. Instead check if the sources of the proof obligations contain the invariant.
