Proof Obligation Names (Rodin User Manual) - Revision history

imported>Ladenberger at 15:09, 15 September 2011

2011-09-15T15:09:26Z

← Older revision		Revision as of 15:09, 15 September 2011
Line 1:		Line 1:
			{\| class="wikitable" style="font-style:italic; text-align: center; font-size:120%; border: 3px dashed red;"
			\|-
			! scope="col" \| Do not edit! This content has been migrated to Subversion.
			\|-
			\|([http://handbook.event-b.org Nightly Handbook Build])
			\|}

	Next is a table describing the names of context proof obligations:		Next is a table describing the names of context proof obligations:

imported>Mathieu: Category:Proof

2009-08-12T12:55:14Z

Category:Proof

← Older revision		Revision as of 12:55, 12 August 2009
Line 107:		Line 107:
	[[Category:Rodin Platform\|Proof Obligation Names]]		[[Category:Rodin Platform\|Proof Obligation Names]]
	[[Category:User manual\|Proof Obligation Names]]		[[Category:User manual\|Proof Obligation Names]]
			[[Category:Proof]]

imported>Nicolas: Changed theorems for derived predicates

2009-05-07T16:28:50Z

Changed theorems for derived predicates

← Older revision		Revision as of 16:28, 7 May 2009
Line 5:		Line 5:
	\|Well-definedness of an Axiom\|\|<math>m</math> / WD\|\|<math>m</math> is the axiom name		\|Well-definedness of an Axiom\|\|<math>m</math> / WD\|\|<math>m</math> is the axiom name
	\|-		\|-
	\|Well-definedness of a ~~Theorem~~\|\|<math>m</math> / WD\|\|<math>m</math> is the ~~theorem~~ name		\|Well-definedness of a Derived Axiom\|\|<math>m</math> / WD\|\|<math>m</math> is the axiom name
	\|-		\|-
	\|~~Theorem~~\|\|<math>m</math> / THM\|\|<math>m</math> is the ~~theorem~~ name		\|Derived Axiom\|\|<math>m</math> / THM\|\|<math>m</math> is the axiom name
	\|}		\|}
	</center>		</center>
Line 17:		Line 17:
	\|Well-definedness of an Invariant\|\|<math>v</math> / WD\|\|<math>v</math> is the invariant name		\|Well-definedness of an Invariant\|\|<math>v</math> / WD\|\|<math>v</math> is the invariant name
	\|-		\|-
	\|Well-definedness of a ~~Theorem~~\|\|<math>m</math> / WD\|\|<math>m</math> is the ~~theorem~~ name		\|Well-definedness of a Derived Invariant\|\|<math>m</math> / WD\|\|<math>m</math> is the invariant name
	\|-		\|-
	\|Well-definedness of an event Guard\|\|<math>t</math> / <math>d</math> / WD		\|Well-definedness of an event Guard\|\|<math>t</math> / <math>d</math> / WD
Line 34:		Line 34:
	<math>d</math> is the action name		<math>d</math> is the action name
	\|-		\|-
	\|~~Theorem~~\|\|<math>m</math> / THM\|\|<math>m</math> is the ~~theorem~~ name		\|Derived Invariant\|\|<math>m</math> / THM\|\|<math>m</math> is the invariant name
	\|-		\|-
	\|Invariant Establishment\|\|INIT. / <math>v</math> / INV\|\|<math>v</math> is the invariant name		\|Invariant Establishment\|\|INIT. / <math>v</math> / INV\|\|<math>v</math> is the invariant name
Line 101:		Line 101:
	</center>		</center>

	Remark: At the moment, the deadlock freeness proof obligation generation is missing. If you need it, you can generate it yourself as a ~~theorem~~ saying the the disjunction of the abstract guards imply the disjunction of the concrete guards.		Remark: At the moment, the deadlock freeness proof obligation generation is missing. If you need it, you can generate it yourself as a derived invariant saying the the disjunction of the abstract guards imply the disjunction of the concrete guards.

imported>Mathieu: New page: Next is a table describing the names of context proof obligations: {{SimpleHeader}} |Well-definedness of an Axiom|| $m$ / WD|| $m$ is the axiom name |- |Well...

2009-02-28T09:57:45Z

