From ClearSy Tools

Contents 1 Versions history 2 Acknowledgements 3 Introduction 4 Principles 5 Refinement Rules 5.1 Concepts 5.1.1 Joker 5.1.2 Identifier 5.1.3 Variable declaration 5.1.4 Expressions 5.1.5 Predicates 5.1.6 Substitutions 5.2 Rule files 5.3 VARIABLES theories 5.4 VARIABLES rules 5.4.1 VARIABLE list of jokers 5.4.2 TYPE identifier (list of variables) 5.4.3 WHEN predicate 5.4.4 IMPORT_TYPE expression 5.4.5 Implementing variables 5.4.6 Refining variables 5.5 OPERATION refinement theories 5.6 OPERATION refinement rules 5.6.1 REFINES substitution 5.6.2 WHEN predicate 5.6.3 REFINEMENT 5.6.4 IMPLEMENTATION substitution 5.6.5 IMPLEMENT list 5.6.6 SUB_REFINEMENT 5.7 INITIALISATION refinement theories 5.8 INITIALISATION refinement rules 5.8.1 REFINES Substitution 5.8.2 WHEN Predicate 5.8.3 IMPLEMENTATION Substitution 5.9 USER_PASS theory 5.10 TACTIC theory 5.10.1 The variable tactics 5.10.2 The substitution tactics 5.11 Constraints on rule files 6 Predefined guards 7 Specific substitutions 7.1 IMPLEMENT 7.2 IMPORTED_OPERATION 7.3 SEEN_OPERATION 7.4 TYPE_ITERATION 7.5 INVARIANT_ITERATION 7.6 CONCRETE_ITERATION 7.7 LH 8 Annotations 8.1 OPERATION_FONC(operation) et MACHINE_FONC(machine) 8.2 CAND 8.3 NOUVELLE_PRE(predicate) and DEPILE_PRE 8.4 MAGIC(theory.rule variable) 8.5 BLACK_MAGIC(theory.rule, variable) 9 Operational specification 9.1 Input paramenters 9.2 Rules and Machines storage 9.3 Variables refinement 9.3.1 Rules search 9.4 Operations refinement 9.4.1 Rules search 9.4.2 Rule application 9.5 Machine refinement decomposition 9.6 Writing general components 9.6.1 Machine header 9.6.2 Clause import 9.6.3 Operation Promotion 9.6.4 Variables 9.6.5 Invariant 9.6.6 Initialisation 9.6.7 Operations 10 Additional requirements 10.1 Adding comments to calling operations 10.2 Rules traceablility 10.3 Generalization with traceable rules 10.4 Headers customization options 10.5 Annotations (pragma) 10.6 SEES addition 11 Extensibility 11.1 Library extension 11.2 New clases addition 11.3 New agrds addition 11.4 Syntatic tree modification 11.5 Decomposition algorithm replacement 11.6 Chossing name algorithm replacement 11.7 Relative independence to BART 12 Annex 1 : complete rule language grammar 12.1 Rule file 12.2 variable refinement rule 12.3 initialization refinement rule 12.4 operation refinement rule 12.5 user pass theory 12.6 tactic theory 12.7 substitutions 12.8 predicates 12.9 expressions

Versions history

ClearSy : Initial version, 31/07/2008

Aryldo G. Russo Jr: French document upload finished, 8/1/2009

Aryldo G. Russo Jr: First draft version in english, 9/1/2009

ClearSy: Review completed 10/03/2009

Acknowledgements

This document was originally written by Antoine Requet and Lilian Burdy (ClearSy).

French to English translation was performed by Aryldo G. Russo Jr (Pesquisa e Desenvolvimento /AeS).

Introduction

This document is the specification of BART (B Automatic Refinement Tool) that allows for generating a B0 implementation from a B machine or a B refinement. BART is composed of an automatic refinement engine and an interactive refinement GUI. This document is only related to the automatic functions.

Principles

This section defines the functionnalities of the tool. Figure n°1 shows the way the tool is behaving. BART inputs are:

• a machine or a refinement
• refinement rules.

It produces a set of B components corresponding to the implementation of this input machine or refinement.

To do that, BART uses refinement rules and possibly annotations added to the input machine, to rewrite it. BART can be considered as a pattern-matcher, as refinement rules are defined in term of patterns and define the way matching terms are transformed. Refinement rules are applied repeatidly applied, generating new machines and/or implementations til one of the two following conditions hold:

• generated components correspond to a translatable B0 implementation. The refinement process is considered as a success.
• No rule can be applied any more. In this case, BART generates machines and display an error message.

Refinement Rules

This section details format and semantics of refinement rules.

Concepts

Joker

A joker corresponds to an element which will be replaced, through parttern-matching, by a part of the machine to convert. Jokers are refered to as "@" caracter followed by a letter. Depending on the context, they can correspond to an expressio, a substitution or a predicate.

The special joker "@_" may be used when the resulting instanciation of the joker is not used.

Identifier

An identifier is composed of several alphanumerics. An identifier could be the name of a variable, constant or operation.

Variable declaration

Within substitutions, BART allows for the implicit declaration of local variables, with the caracter "#" followed by a number. These variables may be refered to in expressions and predicates.

Expressions

Expressions used in BART refinement rule language correspond to B expressions described in the B language reference manual (p35), modified as follow:

• A primary expression may correspond to à joker or a variable, in addition to a hyphened expression, an identifier or a string
• Function composition as well as parallel composition have to be hyphened. For example, f ; g and f || g have to be written as (f ; g) and (f || g).

Predicates

Predicates used in BART correspond to B predicates described in the B language reference manual, modified as follow:

• A predicate may also correspond to a joker or to an implictely declared variable
• A predicate may also correspond to a BART guard. These guards allow for verifying that some conditions are fullfilled.

Substitutions

As for expression and predicates, BART substitutions correspond to those described in the B language reference manual, plus jokers and implicitely declared variables. In the case of refinement patterns, additional substitutions are defined for calling seen or imported operations, and for loops. These additional susbtitutions are defined in chapter 6.

Rule files

Syntax:

RuleFile = [ Theory { "&" Theory } ].

Theory
=
VariableTheory
| OperationTheory
| InitialisationTheory
| UserPassTheory
| TacticTheory
.

Rule file contains a set of theories separated by the ampersand (&) caracter. These theories may be:

• variable theories, containing a set of variable rules
• operation theories, containing a set of operation refinement rules
• initialisation theories, containing a set of initialisation refinement rules
• user pass theory, aimed at selecting rules applicable by BART
• tactic theory, aimed at speeding the rule selection phase

VARIABLES theories

Syntax:

VariableTheory
=
"THEORY_VARIABLE" ident
"IS"
VariableRule { ";" VariableRule }
"END" ident
.

Variable theroies are identified by the keyword "THEORY_VARIABLES" followed by an identifier corresponding to the name of the theory. The keyword "IS" then indroduced a list of variable refinement rules seprated by semicolon. The theory ends up w ith the keyword "END" followed by an identifier. This identifier should be the name of the theory.

VARIABLES rules

Syntax:

VariableRule
=
"RULE" ident ["(" JokerList ")" ]
"VARIABLE" JokerList
[ "TYPE" ident "(" JokerList ")" ]
"WHEN" Predicate
"IMPORT_TYPE" Predicate
(VariableImplementation | VariablesRefinement )
"END"
.

As for all kind of rules, a variable refinement rule has a name and contains a set of clauses, and possibly a set of parameters. A parameterized rule can't be applied directly by BART but needs to be refered to by another rule to be applied (using the REFINED_BY clause for example).

