imported>Son |
|
| Line 1: |
Line 1: |
| − | This page contains descriptions of the available proof tactics within the RODIN Platform.
| + | Return to [[Rodin Plug-ins]] |
| | | | |
| − | For each tactic, the descriptions is as follows:
| + | UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. [[UML-B]] works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams. |
| | | | |
| − | * '''Description''': A high-level description of the tactic. This will be the description appeared in the RODIN Platform preferences.
| + | Our [https://www.uml-b.org UML-B] website contains more information about installing UML-B and getting started, as well as our current research and collaborations. |
| | | | |
| − | * '''Additional details''': (Optional) Details explanation of the tactic.
| + | UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine. |
| | | | |
| − | * '''ID''': An unique ID associated with the tactic. | + | * [[Image:IUMLB.png]] [[Event-B Statemachines| State-machine diagrams]] a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine. |
| | | | |
| − | * '''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. | + | * [[Image:IUMLB.png]] [[Event-B Classdiagrams| Class diagrams]] a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets. |
| | | | |
| − | * '''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.
| + | ==Lectures== |
| | | | |
| − | * '''Preference display''': Information on how an application of the tactic is displayed in the auto-tactic preference or the post-tactic preference. | + | * [[Media:iUML-BClassDiagramsLecture.pdf | UML-B Class-diagrams Lecture]] : Lecture slides on the use of UML-B Class-diagrams |
| | | | |
| − | * '''Interactive''': ''No'': the tactic cannot be invoked interactively. ''Global'': The tactic can be invoked from the Proof Control. ''Goal'': The tactic can be invoked from the goal view. ''Hypothesis'': The tactic can be invoked from the 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. | + | * [[Media:iUML-BStatemachinesLecture.pdf | UML-B State-machines Lecture]] : Lecture slides on the use of UML-B State-machines. |
| | | | |
| − | * '''Proving interface display''': Example(s) on how an application of this tactic can be seen from the proving interface of the RODIN Platform.
| + | ==Tutorials== |
| | | | |
| − | == True Goal ==
| + | * [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of UML-B Class-diagrams. |
| − | * '''Description''': Discharges any sequent whose goal is '⊤' (logical true). | |
| | | | |
| − | * '''ID''': org.eventb.core.seqprover.trueGoalTac | + | * [[iUML-B State-machines Tutorial]] : A tutorial on the use of UML-B State-machines. |
| | | | |
| − | * '''Auto-tactic''': ''Default''
| + | ==Guidelines== |
| | | | |
| − | * '''Post-tactic''': ''Default'' | + | * [[UML-B - Modelling a control system]] : Some guidelines on modelling styles for a control system |
| | | | |
| − | * '''Preference display''': True Goal (Discharge)
| |
| | | | |
| − | * '''Interactive''': ''No''
| + | [[Category:User documentation]] |
| − | | + | [[Category:UML-B]] |
| − | * '''Proving interface display''': ⊤ goal
| + | [[Category:Plugin]] |
| − | | |
| − | [[Image:TrueGoalExp1.png]]
| |
| − | | |
| − | == False Hypothesis ==
| |
| − | * '''Description''': Discharges any sequent containing a '⊥' hypothesis
| |
| − | | |
| − | * '''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
| |
| − | | |
| − | * '''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.
| |
| − | | |
| − | * '''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).
| |
| − | | |
| − | * '''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]].
| |
| − | | |
| − | * '''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''': TODO
| |
| − | | |
| − | * '''ID''': TODO
| |
| − | | |
| − | * '''Display''': TODO
| |
| − | | |
| − | * '''Auto-tactic''': TODO
| |
| − | | |
| − | * '''Post-tactic''': TODO
| |
| − | | |
| − | * '''Interactive''': TODO
| |
| − | | |
| − | * '''Example''': TODO
| |
| − | | |
| − | == For-all Goal ==
| |
| − | * '''Description''': TODO
| |
| − | | |
| − | * '''ID''': TODO
| |
| − | | |
| − | * '''Display''': TODO
| |
| − | | |
| − | * '''Auto-tactic''': TODO
| |
| − | | |
| − | * '''Post-tactic''': TODO
| |
| − | | |
| − | * '''Interactive''': TODO
| |
| − | | |
| − | * '''Example''': TODO
| |
| − | | |
| − | == Exists Hypothesis ==
| |
| − | * '''Description''': TODO
| |
| − | | |
| − | * '''ID''': TODO
| |
| − | | |
| − | * '''Display''': TODO
| |
| − | | |
| − | * '''Auto-tactic''': TODO
| |
| − | | |
| − | * '''Post-tactic''': TODO
| |
| − | | |
| − | * '''Interactive''': TODO
| |
| − | | |
| − | * '''Example''': TODO
| |
| − | | |
| − | == Find Contradictory Hypothesis ==
| |
| − | * '''Description''': TODO
| |
| − | | |
| − | * '''ID''': TODO
| |
| − | | |
| − | * '''Display''': TODO
| |
| − | | |
| − | * '''Auto-tactic''': TODO
| |
| − | | |
| − | * '''Post-tactic''': TODO
| |
| − | | |
| − | * '''Interactive''': TODO
| |
| − | | |
| − | * '''Example''': TODO
| |
| − | | |
| − | == Use Equality Hypothesis ==
| |
| − | * '''Description''': TODO
| |
| − | | |
| − | * '''ID''': TODO
| |
| − | | |
| − | * '''Display''': TODO
| |
| − | | |
| − | * '''Auto-tactic''': TODO
| |
| − | | |
| − | * '''Post-tactic''': TODO
| |
| − | | |
| − | * '''Interactive''': TODO
| |
| − | | |
| − | * '''Example''': TODO
| |
| − | | |
| − | == 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 ==
| |
| − | | |
| − | == eq1 ==
| |
| − | | |
| − | == Double Implication Hypothesis ==
| |
| − | | |
| − | == cont Implication Hypothesis ==
| |
| − | | |
| − | == Functional Overriding ==
| |
| − | | |
| − | == Equality ==
| |
| − | | |
| − | == 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 ==
| |
State-machine diagrams a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.
