BART is a tool that can be used to automatically refine B components. This process is rule based so that the user can drive refinement. Its own rule language has been defined in this purpose. It has been designed to be a stand-alone tool, but it may be launched from Atelier B user interface. As an input, BART must be given at least the machine or refinement to refine. There must be exactly one component to refine. Automatic refinement is a rule based refinement process for B components (abstractions or refinements). The tool is given a component, and it searches, for each element to refine, some rules that specify how it must be treated. These rules allow to implement design patterns for B models. BART is specialized for B software models but is likely to be extended to support event B models.
BART produces a set of B components corresponding to the implementation of this input machine or refinement, by using 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. Two different situations may arise:
- no rule is applicable: the tool stops silently. The user is expected to add/modify existing rules in order to complete the refinement process.
- a variable needs to be implemented in several components: constraints due to decomposition and implentation may leads to have conflicts (both the model and the refinement rules need to be modified). In this case, a xml file is generated (see figure 2.2).
The automatic refinement proces requires some specific conditions to be efficient, as demonstrated in figure 2.3:
- SETS and CONSTANTS have to be sperate from the model to be refined (configuration machine)
- similarly, setters and getters have to be separate (inputs machine)
First elements processed by the BART tool are the abstract variables of the component to refine (content of the ABSTRACT VARIABLES clause). The tool must produce, for each one of them, one or more abstract or concrete variables that implement it. BART processes operations of given component in order to refine them. It must produce, for each operation, a substitution body concrete enough to be put in the component implementation. Refined operations are considered for the whole component abstraction. It means that BART refines the most concrete version of each operation. BART also refines content of initialisation clause of given component. Typically, it produces a concrete result by specifying initialisation substitutions for concrete variables refining content of ABSTRACT VARIABLES clause. Abstract variables are refined first, as other parts of the process need its output to find suitable rules for operations and initialisation. It is necessary at these steps to know how variables have been refined. This variable information is stored as predicates in BART hypothesis stack. As it will be described later, refinement process uses rules to determine how each element is refined. A same rule can apply for several elements, so it must be general. In this purpose, the rule language uses jokers, so that rules can contain variable parts.
BART uses rules for refining variables, operations and substitutions. These rules belong to different types: variables rules, or substitution rules, which can be used for both operations and initialisation. Rules of same type are gathered in theories (ako packages). Theories are associated to predicates/expressions families, as referred in the tactics theory. Rules usually contain a pattern, and may contain a constraint. These two elements are used to know if a rule can be applied to refine a certain element. Rules also contain clauses that express the refinement result. Rules may have constraints, expressed in their WHEN clause. A constraint is a predicate, which may contain jokers. It may be a complex predicate, built with & and OR operators. BART contains a stack of hypothesis , which is built from the machine to refine and its environment. A constraint is successfully checked if its elementary elements (element not containing & or OR) can be pattern-matched with a predicate of the stack so that the complex constraint is true. According to operators, BART uses backtracking to try every combination of instantiation that should be a success. If several instantiations can make the constraint be successfully checked, BART uses one of them. In this case, it is better to write a more detailed constraint to have only one result. If there are several results, BART could choose one which is not the one the user had planned. Usually, when checking a constraint, some jokers have already been instantiated. Guards are special predicates which may be present in rule constraint clauses. They allow checking some properties on elements to re?ne and their environment. There are two kinds of guards:
- some are simply present in the predicate stack. They are added at the environment loading. For instance ABCON (abstract constant) and ABVAR (abstract variable) belong to this kind of guards.
- the other kind is calculated guards. For these ones, during constraint checking, BART doesn’t try to match them) with the stack, but directly calculates if the guard is true or false. These kinds of guards may also have side effects. For example bnum (numeric test) or bident (identifier test) are calculating guards. Guards are simply put in the constraint as regular predicates.
This process is used for variables, operations and initialisation refinement, although it is simpler for variables. Every rule contains a pattern. First BART tries to match it with the element to refine. If it succeeds, it tries, if a rule has a constraint clause, to match the predicate against hypothesis. When checking the constraint, some jokers have already been instantiated by pattern matching. If the constraint checking is a success or the rule had no constraint, then it will be used to re?ne current element. Variable process is simpler as variable rules have simple pattern, which is a single joker. Variable rule patterns are only matched in order to instantiate the joker representing currently re?ned abstract variable. This joker is reused in WHEN or result clauses.
Refinement Rules Database
Rule files are files containing theories, each theory containing one or several rules used to refine given component. Rule file extension is usually .rmf. A rule file can contain variable, operation, structure and initialisation theories. It can also contain utility theories such as tactic, user pass, or definition of predicates synonyms. The rule file syntax must also respect certain constraints:
- User pass can be present at most once
- Tactic can be present at most once
- Predicate theory can be present at most once
Order between theories has no syntactical impact, expect for predicates theory: it must be defined before its elements are used in the rule. Order between theories has an impact on the rule research, as the standard process (no user pass or tactic) reads theories from bottom to top. User pass and tactic can be defined anywhere in the file, even before theories they refer to have been defined.
The BART tool comes with a set of predefined rule base, contained in the file PatchRaffiner.rmf present in BART distribution. It provides rules that permit to refine most of the classical B substitutions. The classical automatic refinement scheme is the following: most elements of given component can be refined using the rule base. If an element can not be refined with it, or needs a more specific treatment, user should write suitable rules in rmf files that will be provided after the rule base on command line, or in the component associated rule file.