Two kinds of variable refinement rule may be elaborated:

• Variable refinement rule, which introduced new abstract variables which will be implemented by other rules
• Variable implementation rule, which only introduce concrete variables

An exemple of variable refinement rule is given below, where a set is implemented by a total function from elements of this set to booleans:

RULE r_ens
VARIABLE @a
TYPE raffinement_ensemble(@a, @b, @c)
WHEN
    SET(@c) &
    @a <: @c
IMPORT_TYPE
    @a <: @c
CONCRETE_VARIABLE
    @a_r
INVARIANT
    @a_r : @c --> BOOL &
    @a = @a_r~[{TRUE}]
END

Authorized clauses and their semantics are detailed in the next sections.

VARIABLE list of jokers

This clause defines the variable(s) to refine. This clause contains a list of jokers that will be instanciated wih the name of corresponding variables.

TYPE identifier (list of variables)

This optional clause defines a predicate that will be added to refinement hypotheses if the rule is applied. This predicate has the form identifier(list of jokers). It can be then tested in other rules as for a guard.

WHEN predicate

This clause defines the necessary condition to apply a rule. The rule can only be applied if the predicate is true. In this clause, predicate may contains guards, which will not be pattern-matched. In the rule r_ens above, SET(@c) corresponds to a guard verifying that the joker @c corresponds to a set declared in the clause SET of a machine.

IMPORT_TYPE expression

This clause defines the typing invariant that has to be added to generated imported machines when a new machine is generated, et when variables are not yet implemented.

Implementing variables

Syntax:

VariableImplementation =
"CONCRETE_VARIABLES" JokerList
[ "DECLARATION" Predicate ]
"INVARIANT" Predicate
.

The implementation of variable allows to define the list of variables replacing the variables present in the clause VARIABLE, and the corresponding invariant.

First of all, the clause CONCRETE_VARIABLES sets the concrete variables to replace the variables listed in the clause VARIABLES. Its content is a list of identifiers or jokers .

Then, the optional clause DECLARATION allows to declare SETS which will be defined in the machine implementing the variable. It contains a predicate that corresponds to a declaration of these sets.

Finally, the clause INVARIANT describes the part of the invariant that corresponds to the concrete variables that were introduced. This clause contains a predicate that will be copied in the machine implementing the variables, and which must also contain the type of variables as well as the gluing invariant. (TL: verified OK ).

Refining variables

Syntax:

VariablesRefinement =
"REFINEMENT_VARIABLES"
VariableRefinement { "," VariableRefinement }
"GLUING_INVARIANT" Predicate
.

VariableRefinement =
"CONCRETE_VARIABLE" joker
"WITH_INV" Predicate
"END"
| "ABSTRACT_VARIABLE" joker
"REFINED_BY" ident "(" Expression ")"
"WITH_INV" Predicate
"END"
.

The refinement rules are more complex than the implementation ones. These rules have a list of variables refinements describing each variable that were introduced and its refinement.

Each variable introduced is defined by the clause CONCRETE_VARIABLE or ABSTRACT_VARIABLE followed by a joker defining the name of the variable.

In the case where the variable introduced is an abstract variable, the clause REFINED_BY allows to specify the refinement rule to be used to refine this new variable.

Finally, the clause WITH_INV introduces the typing invariant of the variable.

When all the variables are declared, the clause GLUING_INVARIANT makes precises the gluing invariant that will be introduced during the refinement.

Note that refinement rules allow to specify the whole implementation rules. For example, the implementation rule (Figure 2) is equivalent to the refinement rule (Figure 3).

RULE r_ens
VARIABLE @a
TYPE raffinement_ensemble(@a, @b, @c)
WHEN
SET(@c) &
    @a <: @c
IMPORT_TYPE
    @a <: @c
REFINEMENT_VARIABLES
CONCRETE_VARIABLE
    @a_r
WITH_INV
    @a_r : @c --> BOOL &
END
GLUING_INVARIANT
    @a = @a_r~[{TRUE}]
END

Figure 3: refinement rule corresponding to the previous implementation rule

OPERATION refinement theories

Syntax:

OperationTheory 
=
"THEORY_OPERATION" ident
"IS"
OperationRule { ";" OperationRule }
"END" ident
.

The format of theories of operations is similar to that of the theories of variables, except that these theories contain rules specifying how to refine substitutions by other substitutions. The next section details the content of the rules of refinement of operations.

OPERATION refinement rules

Syntax:

OperationRule
=
"RULE" ident
"REFINES" Substitution
[ "WHEN" Predicate ]
[ "SUB_REFINEMENT" SubRefinementRule { "," SubRefinementRule } ]
( "REFINEMENT" { RefinementVarDecl } Substitution
| "IMPLEMENTATION" Substitution
)
[ "IMPLEMENT" IdentOrJokerList ]
"END"
.

The operation refinement rules describe how to refine or implement substitutions. An example of rule is given Figure 4.

