Difference between pages "DEPLOY Plenary Workshop 2009" and "Predicate Variables Extension"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Felix-loesch
 
imported>Tommy
m
 
Line 1: Line 1:
{{TOCright}}
+
This extension will allow people to define proof rules for the Rule Based Prover using meta-variables as predicate placeholders.
  
= DEPLOY Plenary Technical Workshop October 21-23 2009 =
+
For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters.
  
== Call for Papers ==
+
The meta-variables will be identified with the symbol '$'.
 +
For one given predicate, one wanting to refer to this predicate as P, will write in his proof rules, the meta-variable '$P'.
 +
The symbol '?' could be originally chosen to define meta-variables but this revealed to be confusing due to the use of the symbol '?' in the CSP language.
 +
The choice of the symbol '$' seems to solve such type of issue.
  
The second DEPLOY annual plenary meeting will be held this year from 21st to 23rd of October in Aix-en-Provence, France. The main difference with respect to the past meeting will be in a significant amount of time dedicated to technical presentations of conference-like papers.  We invite all the academic and industrial partners to submit papers about the work they carried out inside the DEPLOY project. We expect to have submissions belonging to the following categories and we will give to any of these a space proportional to the number of papers received:
+
== Plan to implement this extension in the API ==
  
# '''Full Original Papers (FOP):''' these works have to be never submitted before to any other workshop/conference/journal but they have to be about ideas that have passed their seminal form. We suggest these papers to be contained in 12 pages LNCS format.
+
*A. extend the lexer
# '''Full Published Papers (FPP):''' these papers can have already been published in any workshop/conference proceedings or journal but the authors intend to submit them again for educative or promotional purposes inside the DEPLOY community. Copyright is not an issue since the work will not be formally published and the presentation will remain internal to the project. We suggest these papers to be contained in 15 pages LNCS format.
+
*B. extend the parser
# '''Short Abstract Papers (SAP):''' these papers present unpublished ideas that are still in their seminal form and want to be presented by the authors to receive feedback before going on with proper full papers. We expect these papers to be presented in a known/unknown form with a number of open questions for discussion. We suggest these papers to be contained in 6 pages LNCS format.
+
*C. extend the AST 
# '''Tool Demo Papers (TDP):''' these papers present works done on tools. A demo is thus expected. We suggest these papers to be contained in 6 pages LNCS format.
+
*D. modify visitors, rewriters, filters, etc. accorded to this extension
 +
*E. implement new AST tests
  
 +
== Implementation details ==
  
== Important Dates ==
+
For B, clients (plug-in contributers) will be allowed to select the mode they want to work with.
 +
Thus, will coexist 2 parsing modes one taking into account predicate variables and the other, the current one, which parses predicates or expressions without predicate variables.
  
* 11/09/09: Submission of papers
+
- the current one available in the current API (FormulaFactory),
* 30/09/09: Notification of acceptance
+
  public IParseResult parsePredicate(String formula, LanguageVersion version,Object origin)
* 15/10/09: Camera-ready paper due
+
  public IParseResult parseExpression(String formula, LanguageVersion version,Object origin)
* 21-23/10/09: DEPLOY Plenary Technical Workshop in Aix-en-Provence
 
  
 +
- a specific one providing the support for predicate variables.
 +
  public IParseResult parsePredicatePattern(String formula, LanguageVersion version,Object origin)
 +
  public IParseResult parseExpressionPattern(String formula, LanguageVersion version,Object origin)
  
== Organizers  ==
+
For C, the class 'PredicateVariable' will be added as a new predicate class.
 +
In the Formula class will be added PredicateVariable[] getPredicateVariables() and boolean hasPredicateVariables() methods.
  
* Manuel Mazzzara - University of Newcastle, UK
 
* Felix Lösch - Robert Bosch GmbH, Germany
 
* Michael Jastram -  Heinrich-Heine-Universität Düsseldorf, Germany
 
* Linas Laibinis - Abo Akademi University, Finland
 
  
 +
== Further verifications to carry out ==
  
== Program Committee ==
+
A verification will follow implementation, in order to check that no side-effects were introduced by this extension. We will trace and verify that no external processing on predicates returns predicates containing predicate variables.
 
+
For example, one must ensure that there isn't no call to the "typeCheck()" method in the platform's code that doesn't follow a call to parsePredicate(). The aim is to verify that no predicate variables remain at the time of the "typeCheck()" call.
The program committee will be anounced soon.
 

Revision as of 10:12, 3 December 2009

This extension will allow people to define proof rules for the Rule Based Prover using meta-variables as predicate placeholders.

For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters.

The meta-variables will be identified with the symbol '$'. For one given predicate, one wanting to refer to this predicate as P, will write in his proof rules, the meta-variable '$P'. The symbol '?' could be originally chosen to define meta-variables but this revealed to be confusing due to the use of the symbol '?' in the CSP language. The choice of the symbol '$' seems to solve such type of issue.

Plan to implement this extension in the API

  • A. extend the lexer
  • B. extend the parser
  • C. extend the AST
  • D. modify visitors, rewriters, filters, etc. accorded to this extension
  • E. implement new AST tests

Implementation details

For B, clients (plug-in contributers) will be allowed to select the mode they want to work with. Thus, will coexist 2 parsing modes one taking into account predicate variables and the other, the current one, which parses predicates or expressions without predicate variables.

- the current one available in the current API (FormulaFactory),

 public IParseResult parsePredicate(String formula, LanguageVersion version,Object origin)
 public IParseResult parseExpression(String formula, LanguageVersion version,Object origin)

- a specific one providing the support for predicate variables.

 public IParseResult parsePredicatePattern(String formula, LanguageVersion version,Object origin)
 public IParseResult parseExpressionPattern(String formula, LanguageVersion version,Object origin)

For C, the class 'PredicateVariable' will be added as a new predicate class. In the Formula class will be added PredicateVariable[] getPredicateVariables() and boolean hasPredicateVariables() methods.


Further verifications to carry out

A verification will follow implementation, in order to check that no side-effects were introduced by this extension. We will trace and verify that no external processing on predicates returns predicates containing predicate variables. For example, one must ensure that there isn't no call to the "typeCheck()" method in the platform's code that doesn't follow a call to parsePredicate(). The aim is to verify that no predicate variables remain at the time of the "typeCheck()" call.