Accessing Proof Obligations - Revision history

imported>Mathieu: Category:Proof

2009-08-12T12:53:00Z

← Older revision		Revision as of 12:53, 12 August 2009
Line 45:		Line 45:
	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]
			[[Category:Proof]]

imported>Mathieu: {{TOCright}}

2008-10-28T13:46:01Z

← Older revision		Revision as of 13:46, 28 October 2008
Line 1:		Line 1:
			{{TOCright}}

	==File Types==		==File Types==
	For each machine and each context there exists one of each of the following roots:		For each machine and each context there exists one of each of the following roots:

imported>Maria at 13:19, 28 October 2008

2008-10-28T13:19:14Z

← Older revision		Revision as of 13:19, 28 October 2008
Line 6:		Line 6:
	*IPORoot: This root contains the sequents (IPOSequent) of the proof obligations. It is contained in a file with the extension .bpo.		*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 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>.		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>.

Line 23:		Line 23:

	==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==

imported>Maria at 12:59, 28 October 2008

2008-10-28T12:59:33Z

← Older revision		Revision as of 12:59, 28 October 2008
Line 2:		Line 2:
	For each machine and each context there exists one of each of the following roots:		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.		*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.		*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==

imported>Maria at 10:32, 28 October 2008

2008-10-28T10:32:47Z

← Older revision		Revision as of 10:32, 28 October 2008
Line 24:		Line 24:
	==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==

imported>Maria at 10:32, 28 October 2008

2008-10-28T10:32:28Z

← Older revision		Revision as of 10:32, 28 October 2008
Line 1:		Line 1:
	==File Types==		==File Types==
	For each machine and each context there exists one of each of the following ~~files~~:		For each machine and each context there exists one of each of the following roots:

	*~~IPSFile (.bps)~~: This ~~file~~ contains the statuses (IPSStatus) of the proof obligations.		*IPSRoot: This root contains the statuses (IPSStatus) of the proof obligations.

	*~~IPOFile (.bpo)~~: This ~~file~~ contains the sequents (IPOSequent) of the proof obligations.		*IPORoot: This root contains the sequents (IPOSequent) of the proof obligations.

	==The Connection==		==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 <code>file.getBarName()</code>.~~		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 ~~files~~, one get the others though the functions <code>~~getMachineFile~~()</code>, <code>~~getContextFile~~()</code>, <code>~~getPSFile~~()</code> and <code>~~getPOFile~~()</code>.

	==Accessing the sequents of an ~~IPOFile~~==		==Accessing the sequents of an IPORoot==
	*All sequents of ''~~file~~'': <code>IPOSequent[] sequents = ~~file~~.getSequents()</code>		*All sequents of ''root'': <code>IPOSequent[] sequents = root.getSequents()</code>
	*A specific sequent (e.g. INITIALISATION/inv1/INV) of ''~~file~~'': <code>IPOSequent sequent = ~~file~~.getSequent("INITIALISATION/inv1/INV")</code>		*A specific sequent (e.g. INITIALISATION/inv1/INV) of ''root'': <code>IPOSequent sequent = root.getSequent("INITIALISATION/inv1/INV")</code>

	==Accessing the statuses of an ~~IPSFile~~ ==		==Accessing the statuses of an IPSRoot ==
	*All statuses of ''~~file~~'': <code>IPSStatus[] statuses = ~~file~~.getStatuses()</code>		*All statuses of ''root'': <code>IPSStatus[] statuses = root.getStatuses()</code>
	*A specific status (e.g. INITIALISATION/inv1/INV) of ''~~file~~'': <code>IPSStatus status = ~~file~~.getStatus("INITIALISATION/inv1/INV")</code>		*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 ~~IPOFile~~ that contains ''sequent'': <code>~~IPOFile poFile~~ = sequent.~~getAncestor(IPOFile.ELEMENT_TYPE)~~;</code>		*1. Find the IPORoot that contains ''sequent'': <code>IPORoot poRoot = sequent.getParent;</code>
	*2. Find the matching ~~IPSFile~~: <code>~~IPSFile isFile~~ = ~~poFile~~.~~getPSFile~~();</code>		*2. Find the matching IPSRoot: <code>IPSRoot psRoot = poRoot.getPSRoot();</code>
	*3. Find the machting status: <code>IPSStatus status = ~~psFile~~.getStatus(sequent.getElementName);</code>		*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 all proof obligations of a project==~~
	*All IPOFiles of ''project'': <code>IPOFile[] pofiles = project.getChildrenOfType(IPOFile.ELEMENT_TYPE);</code>

	*All IPSFiles of ''project'': <code>IPSFile[] psfiles = project.getChildrenOfType(IPSFile.ELEMENT_TYPE);</code>

	==Accessing the proof obligations of a given machine or context==		==Accessing the proof obligations of a given machine or context==
	*1. Find the machting ~~IPOFile~~ for ''machine'' (~~IMachineFile~~): <code>~~IPOFile poFile~~ = machine.~~getPOFile~~();</code>		*1. Find the machting IPORoot for ''machine'' (IMachineRoot): <code>IPORoot poRoot = machine.getPORoot();</code>
	*2. Get all sequents: [[Accessing_Proof_Obligations#~~Accessing_the_sequents_of_an_IPOFile~~ \| Accessing the sequents of an ~~IPOFile~~]]		*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 ~~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 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 36:
	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==

imported>Mathieu: cat

2008-09-17T16:59:59Z

cat

← Older revision		Revision as of 16:59, 17 September 2008
Line 45:		Line 45:
	==Finding all the proof obligations for a given Invariant==		==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.		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.


			[[Category:Developer documentation]]
			[[Category:Rodin Platform]]

imported>Maria at 14:38, 16 September 2008

2008-09-16T14:38:57Z

← Older revision		Revision as of 14:38, 16 September 2008
Line 23:		Line 23:
	*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>

	Finding the corresponding sequent to a given status ~~is done basically~~ the ~~same way.~~		==Finding the corresponding sequent to a given status==
			Use the function <code>getPOSequent()</code> in IPSStatus

	==Accessing all proof obligations of a project==		==Accessing all proof obligations of a project==

imported>Maria at 12:08, 16 September 2008

2008-09-16T12:08:20Z

← Older revision		Revision as of 12:08, 16 September 2008
Line 38:		Line 38:
	==The sources of a proof obligations==		==The sources of a proof obligations==
	The sources of a proof obligations describe where that proof obligation comes from (e.g. Invariants, Events).		The sources of a proof obligations describe where that proof obligation comes from (e.g. Invariants, Events).
			They can be accessed from the IPOSequent: <code>IPOSource[] sources = sequents[i].getSources();</code>

			An IPOSource can be an instance of IInvariant, ITheorem etc.

			==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.

imported>Maria at 11:59, 16 September 2008

2008-09-16T11:59:09Z

← Older revision		Revision as of 11:59, 16 September 2008
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).