RULE exemple
REFINES
@a := @a - {@b}
WHEN
raffinement_ensemble (@a, @_, @_)
REFINEMENT
#1 := @b ;
IMPLEMENT (@a_r (#1) := FALSE)
IMPLEMENT
@a
END

Figure 4: example of an operation refinement rule

This rule indicates how an element can be removed from a set when the refinement of this set was made by the refinement rule given Figure 2. As for the variable refinement rule, the operation refinement rules begin withthe key word "RULE" followed by an identifier corresponding to the name of the rule. The various clauses accepted are now detailed.

REFINES substitution

This clause defines the form of substitutions that this rule can refine. To be able to apply this rule in a subtitution refinement, the first constraint is that the substitution could be pattern-matched with the substitution pattern provided in this clause

WHEN predicate

This optional clause indicates the necessary conditions for the application of the rule. Thus, a rule can be applied only if the substitution given in the clause REFINES matches with the substitution to be refined, and if the predicate given in the WHEN clause is valid. In the example Figure 4, the content of the WHEN clause ensures that the variable refinement rule used to refine @a is the given rule Figure 2.

REFINEMENT

Syntax:

"REFINEMENT" { RefinementVarDecl } Substitution
RefinementVarDecl =
"VARIABLE" joker
[ "REFINED_BY" ident "(" Expression ")" ]
"WITH_INV" Predicate
"WITH_INIT" Substitution
"IN"
.

This clause allows to define the substitution to replace the refined substitution. It contains an optional suite of abstract variable declarations, followed by the substitution corresponding to the refinement of the substitution present in the clause REFINES.

Thus, in the example Figure 4, no new variable is declared, and the removal of the element of the set is translated into affecting @b to a new local variable #1, and the indication that the image of this variable by the function @a_r is «FALSE » is given. The particular substitution IMPLEMENT is used here to indicates that « @a_r (#1) := FALSE » corresponds to an implementation. Thus, it will not be necessary to refine the substitution.

In the case of more complex refinements, it may be useful to introduce new abstract variables. The statements of abstract variables are in this clause before the substitution.

Each declaration of variable contains the following clauses:

• VARIABLE joker: joker corresponds to the name of the variable
• REFINED_BY ident(expression): this optional clause allows to indicate the rule to be used to refine the variable newly introduced, as well as the parameters for this rule.
• WITH_INV predicate: this clause defines the corresponding predicate to the invariant of type of the new variable introduced.
• WITH_INIT substitution: this clause defines the substitution to be used for the initialization of the new variable.

IMPLEMENTATION substitution

This clause is similar to the clause REFINEMENT, except that it does not allow to introduce new variables. It provides the substitution to replace the substitution given in the clause REFINES.

IMPLEMENT list

This clause allows to list the set of variables to be implemented in order to apply the rule. In the example Figure 4, the variable @a is listed: indeed, in order to referencing the variable @a_r, it is necessary that the variable @a is implemented.

SUB_REFINEMENT

Syntax:

"SUB_REFINEMENT" SubRefinementRule { "," SubRefinementRule }
SubRefinementRule =
"(" Substitution ")" "->" "(" Joker ")"
.

This optional clause allows you to force the refinement of sub-elements, and to instantiate new jokers as a result of this refinement. This clause contains a set of sub-refinements separated by commas. Each sub-refinement indicates the substitution to refine, followed by the corresponding joker to the result of refinement. Thus, the given rule in Figure 5 uses a sub-refinement to indicate that refine a substitution IF consists in refining the substitution it contains.

RULE raffinement_if
REFINES
IF @a THEN @b END 
SUB_REFINEMENT
(@b) -> (@d)
REFINEMENT
IF @a THEN @d END
END

INITIALISATION refinement theories

Syntax:

InitialisationTheory
=
"THEORY_INITIALISATION" ident
"IS"
InitialisationRule { ";" InitialisationRule }
"END" ident
.

The initialization refinement theories have a list of initialization refinement rules separeted by semicolon. Like others theories, each theory is named and finishes with the « END » keyword followed by the theory name. The next section details the content of the operation refinement rules.

INITIALISATION refinement rules

Syntax:

InitialisationRule
=
"RULE" ident
"REFINES" Substitution
[ "WHEN" Predicate ]
"IMPLEMENTATION" Substitution
"END"
.

The initialization rules describe how to refine the initialization clause of B machines. An example of this can be seen in figure 6.

RULE init_ensemble 
REFINES 
@a := @b
WHEN
raffinement_ensemble(@a,@b,@c)
IMPLEMENTATION
@a_r := @c*{TRUE}
END

They are very close of the operation rules described in the next section. The keyword « RULE » is followed by the name of the rule, and followed by a set of clauses. The clauses accepted are described below.

REFINES Substitution

This clause defines the type of substitution refined by the rule. The rule may be applied for the substitutions « pattern-matching » the substitution defined in this clause.

WHEN Predicate

The predicate of this optional clause defines the necessary conditions for the application of the rule. Thus, the rule may only be applied if:

• The refined substitution corresponds to the substitution of the clause REFINES
• The predicate in the WHEN clause may be evaluated to true.

IMPLEMENTATION Substitution

This clause gives the refined substitution, corresponding to the refinement of the substitution given in the clause REFINES

USER_PASS theory

Syntax:

UserPassTheory = "USER_PASS" "IS"
[ ("VARIABLE"|"OPERATION"|"INITIALISATION") ":" "(" IdentList ")" ]
{ ";" ("VARIABLE"|"OPERATION"|"INITIALISATION") ":" "(" IdentList ")" }
"END"

This optional theory allows to restrict the use of rules, defined in the file, to the rules in the specified theories. If the theory USER_PASS is not present, all the rules may be applied. This theory contains three lists of rules (VARIABLE, OPERATION and INITIALIZATION) corresponding respectively to the variables, operations, and initializations theories.

These clauses are followed by a list of identifiers corresponding to name of the theories that can be used . All the referenced theories must be theories defined in the same file, and must correspond to theories of the same type. For example, the clause VARIABLE cannot reference operation refinement theories.

TACTIC theory

Syntax:

theory_tactic = "THEORY" "TACTICS" "IS" { tactic } "END".
tactic =
"VARIABLE" ":" variable_tactic { ";" variable_tactic }
| "INITIALISATION" ":" substitution_tactic { ";" substitution_tactic }
| "OPERATION" ":" substitution_tactic { ";" substitution_tactic }
.

The TACTIC theory contains a set of rules intended to simplify rule searching by BART. It contains three types of clauses corresponding to different types of theories:

• The clause VARIABLE, allowing to guide the choice of variable refinement rules.
• The clause OPERATION, for the choice of operation refinement rules.
• The clause INITIALIZATION, for the choice of initialization rules.

These clauses are followed by the separator « : » and a list of tactics separated by a semicolon. The tactics for variables are followed by a list of tactics of variables, and tactics for operations and initializations are followed by a list of substitution tactics. The tactics contain a pattern and a list of theory names, and allow to restrict rule searching to the rules defined in these theories for the refinement of elements corresponding to the pattern. Different types of tactics are described below.

The variable tactics

Syntax:

variable_tactic =
ident_list "=>" "(" predicat ")"
.

A tactic for variables corresponds to a list of names of variable refinement theories, followed by « => » and an expression between brackets. This tactic indicates that only the theories contained in the list must be taken into account for the refinement of variables, for which the invariant corresponds to the given expression in parameter.

The substitution tactics

Syntax:

substitution_tactic =
ident_list "=>" "(" substitution")"
.

These tactics are used for the operations and initializations tactics. They consist in a list of name of theories followed by the separator « => » and a pattern of substitution between parentheses. They indicate the list of theories to be taken into account during the refinement of a substitution corresponding to the pattern of the tactics.

Constraints on rule files

BART performs the following checks on the files of theories, and display an error message when at least one of these constraints is not respected.

• The identifier after the keyword END of a variable, operation, and initialization theory must be the same as the name of the theory.
• The theories TACTIC and USER_PASS must appear at once in each file of rules.
• The USER_PASS theory must contain at most one instance of each clause VARIABLE, OPERATION and INITIALIZATION.
• The theories referenced in the USER_PASS theory must be of theories of type referenced defined in the same file of rules.
• The tactics of variables must not refer to theories of refinement of existing variables and defined in the same file.
• The tactics of initializing should refer to theories of refinement of initializations existing and defined in the same file.
• Only the clauses IMPLEMENTATION AND REFINEMENT of the rules of refinements of operations and of initializations may contain specific substitutions BART.
• Several rules may not have the same name within the same theory.
• Several theories of the same type may not have the same name.
• Only the clauses WHEN, VARIABLES, and REFINES allow to introduce new jokers.

Predefined guards

The WHEN clause of the refinement rules may contain « guards » not used to define the pattern of the rule, but to verify that the rule may apply. These guards allow to express rule pre-conditions. The table below lists the various guards that are recognized by BART. This list is not exhaustive, future extensions may add new guards.

Guard	Condition
SET(expression)	expression Is a set defined in the SET clause of a machine
ENUM(expression)	expression Correspond to an enumerated set
COCON(expression)	expression Is a concrete constant
ABCON(expression)	expression Is an abstract constant
COVAR(expression)	expression Is a concrete variable
ABVAR(expression)	expression Is an abstract variable
VAR_G(expression)	expression Is a global variable(concrete or abstract)
PAR_IN(expression)	expression Is an input parameter of an operation
PAR_OUT(expression)	expression Is an output parameter of an operation
match(joker, expression)	Always TRUE. Used for instantiate a joker with an expression
bnot(predicate)	True if the predicate in parameter is not true. This guard does not use the prover of Atelier B, but performs the search in the hypothesis
bident(expression)	TRUE if the expression is an identifier
bnum(expression)	TRUE if the expression is a number
bpattern(f, g)	TRUE if f maches with g, G is supposed to not be instantiated. jokers of g are then instantiated.
bistrue(predicate)	true if the predicate is on the current hypothesis stack
bisfalse(predicate)	TRUE if not(predicate) is on the current hypothesis stack
bsearch(a | b | joker)	The substitution a is present in the substitution b. In this case, the joker is instantiated with b in which the occurrence of a is deleted.
PR(predicate)	Predicate is discharged by the predicate prover of Atelier B.
FREE(joker, expression)	Joker is free in expression.
REFINED(joker list)	Joker list contains only refined variables
B0EXPR(expression)	expression is a B0 expression.

Specific substitutions

The clauses IMPLEMENTATION AND REFINEMENT of the operations and initialization refinement rules allow the use of specific substitutions not already existing in B. These substitutions are specially treated by BART, and will be translated in the form of classical B substitutions in the generated machines. The various BART specific substitutions are described in this section.

IMPLEMENT

Syntax:

ImplementSubstitution = "IMPLEMENT" "(" Substitution ")".

The substitution IMPLEMENT is reflected in the resulting machine as the substitution in parameter. Its role is to assert that the substitution in parameter has no need to be refined. Thus, the substitution IMPLEMENT(a:= 1) will be translated by a:=1 in the machine refined.

IMPORTED_OPERATION

Syntax:

"IMPORTED_OPERATION" "("
[ "name" "=>" ident "," ]
"out" "=>" "(" [ IdentJokerVardeclList ] ")" ","
"in" "=>" "(" [ IdentJokerVardeclList ] ")" ","
"pre" "=>" "(" Predicate ")" ","
"body" "=>" "(" Substitution ")"
")"

The substitution IMPORTED_OPERATION allows to declare a new operation to be defined in an imported machine. The different parameters for this substitution allow to define the specification of the created operation:

• Name: this optional parameter allows you to give a name to the operation. If this parameter does not appear, a name is calculated automatically. The name given may however be changed in order to make it unique.
• Out: output parameters of the operation
• in: input parameters of the operation
• pre: predicate to be included in the pre-condition of the operation
• body: substitution corresponding to the body of the operation

In the refined machine, substitution is reflected by an operation call, the operation is defined as a new operation in a imported machine. The pre-condition of this new operation is calculated as the combination of:

• The pre-condition of the current operation and its abstractions.
• The pre-condition calculated from the fcontrol flow in the current operation (possibly modified by the annotations DEPILE_PRE and EMPILE_PRE).
• The content of the parameter pre.

The whole of the pre-condition calculated nevertheless will not necessarily be included as precondition for the operation: only the part on existing variables in the machine will be retained.

SEEN_OPERATION

Syntax:

"SEEN_OPERATION" "("
"name" "=>" IdentOrJoker ","
"out" "=>" "(" [ IdentJokerVardeclList ] ")" ","
"in" "=>" "(" [ IdentJokerVardeclList ] ")" ","
"body" "=>" "(" Substitution ")"
")"

The substitution SEEN_OPERATION allows to insert a call to a machine defined in a seen machine The parameters are defined as follows:

• name: the name of the operation
• out: the output parameters of operation
• in: the input parameters of the operation
• body: the body of the operation

The substitution SEEN_OPERATION will thus be converted into an operation call.

TYPE_ITERATION

Syntax:

"TYPE_ITERATION" "("
[ ("tant_que"|"while") "=>" IdentOrJokerOrVarDecl "," ]
"index" "=>" Expression ","
"type" "=>" Expression ","
"body" "=>" "(" Substitution ")" ","
"invariant" "=>" Predicate
")"

The special substitution TYPE_ITERATION simplifies the writing of loops by the use of iterators abstract. It allows to scan the whole of the elements of a given set. The different parameters for this substitution are the following:

• While, tant_que: the iteration continues as long as the variable in parameter is true. This parameter allows to stop the iteration before all the elements have been driven. For this, the variable must be put to false in the treatment.
• Index: corresponds to the variable which will receive each element
• type: the set to go. The latter must respond to a constant.
• Body: the treatment to be performed on each of the elements
• invariant: the loop invariant

This substitution creates a machine of iterator which will be imported in the machine refined. This machine of iterator corresponds to the given machine Figure 9. In this figure, the words in italics correspond to the elements which will be replaced by the parameters of the iterator.

vg_loop <-- init_iteration_TYPE;
WHILE vg_loop = TRUE DO
vg_loop, index <-- continue_iteration_TYPE;
body
INVARIANT
vg_loop= bool(TYPE_remaining /= {}) &
TYPE_remaining \/ TYPE_done = TYPE &
TYPE_remaining /\ TYPE_done = {} &
invariant 
VARIANT
card(TYPE_remaining)
END

Similarly, the figure figure 8 gives the translation of the substitution in the machine refined in the case when no while condition has been given. The translation in the case or a condition while has been given is indicated Figure 10.

MACHINE
 nom_iterateur
ABSTRACT_VARIABLES
 TYPE_remaining, TYPE_done
INVARIANT
 TYPE_remaining <: TYPE &
 TYPE_done <: TYPE &
 TYPE_remaining /\ TYPE_done = {}
INITIALISATION
 TYPE_remaining := {} ||
 TYPE_done := {} 
OPERATIONS
 continue <-- init_iteration_TYPE = 
 BEGIN
  TYPE_remaining := TYPE
  TYPE_done := {}
 END;
 continue, elt <-- continue_iteration_TYPE =
 PRE
  TYPE_remaining /= {}
 THEN
  ANY
   nn
  WHERE
   nn : type de TYPE &
   nn : TYPE &
   nn : TYPE_remaining
  THEN
   TYPE_done := TYPE_done \/ {nn} ||
   TYPE_remaining := TYPE_remaining - {nn} ||
   elt := nn ||
   continue := bool(TYPE_remaining /= {nn})
  END
 END
END

vg_loop <-- init_iteration_TYPE;
WHILE vg_loop = TRUE DO
vg_loop, index <-- continue_iteration_TYPE;
body ;
vg_loop := bool(vg_loop = TRUE & while = TRUE)
INVARIANT
vg_loop= bool(TYPE_remaining /= {}) &
TYPE_remaining \/ TYPE_done = TYPE &
TYPE_remaining /\ TYPE_done = {} &
invariant 
VARIANT
card(TYPE_remaining)
END

INVARIANT_ITERATION

Syntax:

"INVARIANT_ITERATION" "("
[ ("tant_que"|"while") "=>" IdentOrJokerOrVardecl "," ]
"1st" "index" "=>" Expression ","
"2nd" "index" "=>" Expression ","
"constant" "=>" Expression ","
"1st" "type" "=>" Expression ","
"2nd" "type" "=>" Expression ","
"body" "=>" "(" Substitution ")" ","
"invariant" "=>" "(" Predicate ")"
")"

The special substitution INVARIANT_ITERATION is another way to simplify the writing of loops. Contrary to the substitution TYPE_ITERATION, which iterated on a set defined by a type, iteration is done here on the image of an element of a relationship. The parameters are defined as follows:

• Tant_que, while: provides a variable to stop the iteration before all the elements are travelled.
• Constant: defines the relationship on which the iteration will proceed
• 1st index: provides the element of origin of the iteration. THE iteration will focus on the elements constant[{1st index }]
• 2nd index: the element which will receive the current element in the loop
• 1st type: the type of elements present in the domain of the constant
• 2nd type: the type of elements present in the image of the constant
• body: the treatment carried out in the loop on the current element
• invariant: the invariant of the loop

vg_loop <-- init_iteration_CONSTANT(index1);
WHILE vg_loop = TRUE DO
vg_loop, index2 <-- continue_iteration_CONSTANT(index1);
body ;
vg_loop := bool(vg_loop = TRUE & while = TRUE)
INVARIANT
vg_loop = bool(CONSTANT_remaining /= {}) & 
CONSTANT_remaining \/ CONSTANT_done = CONSTANT[{index1}]
CONSTANT_remaining /\ CONSTANT_done = {} &
invariant
VARIANT
card(CONSTANT_remaining)
END

From these information, substitution is translated as given Error: Reference source not found and Figure 12, according to the presence or absence of a field "while". The corresponding iteration machine is given Figure 13.

vg_loop <-- init_iteration_CONSTANT(index1);
WHILE vg_loop = TRUE DO
vg_loop, index2 <-- continue_iteration_CONSTANT(index1);
body
INVARIANT
vg_loop = bool(CONSTANT_remaining /= {}) &
CONSTANT_remaining \/ CONSTANT_done = CONSTANT[{index1}]
CONSTANT_remaining /\ CONSTANT_done = {} &
invariant
VARIANT
card(CONSTANT_remaining)

MACHINE
 nom_iterateur
ABSTRACT_VARIABLES
 CONSTANT_remaining,
 CONSTANT_done
INVARIANT
 CONSTANT_remaining <: ran(CONSTANT) &
 CONSTANT_remaining <: TYPE2 &
 CONSTANT_done <: TYPE2 &
 CONSTANT_remaining /\ CONSTANT_done = {}
INITIALISATION
 CONSTANT_remaining := {} ||
 CONSTANT_done := {}
OPERATIONS
 continue <-- init_iteration_CONSTANT(elt) =
 PRE
  elt : TYPE1
 THEN
  CONSTANT_done := {} ||
  CONSTANT_remaining := CONSTANT[{elt}] ||
  continue := bool(CONSTANT[{elt}] /= {})
 END;
 continue, elt <-- continue_iteration_CONSTANT=
 PRE
  CONSTANT_remaining /= {}
 THEN
  ANY
   nn
  WHERE
   nn : TYPE2 &
   nn : CONSTANT_remaining
  THEN
   CONSTANT_done := CONSTANT_done \/ {nn} ||
   CONSTANT_remaining := CONSTANT_remaining - {nn} ||
   elt := nn ||
   continue := bool(CONSTANT_remaining /= {nn})
  END
 END
END

CONCRETE_ITERATION

Syntax:

"CONCRETE_ITERATION" "("
"init_while" "=>" "(" Substitution ")" ","
("tant_que"|"while") "=>" Expression ","
"body" "=>" "(" Substitution ")" ","
"invariant" "=>" "(" Predicate ")" ","
"variant" "=>" Expression ","
"flag" "=>" IdentOrJoker
")"

The clause CONCRETE_ITERATION is translated into WHILE loop without the use of machine of iteration. The translation in B substitution of this substitution is given Figure 14.

init_while;
vg_loop := bool( while );
WHILE vg_loop = TRUE DO
 /*? Flag iteration: flag ?*/
 body ;
 vg_loop := bool( while )
INVARIANT
 invariant
VARIANT
 variant
END

LH

Syntax:

"LH" Predicate "THEN" Substitution "END"

This substitution used in the rules of refinement and implementation allows to introduce locally new hypothesis. The substitution LH is not translated in B substitution by BART, but it affects the translation of substitution in parameter: it adds the predicate to hypothesis of BART during the refinement of the substitution

Annotations

In addition to the rules of refinement, BART can take advantage of annotations (pragma) present in the specification B. These annotations are in the form of special comments starting by /* pragma_b . The content of any comment of this form must be loaded by the tool, even if it is not listed in this specification. In effect, extensions of BART may require the use of new pragmas

OPERATION_FONC(operation) et MACHINE_FONC(machine)

These annotations allow to modify the manner in which the clause ANY is refined. They must be located just after the key word "ANY". The annotation OPERATION_FONC(operation) allows you to indicate the name of a operation to evaluate the variables declared in this clause ANY. name must correspond to a transaction as defined in a machine view having the same number of output parameters that the number of variables defined in the clause ANY. The annotation MACHINE_FONC allows to define the machine where the operation is defined.

CAND

This annotation has the characteristic of not respecting the format /* pragma_b. It is note in effect /*CAND */. It must be placed just after a and (« & »), and indicates that this "and" is a "and" conditional.That is to say that the following expression must not be assessed if the previous condition is not true.

NOUVELLE_PRE(predicate) and DEPILE_PRE

These annotations are used in the substitutions presenting cases, such as IF or SELECT to change the way in which the pre-conditions of operations imported are generated. By default, the assumptions corresponding to the current branch of the substitution are added to the preconditions. In such a branch, the annotation NOUVELLE_PRE allows to replace the corresponding hypothesis for the predicate past in parameter. Thus in the example given Figure 15, at the call of the operation f, the pre-condition calculated would be "aa = 3". However, the use of the annotation NOUVELLE_PRE replaces this pre-condition by "aa < 10". In the same way, at the call of the operation g, the pre-condition calculated should be "not(aa = 3)," however the annotation DEPILE_PRE removes this hypothesis. The pre-condition calculated is therefore empty.

IF aa = 3 THEN
 /* pragma_b NOUVELLE_PRE(aa < 10) /
 f(aa)
ELSE
 /* pragma_b DEPILE_PRE */
 g(aa)
END

MAGIC(theory.rule variable)

This annotation force the use of a special rule for the refinement of variable. Before using this rule, BART verifies that the rule may actually be used in verifying its WHEN clause.

BLACK_MAGIC(theory.rule, variable)

As the annotation MAGIC, this annotation imposes the use of a special rule for the refinement of variable. However, unlike the annotation MAGIC, the validity of the rule is not checked when the annotation BLACK_MAGIC is used.

Operational specification

Input paramenters

BART takes as parameter at least three elements:

• a project name of Atelier B
• a machine or refinement name
• a rules database to use

The name of the Atelier B project must correspond to a project containing the component passed in parameter. It is used to retrieve and analyze the different components referenced by the component in parameter.

The rules database to use may be given implicitly. In particular, it must be defined as a global database, containing the rules of general refinement, automatically loaded.

Similarly, a file bearing the same name as the component refined, present in the same directory, and extension ".rmf » must be considered as a rule databese priority compared to the global database.

Rules and Machines storage

In the first moment, BART loaded into memory the set of rules as well as the machine to refine and the machines that it reference (machines views and the possible abstractions). From the machines read, BART built a list of assumptions associated with this machine. These assumptions shall contain:

• The invariant and content of the clause PROPERTIES of the machine refined.
• The invariant and content of the clause PROPERTIES of the possible abstractions of machine refined.
• The invariant and content of the clause PROPERTIES of the machines views by the machine refined.

These hypothesis are then used in the rules search.

Variables refinement

or each abstract variable, BART search in the rules of refinement of variables a rule that can be applied to this variable. The rule may be found in three different ways:

• Either an annotation MAGIC provides the rule to use as well as its possible parameters. In this case, BART verifies the validity of the WHEN clause, and displays an error message if the rule cannot be applied.
• Either an annotation BLACK_MAGIC provides the rule to use as well as its possible parameters. In this case, the rule is accepted, as-it-is.
• Either no annotation imposes no rules. In this case, the rule is sought in the set of rules, seeking to instantiate the WHEN clause on hypothesis.

If no rule is found for one or several variables, BART leaves and displays an error message indicating the relevant variables. Otherwise, for each of the rules found, the content of the clause TYPE, with the jokers instantiated is added to the hypothesis.

Rules search

For a given variable, in the case or the rule of refinement of variables must be sought, the rule is sought in the whole of the files of rules, beginning with the last passed in parameter. Thus, the first file used for research corresponds to the file .rmf of the same name that the component, if it exists, and the last file used corresponds to the basis of rules global. This behavior allows to provide a basis of a general rule, and of the overload for specific needs.

For each of the rule files, BART determines the list of theories to take into account:

• If the file contains a TACTIC theory, and that this theory contains a clause VARIABLE, the hypothesis are pattern-matched with the rules of this theory. If one or more rules correspond, theories to take into account correspond to theories listed in these rules. The theories are taken into account in reverse order of appearance. Thus, if several rules correspond, the rules placed at the end of the tactics are priority on those placed at the beginning of the tactics.

• If the file contains a USER_PASS theory and that this theory contains a clause VARIABLE, theories to take into account correspond to theories listed in this clause. As for the theory TACTIC, The theories are taken into account in reverse order of appearance.

• Otherwise, the set of the theories of refinement of variable non-parametric present in the file are taken into account. The theories are sought in reverse order of their appearance in the file. Thus, the theories end of the file are priority on the theories in the beginning of file.

For each theory, the rules are then sought one by one, starting with the last rule in the theory. To test if the rule is applicable, BART uses the content of clauses VARIABLE, and WHEN. For this, the joker corresponding to the clause VARIABLE is forum on behalf of the variable sought.

BART then seeks to pattern-matching the content of the WHEN clause not corresponding of guards on the hypothesis.

• If it is possible to pattern-matching the WHEN clause on hypothesis, the guards present in the WHEN clause are tested. If the whole of guards is valid, the rule of refinement will be used to refine the variable, and the search can stop.
• Otherwise, the following rule is tested.

Operations refinement

For each operation, BART search the rules of refinement of operations which may be applied, applies these rules, and repeat this operation on the results to that no rule can no longer be applied. At every stage, the rule used is stored, generating a tree of rules. In the case where a rule of refinement introducing abstract variables is applied, the rules of refinement to use to refine these new variables are sought as soon as described in the previous section.

In the case wehre the application of the rule generates new operations, these operations are incorporated in the tree of rules, under the implementation of the rule, and refined in the same way. In the output of this phase, for each operation, BART calculated a tree of application of rules corresponding to the refinement of this operation. An example of tree for a machine containing two operations opi and op2 is given Figure 11.

The initializations are refined in a similar manner, using the rules of initializations as well as the rules of refinement of operations.

Rules search

The search of rules of refinement of substitution is effected in a similar way refinement of variables: to search for the refinement of a substitution, the search is carried out in the set of rules files, starting with the last file.

During the search, the content of the possible pre-condition of the operation is added temporarily from the hypothesis. The same way, if the substitution for refining is located in one of the cases of a IF or a SELECT, the corresponding hypothesis (condition of IF or denial of the condition) are added. The same way, the hypothesis are update for the other substitutions such as ANY, LET or ASSERT.

In a rule file, the list of theories to examine is built:

• Either through the clause OPERATION of a theory TACTIC. In this case, the theories in which the rules will be sought correspond to theories for which the substitution to refine match with the pattern.
• Either through the clause OPERATION of a theory USER_PASS. In this case, the theories in which the rules will be sought correspond to theories listed.
• Either by looking in the set of theories of operation (and initialization in the case of initializations) present in the file.

Then, the rule is sought in the theories listed. For each theory, research is done by starting at the last rule of the theory.

To check if the rule may apply, the content of the clause REFINES is first of all pattern-matched with the substitution to be refined. Then, in the case or the pattern-matching successful, the WHEN clause is verified in the same way as to the rules of variables. To know, the content of this clause not corresponding of the guards is pattern-matched with the hypothesis, and the guards are then evaluated.

In the case where the rule does not correspond, the following rule is tested until all the rules of the theory are tested. The search continues then to the following theory.

Rule application

When a rule is found, it must be applied prior to reiterate the search. For this, the content of the substitution refined is replaced by the content of the clause REFINEMENT. In the case or a transaction is generated, as in the case or the clause REFINEMENT contains a substitution IMPORTED_OPERATION, the pre-condition of the operation generated is calculated from:

1. The set of pre-conditions of the operation and its abstractions 2. The local hypothesis to the refined substitution (for example the hypothesis corresponding to the current branch in a IF). These may be modified by the annotations EMPILE_PRE and DEPILE_PRE

The pre-condition of the operation generated then corresponds to the whole of these assumptions, restricted to the assumptions relating only to existing variables in the machine generated.

Machine refinement decomposition

Once that each operation is refined entirely, for each operation, BART obtains a tree corresponding to the rules of refinement applied.

In order to write B machines and implementations correct, it is necessary to decompose the refinement in different machines and implementations. This decomposition corresponds to introduce new abstract machines at the refinement. Thus, to implement a machine M, it is not necessarily possible to use a only implementation M_i implementing M.

For example, the rules of refinement used may introduce new operations. To be declared in a new abstract machine. In this case, it will write a machine M1 defining these new operations, and an implementation M_i implementing M and importing M1. In the same way, implement M1 can require the introduction of a new machine M2.

This decomposition can be necessary because of the rule applied, for example when a new variable is introduced, but also to simplify the proof.

The objective of this step is to determine, from the rules of refinement selected in the previous step, the different machines M_i, Mx, Mx_i to be written and their contents. The content of machines is determined from the implementations: the content of the machine Mn is determined from the implementation M_in-1. The content of the implementation M_i is when with its results of the application of the rules of refinement. The decomposition is therefore determine a set of components Mn and M_in sufficient to apply the rules of refinement built in the previous step, and to allocate these rules on the different components in order to obtain machines B correct.

To carry out this decomposition, you can decompose the rules in three types of rules:

• The rules requiring to introduce a refinement or an implementation. Thus, the rules containing a clause IMPLEMENT impose the creation of an implementation or a refinement.
• The rules requiring the introduction of a new abstract machine immediately after the application of the rule. These rules correspond to the rules introducing new operations imported. These rules also require the creation of an implementation important the machine newly created.
• The rules not showing constraints of decomposition specific as for example, a rule turning a substitution in another substitution equivalent on the same variables.

The decomposition is to cut the tree of application of rules generated at the previous step in a manner to involve a machine of destination to each rule, in ensuring that, for each variable refined, either the variable refined, either the or variables of refinement appears in the machine, but not the two. For that, after the application of each rule, one can determine the list of variables to be present in the machine, and those which must no longer be present.

Figure 17 presents an example of tree of rules for a machine M containing two variables abstract v1 and v2, two operations opi and op2. At the side of each rule, the variables to be present after application of the rule are noted. The rules R2, R3 and R7 in red on the figure correspond to the rules requiring the immediate introduction of a new machine.

As regards the refinement of the operation op1, the rules R1, R2 and R3 can be grouped in the same machine, containing variables v1 and v2_r. The rules R4 and R5, require a new machine implementing the variables v1_r and v2_r. Independently, for the operation op2, the rules R6 and R7 may be grouped in a machine containing the variable abstract v2, the application of R8 being separated in a second machine implementing v2 v2_r. The groupings for each of the operations are given Figure 18.

This first decomposition is independent of dependencies between operations. It is then possible sequencing and consolidate the divisions by operation in order to obtain the decomposition final. Such decomposition for the previous example is given Figure 19.

The decomposition described here is not unique. For example, a greater number of machines can be introduced. This decomposition can however be impossible in some cases. For example, if a variable must both be implemented in an operation, and non-implemented in another. In this case, BART must display an error message explaining the problem. According to the selected options, it must either leave either move to the next step in order to generate the whole of the machines valid.

Writing general components

The set of calculated machines are generated. For each written machine, the content is calculated appling the refinement rules associated to that machine.

Machine header

The header of each generated machine represents the same SEES clauses from the oginial one, L'entête de chaque machine générée reprend les mêmes clauses SEES que la machine d'origine, which may be added additional machines within the parameters passed to the tool.

Clause import

The clause IMPORT imports machines generated by the decomposition as well as the machines of iterators generated by the substitutions TYPE_ITERATION and INVARIANT_ITERATION for this step of refinement.

Operation Promotion

In the case where the generated component corresponds to an implementation or a refinement, and that no rule is applied to a transaction, this operation will not be written in the clause OPERATIONS of the machine but promoted. The clause PROMOTES therefore contains all the operations for which no rule of refinement is applied in the machine generated. Thus, in the example of decomposition Figure 19, the operation op1 not being amended, it will be promoted after to the machine M1.

Variables

The variables concrete and abstract to be present in the machine must be declared in the adequate clauses (CONCRETE_VARIABLES and ABSTRACT_VARIABLES).

Invariant

The invariant represent the type of the variables declared in the component generated, and the gluing invariant in the case where the component introduces a refinement of variable. More specifically:

• For non-implemented variables, the invariant reproduces the content of the clause IMPORT_TYPE of the rules of refinement of variables to refine these variables.
• For variables already implemented, the invariant resumed invariant of typing of the variable, without including the gluing invariant. In the case of a rule of refinement of variables containing refinement of variables, it is the clauses WITH_INV. In the case of a rule of implementation simple, it is the part of the clause INVARIANT not referring not the variable refined.
• For the variables for which the machine generated corresponds to the stage of implementation, the invariant corresponding to these variables is the invariant of typing of the variable plus the gluing invariant. For the rules of implementation simple, it is the full content of the clause INVARIANT. For the rules of refinement, it is the clauses WITH_INV and of the clause GLUING_INVARIANT.

Initialisation

The initialization of the variables is generated as the product of the rules of refinement corresponding to the current machine.

Operations

Only the operations not promoted are written in clause operation. The body of the latter is calculated as the result of the rules to be applied for the machine. In the case where the generated component is a machine, only the part of the pre-condition relating to the variables declared in the current machine is maintained.

Additional requirements

Adding comments to calling operations

Before each call of the operation generated, BART must add a comment incorporating the specification of the operation called. This comment must be in the following form, in order to be copied by the translator in the generated code:

/*? <specification (in B)  of the called operation> ?*/

Rules traceablility

BART must retain the information on what rules have been applied on what part of the input file at each stage. Thus, when no rule is applicable for a variable or a substitution, BART must be able indicate not only the substitution objected, but also the part of the machine B original which it.

Generalization with traceable rules

The software must propose an option to add a comment at the beginning of each line of code generated indicating the rule of the origin of the line.

Headers customization options

It is necessary to provide a way to specify preferences to modify the headers used for the generation of code.

Annotations (pragma)

The comments starting by /* pragma must be instructed by the tool even if they do not correspond to off listed in this specification. Indeed, they can be used by extensions of BART.

SEES addition

It must be possible to specify a list of machines that should automatically be added to the SEES clause, in the machines generated. This allows to write the rules referring these machines.

Extensibility

To enable manage new constraints, for example, related to language at the B0 targeted, it must be necessary to extend BART.

Library extension

BART must provide a library of extension allowing to extend the capabilities and the language of BART. The form of this library will depend on the language used for the development of BART.

New clases addition

The functionality of scalability must allow the addition of new clauses in the language of rules.

New agrds addition

The functionality of extension must allow the definition of new guards.

Syntatic tree modification

Before and after the different steps of browse generated code, it must be possible to insert steps of rewriting of the tree generated.

Decomposition algorithm replacement

It must be possible to replace the algorithm used to perform the decomposition in machine described in section 8.5. This possibility is for example necessary to allow compatibility with existing tools.

Chossing name algorithm replacement

It must be possible to replace the algorithms used for the choice of names of local variables and operations generated by BART. This replacement must also be possible for the machines of iterators. This possibility allows a share of adapting the code generated at different naming conventions, and on the other hand to translate the code for other language (by default, BART generates names in english).

Relative independence to BART

A plugin must be written, compiled and deployed without access to the source code of BART. Only the library of extension must be necessary to the development of a plugin.

Annex 1 : complete rule language grammar

This annex contains the ENBF grammer of the rule language accepted by NART.

Rule file

RuleFile = [ Theory { "&" Theory } ].
Theory
=
VariableTheory
| OperationTheory
| InitialisationTheory
| UserPassTheory
| TacticTheory
.

variable refinement rule

VariableTheory
=
"THEORY_VARIABLE" ident
"IS"
VariableRule { ";" VariableRule }
"END" ident
.

VariableRule
=
"RULE" ident
["(" JokerList ")" ]
"VARIABLE" JokerList
[ "TYPE" ident "(" JokerList ")" ]
"WHEN" Predicate
"IMPORT_TYPE" Predicate
(VariableImplementation | VariablesRefinement )
"END"
.

VariableImplementation =
"CONCRETE_VARIABLES" JokerList
[ "DECLARATION" Predicate ]
"INVARIANT" Predicate
.

VariablesRefinement =
"REFINEMENT_VARIABLES"
VariableRefinement { "," VariableRefinement }
"GLUING_INVARIANT" Predicate
.

VariableRefinement =
"CONCRETE_VARIABLE" joker
"WITH_INV" Predicate
"END"
| "ABSTRACT_VARIABLE" joker
"REFINED_BY" ident "(" Expression ")"
"WITH_INV" Predicate
"END"
.

initialization refinement rule

InitialisationTheory
=
"THEORY_INITIALISATION" ident
"IS"
InitialisationRule { ";" InitialisationRule }
"END" ident
.

InitialisationRule
=
"RULE" ident
"REFINES" Substitution
[ "WHEN" Predicate ]
"IMPLEMENTATION" Substitution
"END"
.

operation refinement rule

OperationTheory
=
"THEORY_OPERATION" ident
"IS"
OperationRule { ";" OperationRule }
"END" ident
.

OperationRule
=
"RULE" ident
"REFINES" Substitution
[ "WHEN" Predicate ]
[ "SUB_REFINEMENT" SubRefinementRule { "," SubRefinementRule } ]
( "REFINEMENT" { RefinementVarDecl } Substitution
| "IMPLEMENTATION" Substitution
)
[ "IMPLEMENT" IdentOrJokerList ]
"END"
.

RefinementVarDecl =
"VARIABLE" joker
[ "REFINED_BY" ident "(" Expression ")" ]
"WITH_INV" Predicate
"WITH_INIT" Substitution
"IN"
.

SubRefinementRule =
"(" Substitution ")" "->" "(" Substitution ")"
.

user pass theory

UserPassTheory
=
"USER_PASS" "IS"
[ ("VARIABLE"|"OPERATION"|"INITIALISATION") ":" "(" IdentList ")" ]
{ ";" ("VARIABLE"|"OPERATION"|"INITIALISATION") ":" "(" IdentList ")" }
"END"
.

tactic theory

TacticTheory
=
"THEORY" "TACTICS" "IS"
{ Tactic }
"END"
.

Tactic =
"VARIABLE" ":" VariableTactic { ";" VariableTactic }
| "INITIALISATION" ":" SubstitutionTactic { ";" SubstitutionTactic }
| "OPERATION" ":" SubstitutionTactic { ";" SubstitutionTactic }
.

SubstitutionTactic =
IdentList "=>" "(" Substitution ")"
.

VariableTactic =
IdentList "=>" "(" Predicate ")"
.

substitutions

Substitution = SimpleSubstitution { ("||"|";") SimpleSubstitution }.

SimpleSubstitution
=
"skip"
| "BEGIN" Substitution "END"
| "PRE" Predicate
"THEN" Substitution
"END"
| "ASSERT" Predicate
"THEN" Substitution
"END"
| "CHOICE" Substitution
{ "OR" Substitution }
"END"
| "IF" Predicate
"THEN" Substitution
{ "ELSIF" Predicate
"THEN" Substitution }
[ "ELSE" Substitution ]
"END"
| "SELECT" SelectContent [ "ELSE" Substitution ] "END"
| "CASE" Expression "OF"
"EITHER" PrimaryExpression
"THEN" Substitution
{ "OR" PrimaryExpression
"THEN" Substitution }
[ "ELSE" Substitution ]
"END"
| "ANY" IdentOrJokerList
"WHERE" Predicate
"THEN" Substitution
"END"
| "LET" IdentOrJokerList "BE"
Predicate
"IN" Substitution
"END"
| "VAR" IdentOrJokerList
"IN" Substitution
"END"
| "WHILE" Predicate
"DO" Substitution
"INVARIANT" Predicate
"VARIANT" Expression
"END"
| "LH" Predicate
"THEN" Substitution
"END"
| joker
| ident
| AffectSubstitution
| Iteration
| ImportedOperation
| ImplementSubstitution
.

SelectContent =
Predicate
"THEN" Substitution
{ "WHEN" Predicate
"THEN" Substitution }
.

ImplementSubstitution = "IMPLEMENT" "(" Substitution ")".

ImportedOperation
=
"IMPORTED_OPERATION" "("
[ "name" "=>" ident "," ]
"out" "=>" "(" [ IdentJokerVardeclList ] ")" ","
"in" "=>" "(" [ IdentJokerVardeclList ] ")" ","
"pre" "=>" "(" Predicate ")" ","
"body" "=>" "(" Substitution ")"
")"
| "SEEN_OPERATION" "("
"name" "=>" IdentOrJoker ","
"out" "=>" "(" [ IdentJokerVardeclList ] ")" ","
"in" "=>" "(" [ IdentJokerVardeclList ] ")" ","
"body" "=>" "(" Substitution ")"
")"
.

Iteration 
=
"INVARIANT_ITERATION" "("
[ ("tant_que"|"while") "=>" IdentOrJokerOrVarDecl "," ]
"1st" "index" "=>" BinaryExpression115 ","
"2nd" "index" "=>" BinaryExpression115 ","
"constant" "=>" BinaryExpression115 ","
"1st" "type" "=>" BinaryExpression115 ","
"2nd" "type" "=>" BinaryExpression115 ","
"body" "=>" "(" Substitution ")" ","
"invariant" "=>" "(" Predicate ")"
")"
| "TYPE_ITERATION" "("
[ ("tant_que"|"while") "=>" IdentOrJokerOrVarDecl "," ]
"index" "=>" BinaryExpression115 ","
"type" "=>" BinaryExpression115 ","
"body" "=>" "(" Substitution ")" ","
"invariant" "=>" Predicate
")"
| "CONCRETE_ITERATION" "("
"init_while" "=>" "(" Substitution<out Substitution init> ")" ","
("tant_que"|"while") "=>" BinaryExpression115<out Expression e> ","
"body" "=>" "(" Substitution<out Substitution body> ")" ","
"invariant" "=>" "(" Predicate<out Predicate invariant> ")" ","
"variant" "=>" BinaryExpression115<out Expression variant> ","
"flag" "=>" IdentOrJoker<out Expression flag>
")"
.

AffectSubstitution 
=
IdentJokerVardeclList
( ":" "(" Predicate ")"
| "::" Expression
| [ "(" Expression ")" ]
":=" Expression
| "<--" IdentOrJoker [ "(" Expression ")" ]
)
.

predicates

Predicate = ConjunctionPredicates { "=>" ConjunctionPredicates }.
ConjunctionPredicates
=
EquivalencePredicate { ("&"|"or"|"cand") EquivalencePredicate }
.

EquivalencePredicate = SimplePredicate { "<=>" SimplePredicate }.
SimplePredicate
=
"(" Predicate ")"
| "bnot" "(" Predicate ")"
| joker
| ident "(" Expression ")"
| Expression ComparisonOperator Expression
| "not" "(" Predicate ")"
| ("!"|"#") QuantifiedList "." "(" Predicate ")"
.

ComparisonOperator =
"="|"/="|":"|"/:"|"<:"|"<<:"|"/<:"|"/<<:"|"<="|">="|">"|"<"
.

expressions

Expression = BinaryExpression20.
// Expression that can occur between operators of priority 20
BinaryExpression20 = BinaryExpression115 { "," BinaryExpression115 }.
// Expression that can occur between operators of priority 115
BinaryExpression115 =
BinaryExpression125 { Operator115 BinaryExpression125 }
.

Operator115 = "<->"|"+->"|"+->>"|">->"|"-->"|">+>>"|">+>"|"-->>"|">->>".
// Expression that can be located between operators of priority 125
BinaryExpression125 =
BinaryExpression160 { Operator125 BinaryExpression160 }
.

Operator125 =
"<-"|"><"|"<<|"|"|>>"|"<|"|"\/"|"/\"|"^"|"->"|"\|/"|"<+"|"/|\"|"|>"|"|->"
.

// Expression that can occur between operators of priorty 160
BinaryExpression160
=
BinaryExpression170 { ".." BinaryExpression170 }
.

BinaryExpression170
=
BinaryExpression180 { ("+"|"-") BinaryExpression180 }
.

BinaryExpression180
=
BinaryExpression190 { ("*"|"/"|"mod") BinaryExpression190 }
.

BinaryExpression190
=
Expression200 { "**" Expression200 }
.

Expression200
=
Expression210
| "-" Expression210
.

Expression210
=
PrimaryExpression
{
"~"
| ("[" Expression "]")
| ("(" Expression ")")
}
.

PrimaryExpression
=
ident
| number
| joker
| vardecl
| "(" Expression { (";"|"||") Expression } ")"
| "MAXINT"
| "MININT"
| "{}"
| "[]"
| FuncOperator "(" Expression ")"
| "{" Expression [ "|" Predicate ] "}"
| "[" Expression "]"
| "TRUE"
| "FALSE"
| "bool" "(" Predicate ")"
| "%" QuantifiedList "." "(" Predicate "|" Expression ")"
.

QuantifiedList
=
IdentOrJokerList
| "(" IdentOrJokerList ")"
.

FuncOperator =
"max"|"min"|"card"|"dom"|"ran"|"POW"|"POW1"|"FIN"|"FIN1"|"union"|"inter"
.

== others ==

JokerList = joker { "," joker }.
IdentOrJokerList = IdentOrJoker { "," IdentOrJoker }.
IdentOrJoker = ident | joker.
IdentJokerVardeclList =
IdentOrJokerOrVardecl { "," IdentOrJokerOrVardecl }
.

IdentOrJokerOrVardecl = ident | joker | vardecl.
IdentList = ident { "," ident }.

---