Difference between pages "Rodin Plug-ins" and "Rodin Proof Tactics"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Rivera
 
imported>Son
 
Line 1: Line 1:
−
''For developer support, see [[Rodin Developer Support]]''
+
This page contains descriptions of the available proof tactics within the RODIN Platform.
  
−
== Rodin Plug-in Documentation ==
+
For each tactic, the descriptions is as follows:
  
−
=== Modelling ===
+
* '''Description''': A high-level description of the tactic
−
* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
 
−
* [[Rodin Editor]] augments the standard structured editor of Rodin with a structured text based editor.
 
−
* [[Records_Extension|Records]] provide structured types for Event-B.
 
−
* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.
 
−
* [[Parallel Composition using Event-B]] allows the composition of machines through events for Event-B.
 
−
* [[Decomposition Plug-in User Guide|Decomposition Plug-in]] allows the decomposition of Event-B machines/contexts (shared variables (A-style) and shared events decomposition (B-style))
 
−
* [[Refactoring Framework]] allows the refactoring of elements that are part of file (and also on related files).
 
−
* [[Rose (Structured) Editor]] a model structured editor.
 
−
* [[Flows]] plug-in allows the addition of control flow to a machine.
 
−
* [[Image:Mlogo_big.png|40px]] [[Modularisation Plug-in]] provides a mechanism for constructing and proving modular developments.
 
−
* [[Mode/FT Views]] plug-in brings modelling of modal and fault tolerance features.
 
−
* [[Team-based development]] enables Event-B models to be stored in a shared repository (e.g. SVN).
 
−
* [[Event-B Qualitative Probability User Guide | Qualitative Probability]] provides supports for reasoning about termination with probability 1 (almost-certain termination).
 
  
−
=== Animation ===
+
* '''ID''': An unique ID associated with the tactic.
−
* [[Image:prob_logo_small.png|16px]] [[ProB]] is an animator and model checker for the B-Method,
 
−
* [[Image:AnimB.png|50px]] [[AnimB]] is an animator for the Rodin platform,
 
−
* [[UML-B - Statemachine Animation]] provides an animation (using Pro-B) of UML-B State-machines,
 
  
−
=== Visualization ===
+
* '''Display''': How an application of the tactic is displayed in the proof tree, the auto-tactic preference or the post-tactic preference.
−
* [[Image:bms_logo_small.png|16px]] [[BMotion Studio]] a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization.
 
  
−
=== Documentation ===
+
* '''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:ProR_logo.png|32px]] [[ProR]] supports integration of natural language requirements and Event-B models.
 
−
* [[B2Latex]] allows to typeset an event-B model with latex,
 
  
−
=== Theory and Proof ===
+
* '''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.
−
* [[Isabelle for Rodin]]: Prove proof obligations with Isabelle/HOL. Export proof obligations to Isabelle/HOL theories.
 
−
* [[Theory Plug-in|Theory Plug-in]] provides capabilities to extend the Event-B mathematical language and the Rodin proving infrastructure.
 
−
* [[Proof Purger Interface|Proof Purger]] offers to delete unused proofs.
 
−
* [[Proof Skeleton View]] displays the skeleton of existing proofs.
 
−
* [[SMT Plug-in]] provides interface for SMT solvers.  
 