New page: Next is a table describing the names of context proof obligations: <center> {{SimpleHeader}} |Well-definedness of an Axiom||<math>m</math> / WD||<math>m</math> is the axiom name |- |Well...

New page

Next is a table describing the names of context proof obligations:

<center>
{{SimpleHeader}}
|Well-definedness of an Axiom||<math>m</math> / WD||<math>m</math> is the axiom name
|-
|Well-definedness of a Theorem||<math>m</math> / WD||<math>m</math> is the theorem name
|-
|Theorem||<math>m</math> / THM||<math>m</math> is the theorem name
|}
</center>

Next is a table showing the name of machine proof obligations:

<center>
{{SimpleHeader}}
|Well-definedness of an Invariant||<math>v</math> / WD||<math>v</math> is the invariant name
|-
|Well-definedness of a Theorem||<math>m</math> / WD||<math>m</math> is the theorem name
|-
|Well-definedness of an event Guard||<math>t</math> / <math>d</math> / WD
|<math>t</math> is the event name

<math>d</math> is the action name
|-
|Well-definedness of an event Action||<math>t</math> / <math>d</math> / WD
|<math>t</math> is the event name

<math>d</math> is the action name
|-
|Feasibility of a non-det. event Action||<math>t</math> / <math>d</math> / FIS
|<math>t</math> is the event name

<math>d</math> is the action name
|-
|Theorem||<math>m</math> / THM||<math>m</math> is the theorem name
|-
|Invariant Establishment||INIT. / <math>v</math> / INV||<math>v</math> is the invariant name
|-
|Invariant Preservation||<math>t</math> / <math>v</math> / INV
|<math>t</math> is the event name

<math>v</math> is the invariant name
|}
</center>

Next are the proof obligations concerned with machine refinements:
<center>
{{SimpleHeader}}
|Guard Strengthening||<math>t</math> / <math>d</math> / GRD
|<math>t</math> is the concrete event name

<math>d</math> is the abstract guard name
|-
|Guard Strengthening (merge)||<math>t</math> / MRG||<math>t</math> is the concrete event name
|-
|Action Simulation||<math>t</math> / <math>d</math> / SIM
|<math>t</math> is the concrete event name

<math>d</math> is the abstract action name
|-
|Equality of a preserved Variable||<math>t</math> / <math>v</math> / EQL
|<math>t</math> is the concrete event name

<math>v</math> is the preserved variable
|}
</center>

Next are the proof obligations concerned with the new events variant:

<center>
{{SimpleHeader}}
|Well definedness of Variant||VWD||
|-
|Finiteness for a set Variant||FIN||
|-
|Natural number for a numeric Variant||<math>t</math> / NAT||<math>t</math> is the new event name
|-
|Decreasing of Variant||<math>t</math> / VAR||<math>t</math> is the new event name
|}
</center>
Finally, here are the proof obligations concerned with witnesses:

<center>
{{SimpleHeader}}
|Well definedness of Witness||<math>t</math> / <math>p</math> / WWD
|<math>t</math> is the concrete event name

<math>p</math> is parameter name

or a primed variable name
|-
|Feasibility of non-det. Witness||<math>t</math> / <math>p</math> / WFIS
|<math>t</math> is the concrete event name

<math>p</math> is parameter name

or a primed variable name
|}
</center>

Remark: At the moment, the deadlock freeness proof obligation generation is missing. If you need it, you can generate it yourself as a theorem saying the the disjunction of the abstract guards imply the disjunction of the concrete guards.

[[Category:User documentation|Proof Obligation Names]]
[[Category:Rodin Platform|Proof Obligation Names]]
[[Category:User manual|Proof Obligation Names]]

Proof Obligation Names (Rodin User Manual) - Revision history

imported>Ladenberger at 15:09, 15 September 2011

imported>Mathieu: Category:Proof

imported>Nicolas: Changed theorems for derived predicates

imported>Mathieu: New page: Next is a table describing the names of context proof obligations: {{SimpleHeader}} |Well-definedness of an Axiom||m / WD||m is the axiom name |- |Well...

imported>Mathieu: New page: Next is a table describing the names of context proof obligations: {{SimpleHeader}} |Well-definedness of an Axiom|| $m$ / WD|| $m$ is the axiom name |- |Well...