Difference between pages "Event-B Indexers" and "Event-B to SMT-LIB"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Pascal
 
Line 1: Line 1:
−
==Purpose==
+
{{TOCright}}
  
−
Event-B indexers populate the index repository. Currently, indexers are implemented for the following files :
+
== Introduction ==
−
* machine (.bum)
+
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.
−
* context (.buc)
 
  
 +
The considered lemmas are those often encountered in practice, but not yet well supported by proving
 +
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.
  
−
==Event-B Occurrence Kinds==
+
This version mainly focuses on lemmas based on unquantified integer linear arithmetic.
  
−
So far, the following occurrence kinds have been defined :
+
== Specification ==
−
* DECLARATION : when a variable, a carrier set, ..., is declared
+
A first [[#ancre_2|specification draft]] has been written.
−
* REFERENCE : when a variable, a carrier set, ..., is referenced (but not modified)
 
−
* MODIFICATION : when a variable is modified (e.g., occurs in the left-hand side of an event action)
 
−
* REDECLARATION : when a variable, parameter or event is redeclared (refined).
 
−
Please notice the distinction between the index repository notion of declaration ({{class|IDeclaration}}) and the Event-B occurrence kind DECLARATION.
 
  
−
==What Is Indexed==
+
== Implementation ==
 +
A first plug-in prototype is accessible under the following respositories:
 +
* <tt>_exploratory/carinepascal/fr.systerel.decert</tt>
 +
* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>
  
−
Currently, indexed elements are :
+
The following theories are currently supported: Linear Arithmetic, Linear Order and Integer. The lemmas referencing other theories will not be translated.
−
* carrier sets
 
−
* constants
 
−
* variables
 
−
* events
 
−
* parameters
 
  
−
Formulas which cannot be parsed are ignored.
+
== How to perform the translation? ==
  
−
In the descriptions below, the following notation will be used to specify locations :
+
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.
−
* [element] : internal location
 
−
* [element/attribute] : attribute location
 
−
* [element/attribute/begin..end] : attribute substring location
 
  
−
===Context Indexer===
+
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.
  
−
====Dependencies====
+
<li> Launch the <tt>fr.systerel.decert.tests.smt.TranslationTests</tt> JUnit test to translate the lemmas (mandatory).
−
* extended contexts
+
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>
  
−
====Declarations====
+
== Bibliography ==
−
* carrier sets
+
* <font id="ancre_1">DECERT</font>, [http://decert.gforge.inria.fr/index.html ''DEduction and CERTification'']
−
* constants
+
* 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.
  
−
====Occurrences====
+
[[Category:Design]]
−
 
 
−
* DECLARATION of carrier sets [CarrierSet/Identifier]
 
−
* DECLARATION of constants [Constant/Identifier]
 
−
* REFERENCE of elements in axioms [Axiom/Predicate/b..e]
 
−
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]
 
−
 
 
−
Example:
 
−
 
 
−
  Ctx
 
−
  Sets
 
−
    S
 
−
  Constants
 
−
    C
 
−
  Axioms
 
−
    axm1 : C ∈ S
 
−
 
 
−
We will end up with the following occurrences :
 
−
 
 
−
  S :
 
−
    DECLARATION in [S/Identifier]
 
−
    REFERENCE in [axm1/Predicate/4..5]
 
−
  C :
 
−
    DECLARATION in [C/Identifer]
 
−
    REFERENCE in [axm1/Predicate/0..1]
 
−
 
 
−
====Exports====
 
−
* imported and declared carrier sets
 
−
* imported and declared constants
 
−
 
 
−
===Machine Indexer===
 
−
 
 
−
====Dependencies====
 
−
* refined machines
 
−
* seen contexts
 
−
 
 
−
====Declarations====
 
−
* variables
 
−
* events
 
−
* parameters
 
−
 
 
−
====Occurrences====
 
−
* DECLARATION of (local) variables [Root]
 
−
* DECLARATION of (local) events [Root]
 
−
* DECLARATION of (local) parameters [Event]
 
−
* REDECLARATION of abstract variables in the local variables that redeclare them [Variable/Identifier]
 
−
* REDECLARATION of abstract events in the local events that refine them [Event/RefinesEvent/Target]
 
−
* REDECLARATION of abstract parameters in the local parameters that redeclare them [Parameter/Identifier]
 
−
* REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
 
−
* REFERENCE of elements in invariants [Invariant/Predicate/b..e]
 
−
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]
 
−
* REFERENCE of elements in variants [Variant/Expression/b..e]
 
−
* REFERENCE of elements in guards [Guard/Predicate/b..e]
 
−
* REFERENCE of elements in witnesses [Witness/Predicate/b..e]
 
−
* REFERENCE of non assigned elements in actions [Action/Assignment/b..e]
 
−
* MODIFICATION of assigned elements in actions [Action/Assignment/b..e]
 
−
 
 
−
Example :
 
−
 
 
−
  M1
 
−
  VARIABLES
 
−
    var1
 
−
  INVARIANTS
 
−
    inv1 : var1 > 0
 
−
  EVENTS
 
−
    INITIALISATION
 
−
      THEN
 
−
        act1 : var1 := 1
 
−
 
 
−
After indexing M1, we will have the following occurrences:
 
−
 
 
−
  M1.var1 :
 
−
    DECLARATION in [M1.Root]
 
−
    REFERENCE in [M1.inv1/Predicate/0..4]
 
−
    MODIFICATION in [M1.act1/Assignment/0..4]
 
−
  M1.INITIALISATION :
 
−
    DECLARATION in [M1.Root]
 
−
 
 
−
Then, if we add another machine
 
−
 
 
−
  M2
 
−
  REFINES
 
−
    M1
 
−
  VARIABLES
 
−
    var1
 
−
  EVENTS
 
−
    INITIALISATION
 
−
      THEN
 
−
        act1 : var1 := 1
 
−
 
 
−
we will add the following occurrences :
 
−
 
 
−
  M1.var1 :
 
−
    REDECLARATION in [M2.var1/Identifier]
 
−
  M2.var1 :
 
−
    DECLARATION in [M2.Root]
 
−
    MODIFICATION in [M2.act1/Assignment/0..4]
 
−
  M2.INITIALISATION :
 
−
    DECLARATION in [M2.Root]
 
−
 
 
−
====Exports====
 
−
* imported carrier sets
 
−
* imported constants
 
−
* local variables
 
−
* local events
 
−
* local parameters
 
−
 
 
−
==Propagation==
 
−
 
 
−
Propagators are defined for :
 
−
* events ({{class|EventPropagator}}) to propagate through refines
 
−
* parameters ({{class|IdentifierPropagator}}) to propagate through redeclaration
 
−
* variables ({{class|IdentifierPropagator}} as well) to propagate through redeclaration
 
−
 
 
−
In the above example with machines M1 and M2, after both files have been indexed, we can query occurrences of M1.var1.
 
−
 
 
−
With no propagator, the result would be :
 
−
 
 
−
  M1.var1 :
 
−
    DECLARATION in [M1.Root]
 
−
    REFERENCE in [M1.inv1/Predicate/0..4]
 
−
    MODIFICATION in [M1.act1/Assignment/0..4]
 
−
    REDECLARATION in [M2.var1/Identifier]
 
−
 
 
−
Using the {{class|IdentifierPropagator}}, the result becomes :
 
−
 
 
−
  M1.var1 (propagated) :
 
−
    DECLARATION in [M1.Root]
 
−
    REFERENCE in [M1.inv1/Predicate/0..4]
 
−
    MODIFICATION in [M1.act1/Assignment/0..4]
 
−
    REDECLARATION in [M2.var1/Identifier]
 
−
    DECLARATION in [M2.Root]
 
−
    MODIFICATION in [M2.act1/Assignment/0..4]
 
−
 
 
−
[[Category:Developer documentation]]
 

Revision as of 15:26, 25 August 2009

Introduction

The Event-B to SMT-LIB plug-in allows to translate mathematical lemmas that rely on the Event-B language to the SMT-LIB format.

The considered lemmas are those often encountered in practice, but not yet well supported by proving 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 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.

Specification

A first specification draft has been written.

Implementation

A first plug-in prototype is accessible under the following respositories:

  • _exploratory/carinepascal/fr.systerel.decert
  • _exploratory/carinepascal/fr.systerel.decert.tests

The following theories are currently supported: Linear Arithmetic, Linear Order and Integer. The lemmas referencing other theories will not be translated.

How to perform the translation?

The XML files containing the Event-B lemmas are assumed to be stored in the Lemmas folder. The SMT files containing the SMT-LIB benchmarks are assumed to be stored in the Benchmarks folder.

Follow the following steps in order to translate Event-B lemmas to SMT-LIB benchmarks:

  1. Launch the fr.systerel.decert.tests.TypeCheckingTests JUnit test to type-check the lemmas (optional). Note that it is previously necessary to set the XMLFolder field of the TypeCheckingTests class to specify the absolute path of the Lemmas folder.
  2. Launch the fr.systerel.decert.tests.smt.TranslationTests JUnit test to translate the lemmas (mandatory). Note that it is necessary to previously configure the test:
    • The XMLFolder field shall contain the absolute path of the Lemmas folder.
    • The SMTFolder field shall contain the absolute path of the Benchmarks folder.
    • If the format of the generated SMT files is to be checked, the CHECK_FORMAT option shall be set and the SMTParserFolder 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 SMT-LIB web page.
    • If the generated benchmarks are to be checked for satisfiability, the CHECK_SAT option shall be set and the SMTSolverFolder 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 following address.

Bibliography

Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_Indexers&oldid=4340’