imported>Pascal |
|
| Line 1: |
Line 1: |
| | {{TOCright}} | | {{TOCright}} |
| | + | Return to [[Rodin Plug-ins]] |
| | | | |
| − | == Introduction ==
| + | The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines. |
| − | The Event-B to [[#ancre_3|SMT-LIB]] plug-in allows to translate mathematical lemmas that rely on the Event-B language to the SMT-LIB format. | + | Extension to Event-B including the ''machine inclusion'' mechanism is also supported. |
| | | | |
| − | The considered lemmas are those often encountered in practice, but not yet well supported by proving
| + | <br style="clear: both" /> |
| − | tools such as those embedded in the Rodin platform. The purpose is not here to entirely define the translation, but rather to give a mapping for this subset of Event-B formulas. These typical mathematical problems are entry points for the [[#ancre_1|DECERT]] project, and more precisely for the Work Package 1. Using the SMT-LIB standard is among the requirements for this project.
| |
| | | | |
| − | This version mainly focuses on lemmas based on unquantified integer linear arithmetic.
| + | Please have a look also at the [[CamilleX User Guide]]. |
| | | | |
| − | == Specification == | + | === Current version === |
| − | A first [[#ancre_2|specification draft]] has been written.
| + | The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the ''CamilleX'' category). Notice that the Soton plug-in update site is now included in the composite Rodin Update Site. |
| | | | |
| − | == Implementation == | + | === Principles === |
| − | A first plug-in prototype is accessible under the following respositories:
| + | The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files. |
| − | * <tt>_exploratory/carinepascal/fr.systerel.decert</tt>
| |
| − | * <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>
| |
| − | | |
| − | The following theories are currently supported: Linear Arithmetic, Linear Order Int and Integer.
| |
| − | | |
| − | == How to perform the translation? ==
| |
| − | | |
| − | The XML files containing the Event-B lemmas are assumed to be stored in the <tt>Lemmas</tt> folder. The SMT files containing the SMT-LIB benchmarks are assumed to be stored in the <tt>Benchmarks</tt> folder. | |
| − | | |
| − | Follow the following steps in order to translate Event-B lemmas to SMT-LIB benchmarks:
| |
| − | <ol>
| |
| − | <li> Launch the <tt>fr.systerel.decert.tests.TypeCheckingTests</tt> JUnit test to type-check the lemmas (optional).
| |
| − | Note that it is previously necessary to set the <tt>XMLFolder</tt> field of the <tt>TypeCheckingTests</tt> class to specify the absolute path of the <tt>Lemmas</tt> folder.
| |
| − | | |
| − | <li> Launch the <tt>fr.systerel.decert.tests.smt.TranslationTests</tt> JUnit test to translate the lemmas (mandatory).
| |
| − | Note that it is necessary to previously configure the test:
| |
| − | * The <tt>XMLFolder</tt> field shall contain the absolute path of the <tt>Lemmas</tt> folder.
| |
| − | * The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.
| |
| − | * If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> field shall contain the absolute path of the directory where is installed the SMT-LIB parser. Otherwise, the option shall be turned off. The SMT-LIB parser is available from the [http://goedel.cs.uiowa.edu/smtlib SMT-LIB web page].
| |
| − | * If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> field shall contain the absolute path of the directory where is installed the Z3 SMT solver. Otherwise, the option shall be turned off. The Z3 SMT solver is available from the [http://research.microsoft.com/en-us/um/redmond/projects/z3 following address].
| |
| − | </ol>
| |
| − | | |
| − | == Bibliography ==
| |
| − | * <font id="ancre_1">DECERT</font>, [http://decert.gforge.inria.fr/index.html ''DEduction and CERTification'']
| |
| − | * C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.
| |
| − | * S. Ranise and C. Tinelli, [http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf <font id="ancre_3">''The SMT-LIB standard''</font>], Version 1.2, 2006, 2006.
| |
| − | | |
| − | [[Category:Design]]
| |
Return to Rodin Plug-ins
The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
Extension to Event-B including the machine inclusion mechanism is also supported.
Please have a look also at the CamilleX User Guide.
Current version
The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the CamilleX category). Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.
Principles
The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.
