Difference between pages "Predicate Variables Extension" and "Proof Obligation Commands"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Nicolas
 
Line 1: Line 1:
−
The aim of this extension is to allow defining proof rules for the Rule Based Prover using meta-variables as predicate placeholders.
+
In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:
  
−
For example, one will then be able to write a proof rule involving P and Q directly by using such naming letters.
+
[[Image:PO_Commands.png]]
  
−
For technical reasons (predicates and expressions are distinct syntactic categories), predicate meta-variables are distinguished by a leading symbol '$'.
+
These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).
−
For one given predicate, one wanting to refer to this predicate as P, will write in one's proof rules 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 CSP.
 
−
The choice of the symbol '$' seems to solve such kind of issue.
 
  
−
== Plan to implement this extension in the API ==
+
== Retry Auto Provers ==
  
−
*A. extend the lexer
+
As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).
−
*B. extend the parser
 
−
*C. extend the AST 
 
−
*D. modify visitors, rewriters, filters, etc. according to this extension
 
−
*E. implement new AST tests
 
  
−
== Implementation details ==
+
It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s).
  
−
For B, clients (plug-in contributers) will be allowed to select the mode they want to work with.
+
== Recalculate Auto Status ==
−
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),
+
{{TODO}}
−
  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.
+
== Proof Replay on Undischarged POs ==
−
  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.
+
{{TODO}}
−
In class Formula, two methods are added
 
−
public PredicateVariable[] getPredicateVariables()
 
−
public boolean hasPredicateVariables()
 
  
−
== Further verifications to carry out ==
 
  
−
A verification will follow implementation, in order to check that no side-effect is introduced by this extension.
 
−
The typical unwanted side-effet is that a predicate meta-variable creep into code that was not designed to cope with it.
 
  
−
This verification will be done as follows:  Check each occurrence of the <tt>typeCheck()</tt> method applied to an AST node.  If this call occurs just after a <tt>parsePredicate()</tt> or <tt>parseExpression()</tt> call, then there is no risk of introducing a predicate meta-variable (as it would be ruled out by the parser). In all other cases (especially when receiving an AST object coming from an external reasoner), a check must be added to ensure that the AST tree that is type-checked is also free of predicate meta-variable.
+
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
{{TODO|Category}}

Revision as of 16:56, 4 March 2010

In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:

PO Commands.png

These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).

Retry Auto Provers

As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).

It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s).

Recalculate Auto Status

TODO

Proof Replay on Undischarged POs

TODO










TODO: Category

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