Difference between revisions of "Accessing Proof Obligations"

From Event-B
Jump to navigationJump to search
imported>Maria
imported>Maria
Line 22: Line 22:
 
*2. Find the matching IPSFile: <code>IPSFile isFile = poFile.getPSFile();</code>
 
*2. Find the matching IPSFile: <code>IPSFile isFile = poFile.getPSFile();</code>
 
*3. Find the machting status: <code>IPSStatus status =  psFile.getStatus(sequent.getElementName);</code>
 
*3. Find the machting status: <code>IPSStatus status =  psFile.getStatus(sequent.getElementName);</code>
 
==The sources of a proof obligations==
 
The sources of a proof obligations describe where that proof obligation comes from (e.g. Invariants, Events).
 
 
  
 
Finding the corresponding sequent to a given status is done basically the same way.
 
Finding the corresponding sequent to a given status is done basically the same way.
Line 40: Line 36:
 
*3. For each sequent access the status with the same name in the IPSFile: [[Accessing_Proof_Obligations#Accessing_the_statuses_of_an_IPSFile | Accessing the statuses of an IPSFile]]
 
*3. For each sequent access the status with the same name in the IPSFile: [[Accessing_Proof_Obligations#Accessing_the_statuses_of_an_IPSFile | Accessing the statuses of an IPSFile]]
  
==Finding the sources of a
+
==The sources of a proof obligations==
 +
The sources of a proof obligations describe where that proof obligation comes from (e.g. Invariants, Events).

Revision as of 11:59, 16 September 2008

File Types

For each machine and each context there exists one of each of the following files:

  • IPSFile (.bps): This file contains the statuses (IPSStatus) of the proof obligations.
  • IPOFile (.bpo): This file contains the sequents (IPOSequent) of the proof obligations.

The Connection

An IPSFile, an IPOFile and an IMachineFile or IContextFile are connected through the name. For example machine m0 has IMachineFile m0.bum, IPSFile m0.bps and IPOFile m0.bpo. The name of each of these files is accessible via file.getBarName(). If one has any of these files, one get the others though the functions getMachineFile(), getContextFile(), getPSFile() and getPOFile().

Accessing the sequents of an IPOFile

  • All sequents of file: IPOSequent[] sequents = file.getSequents()
  • A specific sequent (e.g. INITIALISATION/inv1/INV) of file: IPOSequent sequent = file.getSequent("INITIALISATION/inv1/INV")

Accessing the statuses of an IPSFile

  • All statuses of file: IPSStatus[] statuses = file.getStatuses()
  • A specific status (e.g. INITIALISATION/inv1/INV) of file: IPSStatus status = file.getStatus("INITIALISATION/inv1/INV")

Finding the corresponding status to a given sequent

  • 1. Find the IPOFile that contains sequent: IPOFile poFile = sequent.getAncestor(IPOFile.ELEMENT_TYPE);
  • 2. Find the matching IPSFile: IPSFile isFile = poFile.getPSFile();
  • 3. Find the machting status: IPSStatus status = psFile.getStatus(sequent.getElementName);

Finding the corresponding sequent to a given status is done basically the same way.

Accessing all proof obligations of a project

  • All IPOFiles of project: IPOFile[] pofiles = project.getChildrenOfType(IPOFile.ELEMENT_TYPE);
  • All IPSFiles of project: IPSFile[] psfiles = project.getChildrenOfType(IPSFile.ELEMENT_TYPE);

Accessing the proof obligations of a given machine or context

The sources of a proof obligations

The sources of a proof obligations describe where that proof obligation comes from (e.g. Invariants, Events).