Difference between pages "Rodin Proof Tactics" and "Rodin Workshop 2020"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Son
 
imported>Son
m
 
Line 1: Line 1:
This page contains descriptions of the available proof tactics within the RODIN Platform.
+
=The 8th Rodin User and Developer Workshop, 26 May, 2020, Ulm, Germany=
  
For each tactic, the descriptions is as follows:
+
[https://abz2020.uni-ulm.de/workshop Rodin Workshop 2020 Website @ ABZ2020]
  
* '''Description''': A high-level description of the tactic. This will be the description appeared in the RODIN Platform preferences.
+
Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and tool-assisted reasoning, in particular, automated proof. The platform is open source and can be extended with plug-ins. A range of plug-ins are available that can be installed via the built-in extensions mechanism of Eclipse.
  
* '''Additional details''': Details explanation of the tactic, when it is applicable, give the associated proof rule. See [[Inference Rules|Inference rules]] list and [[All Rewrite Rules | Rewriting rules]] list.
+
The 8th Rodin workshop will be collocated with the [https://abz2020.uni-ulm.de ABZ2020 Conference].
  
* '''ID''': An unique ID associated with the tactic.
+
The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.
  
* '''Auto-tactic''': ''No'': the tactic cannot be added as an auto-tactic. ''Yes'': the tactic can be added as an auto-tactic. ''Default'': the tactic is a default auto-tactic.
+
For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.
  
* '''[[The Proving Perspective (Rodin User Manual)#The Automatic Post-tactic|Post-tactic]]''': ''No'': the tactic cannot be added as a post-tactic. ''Yes'': the tactic can be added as a post-tactic. ''Default'': the tactic is a default post-tactic.
+
If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to [mailto:rodin@ecs.soton.ac.uk?subject=%91RodinWorkshop2020%93%20Contribution rodin@ecs.soton.ac.uk] by '''24 April 2020''' with subject '''[RodinWorkshop2020] Contribution''', indicating whether it is a tool usage or tool development presentation.
  
* '''Preference display''': (Optional) If the tactic can be used as an auto-tactic or a post-tactic, information on how the tactic is displayed in the auto-tactic preference or the post-tactic preference.
+
We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.
  
* '''Interactive''': ''No'': the tactic cannot be invoked interactively from the [[The Proving Perspective (Rodin User Manual)|proving interface]]. ''Global'': The tactic can be invoked interactively from the [[The Proving Perspective (Rodin User Manual)#The Proof Control Window|Proof Control View]]. ''Goal'': The tactic can be invoked from the [[The Proving Perspective (Rodin User Manual)#Goal and Selected Hypotheses|Goal view]]. ''Hypothesis'': The tactic can be invoked from the [[The Proving Perspective (Rodin User Manual)#Goal and Selected Hypotheses| Hypothesis view]].  If the tactic can be invoked interactively (i.e. either ''Global'', ''Goal'' or ''Hypothesis''), more information about how this could be done will be given. Note that since the '''Post-tactics''' can be launched manually, any tactics that can be included in the post-tactic in principle can be invoked interactively via the post-tactic. Here ''No'' only means that there is no separate invocation for this specific tactic.
+
The proceedings of the workshop will be available as a technical report at the University of Southampton.
  
* '''Proving interface display''': Example(s) on how applications of this tactic can be seen from the [[The Proving Perspective (Rodin User Manual)|proving interface]] of the RODIN Platform.
+
==Organisers==
  
== True Goal ==
 
* '''Description''': Discharges any sequent whose goal is '⊤' (logical true).
 
  
* '''Additional details''': {{InfRule|TRUE_GOAL|<math>\frac{}{\mathsf{H} \;\;\vdash \;\; \btrue}</math>}}
+
Asieh Salehi Fathabadi, University of Southampton
  
* '''ID''': org.eventb.core.seqprover.trueGoalTac
+
Thai Son Hoang, University of Southampton
  
* '''Auto-tactic''': ''Default''
+
Colin Snook, University of Southampton
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': True Goal (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': ⊤ goal
 
 
 
[[Image:TrueGoalExp1.png]]
 
 
 
== False Hypothesis ==
 
* '''Description''': Discharges any sequent containing a '⊥' hypothesis
 
 
 
* '''Additional details''': {{InfRule|FALSE_HYP|<math>\frac{}{\mathsf{H}, \bfalse \;\;\vdash \;\; \mathit{P}}</math>}}
 
 
 
* '''ID''': org.eventb.core.seqprover.falseHypTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': False Hypothesis (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': ⊥ hyp
 
 
 
[[Image: FalseHypExp1.png]]
 
 
 
== Goal in Hypotheses ==
 
* '''Description''': Discharges any sequent whose goal is contained in its hypotheses
 
 
 
* '''Additional details''': {{InfRule|HYP|<math>\frac{}{\mathsf{H}, \mathit{P} \;\;\vdash \;\; \mathit{P}}</math>}}
 
 
 
* '''ID''': org.eventb.core.seqprover.goalInHypTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Goal in Hypotheses (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': hyp
 
 
 
[[Image: GoalInHypExp1.png]]
 
 
 
== Goal Disjunct in Hypothesis ==
 
* '''Description''': Discharges any sequent whose goal is a disjunction and one of whose disjuncts is present in the hypotheses.
 
 
 
* '''Additional details''': {{InfRule|HYP_OR|<math>\frac{}{\mathsf{H}, \mathit{Q} \;\;\vdash \;\; \mathit{P} \lor \ldots \lor \mathit{Q} \lor \ldots \lor \mathit{R}}</math>}}
 
 
 
* '''ID''': org.eventb.core.seqprover.goalDisjInHypTac
 
 
 
* '''Auto-tactic''': ''No''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Goal Disjunct in Hypotheses (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': ∨ goal in hyp
 
 
 
[[Image: GoalDisjInHypExp1.png]]
 
 
 
== Functional Goal ==
 
* '''Description''': Tries to discharge a sequent whose goal states that an expression is a function (i.e. f ∈ T1 ⇸ T2, where T1 and T2 are type expressions).
 
 
 
* '''Additional details''': The sequent is discharged if there is a hypothesis specifying that f is a function of any kind (i.e. partial function, total function, partial injection, total injection, partial surjection,  total surjection, bijection). More information about type expressions in Event-B is in the [[FAQ#What are type expressions in Event-B?|FAQ]] page.
 
 
 
* '''Additional details''': {{InfRule|FUN_GOAL|<math>\frac{}{\mathsf{H}, f \in E \; op \; F \;\;\vdash \;\; f \in T1 \pfun T2}</math>}}
 
 
 
where <math>op</math> is either <math>\pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij </math>.
 
 
 
* '''ID''': org.eventb.core.seqprover.funGoalTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Functional Goal (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': functional goal
 
 
 
[[Image:FunctionalGoalExp1.png]]
 
 
 
== Simplification Rewriter ==
 
* '''Description''': Tries to simplify all predicates in a sequent using pre-defined simplification rewriting rules.
 
 
 
* '''Additional details''': The list of rewriting rules are in the following page [[All Rewrite Rules | http://wiki.event-b.org/index.php/All_Rewrite_Rules]], which are marked as ''Automatic''.
 
 
 
* '''ID''': org.eventb.core.seqprover.autoRewriteTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Simplification Rewriter (Simplify)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': simplification rewrites
 
 
 
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.  There are 3 rewritings have been done as follows.
 
 
 
<math>
 
\begin{array}{rcl}
 
a + 0  & \Longrightarrow & a \\
 
a = a & \Longrightarrow & \btrue \\
 
c * 1 & \Longrightarrow & c \\
 
\end{array}
 
</math>
 
 
 
Note that <math>\btrue</math> hypothesis is always ''dropped'' in the RODIN Platform.
 
 
 
Before [[Image:SimplifcationRewritesExp1.png]]
 
 
 
After [[Image:SimplifcationRewritesExp2.png]]
 
 
 
== Type Rewriter ==
 
* '''Description''': Simplifies predicates containing type expressions such as E ∈ T to ⊤ and T = ∅ to ⊥.
 
 
 
* '''Additional details''': More information about type expressions in Event-B is in the [[FAQ#What are type expressions in Event-B?|FAQ]] page.
 
 
 
* '''ID''': org.eventb.core.seqprover.typeRewriteTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Type Rewriter (Simplify)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': type rewrites
 
 
 
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.
 
 
 
Before [[Image: TypeRewritesExp1.png]]
 
 
 
After [[Image: TypeRewritesExp2.png]]
 
 
 
== Implication Goal ==
 
* '''Description''': Simplifies any sequent with an implicative goal by adding the left hand side of the implication to the hypotheses and making its right hand side the new goal.
 
 
 
* '''ID''': org.eventb.core.seqprover.impGoalTac
 
 
 
* '''Auto-tactic''': ''No''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Implicative Goal (Simplify)
 
 
 
* '''Interactive''': ''Goal''. The <math>\limp</math> symbol in the implicative goal is <font color=red>''redden''</font>. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Deduction''.
 
 
 
[[Image: ImpGoalInteractive1.png]]
 
 
 
* '''Proving interface display''': ⇒ goal
 
 
 
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.
 
 
 
Before [[Image: ImpGoalExp1.png]]
 
 
 
After [[Image: ImpGoalExp2.png]]
 
 
 
== For-all Goal ==
 
* '''Description''': Simplifies any sequent with a universally quantified goal by freeing all its bound variables.
 
 
 
* '''Additional details''': The bound variables will be renaming accordingly to avoid name collision.
 
 
 
* '''ID''': org.eventb.core.seqprover.forallGoalTac
 
 
 
* '''Auto-tactic''': ''No''
 
 
 
* '''Post-tactic''': ''Yes''
 
 
 
* '''Preference display''': For-all Goal (Simplify)
 
 
 
* '''Interactive''': ''Goal''. The  symbol <math>\forall</math> in the universal quantified goal is <font color=red>''redden''</font>. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Forall instantiation''.
 
 
 
[[Image: ForallGoalInteractive1.png]]
 
 
 
* '''Proving interface display''': ∀ goal (frees ''list-of-bounded-identifiers'')
 
 
 
The first example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.  There is no renaming of the bound variable.
 
 
 
Before [[Image: ForallGoalExp1.png]]
 
 
 
After [[Image: ForallGoalExp2.png]]
 
 
 
The second example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. The bound variable <math>x</math> is not renamed, but the bound variable <math>z</math> is renamed to <math>z0</math> to avoid capture of the existing variable <math>z</math>.
 
 
 
Before [[Image: ForallGoalExp3.png]]
 
 
 
After [[Image: ForallGoalExp4.png]]
 
 
 
== Exists Hypothesis ==
 
* '''Description''': In automatic mode (as an auto-tactic or post-tactic), this tactic simplifies any sequent containing existentially quantified hypotheses by freeing their bound variables. In interactive mode, only the selected hypothesis is simplified by freeing its bound variables.
 
 
 
* '''Additional details''': The bound variables will be renaming if necessary to avoid name collision. After freeing their bound variables, if the resulting predicate is a conjunction then it is split into several hypotheses.
 
 
 
* '''ID''': org.eventb.core.seqprover.existHypTac
 
 
 
* '''Auto-tactic''': ''No''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Exists Hypotheses (Simplify)
 
 
 
* '''Interactive''': ''Hypothesis''. The symbol <math>\exists</math> in the existential quantified hypothesis is redden. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Free existential variables''.
 
 
 
[[Image: ExistsHypInteractive1.png]]
 
 
 
* '''Proving interface display''':
 
 
 
The first example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. There is no renaming of the bound variable.
 
 
 
Before [[Image: ExistHypExp1.png]]
 
 
 
After [[Image: ExistHypExp2.png]]
 
 
 
The second example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. The bound variable x is not renamed, but the bound variable z is renamed to z0 to avoid capture of the existing variable z.
 
 
 
Before [[Image: ExistHypExp3.png]]
 
 
 
After [[Image: ExistHypExp4.png]]
 
 
 
== Find Contradictory Hypothesis ==
 
* '''Description''': Discharges a sequent by finding contradictory hypotheses, i.e. <math>P</math> and <math>\neg P </math>.
 
 
 
* '''Additional details''': This tactic tries to find a contradiction using each selected hypothesis that is a negation.
 
 
 
* '''ID''': org.eventb.core.seqprover.findContrHypsTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display''': Find Contradictory Hypotheses (Discharge)
 
 
 
* '''Interactive''': ''No''
 
 
 
* '''Proving interface display''': ct in hyps (''the negated hypothesis'')
 
 
 
[[Image: FindContrHypsExp1.png]]
 
 
 
== Use Equality Hypothesis ==
 
* '''Description''': Simplifies a sequent by rewriting all selected hypotheses and the goal using a (selected) hypothesis that is an equality between a free variable and an expression that does not contain the free variable. The used equality remains in the selected hypotheses to be used again.
 
 
 
* '''Additional details''': Each application of the tactic take only one equality hypothesis into account. If there are several equality hypotheses, they require several applications of the tactic. Moreover, in the case where there are several equality hypotheses, the choice of which hypothesis will be chosen is non-deterministic.  This tactic behaves as [[#Use Equality Hypothesis from Left to Right]] or [[#Use Equality Hypothesis from Right to Left]] depending on if the free variable is on the left or on the right of the equality.
 
 
 
* '''ID''': org.eventb.core.seqprover.eqHypTac
 
 
 
* '''Auto-tactic''': ''Default''
 
 
 
* '''Post-tactic''': ''Default''
 
 
 
* '''Preference display'': Use Equals Hypotheses (Simplify)
 
 
 
* '''Interactive''': ''Hypothesis''. See [[#Use Equality Hypothesis from Left to Right]] and [[#Use Equality Hypothesis from Right to Left]]
 
 
 
* '''Proving interface display''': eh (''the equal hypothesis'') in the case where the free variable is on the left-hand side or he (''the equal hypothesis'') in the case where the free variable is on the right-hand side.
 
 
 
The  example below shows the screen-shots of the step before the application of the tactic, the step after the first application of the tactic with hypothesis <math>x = y + 1</math> and the step just after the second application of the tactic with hypothesis <math>1 = y</math>.
 
 
 
Before [[Image:UseEqualityHypExp1.png]]
 
 
 
After the first application [[Image:UseEqualityHypExp2.png]]
 
 
 
After the second application [[Image:UseEqualityHypExp3.png]]
 
 
 
== Use Equality Hypothesis from Left to Right ==
 
 
 
* '''Description''': Rewriting all selected hypotheses and the goal using a (selected) hypothesis that is an equality between two expressions. The used equality remains in the selected hypotheses to be used again.
 
 
 
* '''ID''':
 
 
 
* '''Auto-tactic''': See [[#Use Equality Hypothesis]]
 
 
 
* '''Post-tactic''': See [[#Use Equality Hypothesis]]
 
 
 
* '''Interactive''': ''Hypothesis''
 
 
 
* '''Proving interface display''':
 
 
 
== Shrink Implicative Hypothesis ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Shrink Enumerated Set ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Implicative Hypothesis with Conjunctive RHS ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Implicative Hypothesis with Disjunctive LHS ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Conjunctive Goal ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Clarify Goal ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Functional Overriding in Goal ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Functional Overriding in Hypothesis ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Partition Rewriter ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== One-Point Rule in Goal ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== One-Point Rule in Hypothesis ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Bounded Goal with Finite Hypothesis ==
 
* '''Description''': TODO
 
 
 
* '''ID''': TODO
 
 
 
* '''Display''': TODO
 
 
 
* '''Auto-tactic''': TODO
 
 
 
* '''Post-tactic''': TODO
 
 
 
* '''Interactive''': TODO
 
 
 
* '''Example''': TODO
 
 
 
== Falsify Goal ==
 
 
 
== conjI ==
 
 
 
== allI ==
 
 
 
== exI ==
 
 
 
== Remove Negation ==
 
 
 
== Review ==
 
 
 
== Proof by cases ==
 
 
 
== Add Hypothesis ==
 
 
 
== Abstract Expression ==
 
 
 
== Automatic Prover ==
 
 
 
== Post tactic ==
 
 
 
== Lasoo ==
 
 
 
== Back Tracking ==
 
 
 
== Prune ==
 
 
 
== Search Hypothesis ==
 
 
 
== Cache Hypothesis ==
 
 
 
== Previous ==
 
 
 
== Next ==
 
 
 
== Information ==
 
 
 
== Falsify Hypothesis ==
 
 
 
== Modus Ponens ==
 
 
 
== conjE ==
 
 
 
== disjE ==
 
 
 
== allE ==
 
 
 
== exE ==
 
 
 
 
 
 
 
== Double Implication Hypothesis ==
 
 
 
== cont Implication Hypothesis ==
 
 
 
== Functional Overriding ==
 
 
 
 
 
 
 
== Modus Tollens ==
 
 
 
== Remove Membership ==
 
 
 
== Remove Inclusion ==
 
 
 
== Remove Strict-Inclusion ==
 
 
 
== Inclusion Set Minus Right ==
 
 
 
== Remove Inclusion Universal ==
 
 
 
== Implication Introduction ==
 
 
 
== Disjunction to Implication ==
 
 
 
== Forall Modus Ponens ==
 
 
 
== Next Pending Sub-goal ==
 
 
 
== Next Reviewed Sub-goal ==
 
 
 
== impAndHyp ==
 
 
 
== impAndGoal ==
 
 
 
== impOrHyp ==
 
 
 
== impOrGoal ==
 
 
 
== relImgUnionRight ==
 
 
 
== relImgUnionLeft ==
 
 
 
== Set Equality ==
 
 
 
== Equivalent ==
 
 
 
== Functional Intersection Image ==
 
 
 
== Functional Set Minus Image ==
 
 
 
== Functional Singleton Image ==
 
 
 
== Converse Relation ==
 
 
 
== Domain Distribution to the Left ==
 
 
 
== Domain Distribution to the Right ==
 
 
 
== Range Distribution to the Left ==
 
 
 
== Range Distribution to the Right ==
 
 
 
== Set Minus ==
 
 
 
== Conjunction and Disjunction Distribution ==
 
 
 
== Union Conjunction Distribution ==
 
 
 
== compUnionDist ==
 
 
 
== Domain/Range Union Distribution ==
 
 
 
== Relational Overriding ==
 
 
 
== Composition Image ==
 
 
 
== Domain Composition ==
 
 
 
== Range Composition ==
 
 
 
== Functional Composition Image ==
 
 
 
== Finite Set in Goal ==
 
 
 
== Finite Intersection in Goal ==
 
 
 
== Finite Set Minus in Goal ==
 
 
 
== Finite Relation in Goal ==
 
 
 
== Finite Relation Image in Goal ==
 
 
 
== Finite Domain in Goal ==
 
 
 
== Finite Range in Goal ==
 
 
 
== Finite Function in Goal ==
 
 
 
== Finite Function Converse in Goal ==
 
 
 
== Finite Functional Relational Image in Goal ==
 
 
 
== Finite Functional Range in Goal ==
 
 
 
== Finite Functional Domain in Goal ==
 
 
 
== Finite Minimum in Goal ==
 
 
 
== Finite Maximum in Goal ==
 
 
 
== Finite Negative in Goal ==
 
 
 
== Finite Positive in Goal ==
 
 
 
== Cardinality Comparison in Goal ==
 
 
 
== Cardinality Up to ==
 
 
 
== Partition Rewrite ==
 
 
 
== Arithmetic Rewrite ==
 
 
 
== Total Domain in Hypothesis / Goal ==
 

Revision as of 20:43, 27 February 2020

The 8th Rodin User and Developer Workshop, 26 May, 2020, Ulm, Germany

Rodin Workshop 2020 Website @ ABZ2020

Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and tool-assisted reasoning, in particular, automated proof. The platform is open source and can be extended with plug-ins. A range of plug-ins are available that can be installed via the built-in extensions mechanism of Eclipse.

The 8th Rodin workshop will be collocated with the ABZ2020 Conference.

The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.

For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.

If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to rodin@ecs.soton.ac.uk by 24 April 2020 with subject [RodinWorkshop2020] Contribution, indicating whether it is a tool usage or tool development presentation.

We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.

The proceedings of the workshop will be available as a technical report at the University of Southampton.

Organisers

Asieh Salehi Fathabadi, University of Southampton

Thai Son Hoang, University of Southampton

Colin Snook, University of Southampton