−
* [[Relevance Filter Plug-in]] Uses heuristics to filter hypotheses shown to the prover
 
  
−
=== Code Generation ===
+
* '''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. ''No'' here mean that there is no separate invocation for this specific tactic.
−
* [http://poporo.uma.pt/favas/EventB2Java.html EventB2Java] generates JML-specified Java implementations of Event-B models. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
 
−
* [http://poporo.uma.pt/favas/EventB2JML.html EventB2JML] translates Event-B machines to JML-specified Java abstract classes. Contributions by Néstor Cataño, Tim Wahls, Camilo Rueda and Víctor Rivera.
 
−
* [http://poporo.uma.pt/eventb2dafny/Home.html EventB2Dafny] translates Event-B proof-obligations into the input language of Dafny. Developed by Néstor Cataño.
 
−
* [http://eb2all.loria.fr/ EB2ALL] (Beta Version) supports automatic code generation from Event-B to C, C++, Java and C#.
 
−
* [[Code Generation|Tasking Event-B]] supports generation of multi-tasking Java, Ada, and OpenMP C code from Event-B.
 
−
* [[B2C plugin|B2C]] translates Event-B models to C source code, which may then be compiled using external C development tools.
 
−
* [http://eventb-to-vhdl.tk/ EHDL] The plug-in enables [http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6037401 VHDL code generation] from formal Event-B models automatically.
 
  
−
=== Experimental ===
+
* '''Example''': Example(s) on how the tactic can be seen from the RODIN Platform.
−
* [[Group refinement plugin|Group Refinement]] changes the set of refinement laws for one refinement step to facilitate a case of atomicity refinement.
 
−
* [[Model Critic]] is an extension using the Epsilon scripting language to analyse Event-B models
 
−
* [[Feature Composition Plug-in]] allows the composition of Event-B features (machines|contexts) and helps the user in resolving conflicts before composition.
 
−
* [[Feature Modelling Tool]] (prototype) can be used to build feature models for product lines and configure these to generate product line members.
 
−
* [[Pattern]] allows the reusing of existing models within a development in order to save the modelling and proving effort.
 
−
* [[Image:Project diagram icon s.png]] [[Project Diagram]] displays the diagram of a Rodin project.
 
−
* [[MBT_plugin|MBT plugin]] can be used to generate test sequences covering the events of an Event-B model.
 
−
* [[Transformation patterns]] allow writing and running transformation scripts in EOL over Event-B models.
 
  
−
== Rodin Plug-in Tutorials ==
+
== True Goal ==
−
* [[UML-B Tutorial]]
+
* '''Description''': Discharges any sequent whose goal is '⊤' (logical true).
−
* [[Requirements Tutorial]],
 
−
* [[AnimB Flash Tutorial|Flash Animation Tutorial]] with animB and Adobe CS3.
 
−
* [http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Tutorial]
 
−
== Tips & Tricks ==
 
  
−
* [[Installing external plug-ins manually]]
+
* '''ID''': org.eventb.core.seqprover.trueGoalTac
  
−
[[Category:User documentation]]
+
* '''Display''': ⊤ Goal
−
[[Category:Plugin]]
+
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Example''': TODO
 +
 
 +
== False Hypothesis ==
 +
 
 +
== Goal in Hypothesis ==
 +
 
 +
== Goal Disjunct in Hypothesis ==
 +
 
 +
== Functional Goal ==
 +
 
 +
== Simplification Rewriter ==
 +
 
 +
== Type Rewriter ==
 +
 
 +
== Implication Goal ==
 +
 
 +
== For-all Goal ==
 +
 
 +
== Exists Hypothesis ==
 +
 
 +
== Find Contradictory Hypothesis ==
 +
 
 +
== Use Equality Hypothesis ==
 +
 
 +
== Shrink Implicative Hypothesis ==
 +
 
 +
== Shrink Enumerated Set ==
 +
 
 +
== Implicative Hypothesis with Conjunctive RHS ==
 +
 
 +
== Implicative Hypothesis with Disjunctive LHS ==
 +
 
 +
== Conjunctive Goal ==
 +
 
 +
== Clarify Goal ==
 +
 
 +
== Functional Overriding in Goal ==
 +
 
 +
== Functional Overriding in Hypothesis ==
 +
 
 +
== Partition Rewriter ==
 +
 
 +
== One-Point Rule in Goal ==
 +
 
 +
== One-Point Rule in Hypothesis ==
 +
 
 +
== Bounded Goal with Finite Hypothesis ==

Revision as of 22:36, 6 March 2010

This page contains descriptions of the available proof tactics within the RODIN Platform.

For each tactic, the descriptions is as follows:

  • Description: A high-level description of the tactic
  • ID: An unique ID associated with the tactic.
  • Display: How an application of the tactic is displayed in the proof tree, the auto-tactic preference or the post-tactic preference.
  • 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.
  • 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.
  • 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. No here mean that there is no separate invocation for this specific tactic.
  • Example: Example(s) on how the tactic can be seen from the RODIN Platform.

True Goal

  • Description: Discharges any sequent whose goal is '⊤' (logical true).
  • ID: org.eventb.core.seqprover.trueGoalTac
  • Display: ⊤ Goal
  • Auto-tactic: Default
  • Post-tactic: Default
  • Interactive: No
  • Example: TODO

False Hypothesis

Goal in Hypothesis

Goal Disjunct in Hypothesis

Functional Goal

Simplification Rewriter

Type Rewriter

Implication Goal

For-all Goal

Exists Hypothesis

Find Contradictory Hypothesis

Use Equality Hypothesis

Shrink Implicative Hypothesis

Shrink Enumerated Set

Implicative Hypothesis with Conjunctive RHS

Implicative Hypothesis with Disjunctive LHS

Conjunctive Goal

Clarify Goal

Functional Overriding in Goal

Functional Overriding in Hypothesis

Partition Rewriter

One-Point Rule in Goal

One-Point Rule in Hypothesis

Bounded Goal with Finite Hypothesis

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Plug-ins&oldid=8430’