The B Rules domain-specific language mainly provides operations for data validation. Rules allow checking for expected properties, while computations can be used to define and compute variables based on the successful execution of certain rules. Furthermore you can use functions to compute values multiple times depending on different inputs.
Rules machines are stored in .rmch
-files. The general setup for the machine header is:
RULES_MACHINE machine_name REFERENCES list of rules machines
The latter allows inclusion of other rules machines. Below, you can use SETS
, DEFINITIONS
, PROPERTIES
or CONSTANTS
as in a normal B machine. Note that VARIABLES
are not allowed as they are set by rule based computations.
Rules can be defined in the OPERATIONS
-section of a rules machine. Depending on whether the expectations are met, a rule returns SUCCESS
or FAIL
. If a rule fails, additionally provided string messages are returned as counterexamples.
In the B Rules-DSL a rule has the following structure:
RULE rule_name // will be the name of the operation and variable storing the result RULE_ID id DEPENDS_ON_RULE list of rules DEPENDS_ON_COMPUTATION list of computations ACTIVATION predicate ERROR_TYPES positive number of error types BODY arbitrarily many rule bodys (see below) END
If a rule depends on other rules, it can only be executed if the specified rules have been successfully checked, i.e. their corresponding variables rule_name
have the value SUCCESS
. In addition, rules can depend on computations. In this case, a rule is enabled when the specified calculation has been executed. You can also specify an individual ACTIVATION
predicate. You can omit all activation predicates and dependencies if they are not needed.
If you want to use different error types, e.g. if you use multiple bodys in one rule and want to distinguish between them, you must declare the number of error types in the rule header. Error types are also optional.
Within the body you can use as many conditions for the outer rule as you like. There are two constructs for specifiying the expectation of the rule.
The following is formulated in a positive way, i.e. the execution of the rule leads to SUCCESS
if the conditions in the EXPECT
-part are fulfilled.
RULE_FORALL list of identifiers WHERE conditions on identifiers EXPECT conditions that must be fulfilled for this rule ERROR_TYPE number encoding error type, must be in range of error types COUNTEREXAMPLE STRING_FORMAT("errorMessage ~w", identifier from list) END
Alternatively, you can also formulate the rule negatively, i.e. the execution of the rule leads to FAIL
if the conditions in the WHEN
-part are fulfilled.
RULE_FAIL list of identifiers WHEN conditions on identifiers for a failing rule ERROR_TYPE number encoding error type, must be in range of error types COUNTEREXAMPLE STRING_FORMAT("errorMessage ~w", identifier from list) END
Counterexamples are of the type INTEGER <-> STRING
. The integer contains the error type, while the string contains the message of the counterexample.
Computations can be used to create variables. As for rules, their activation can depend on further rules, computations or any other predicate specified as an activation condition. Note that any variable used in ACTIVATION
must have an initial value. For this purpose, use the DUMMY_VALUE
(in the corresponding computation of that variable), which initializes the variable with the specified value instead of the empty set. The general syntax for computations:
COMPUTATION computation_name DEPENDS_ON_RULE list of rules DEPENDS_ON_COMPUTATION list of computations ACTIVATION predicate BODY DEFINE variable_name TYPE type of variable DUMMY_VALUE value of variable before execution (initialisation) VALUE value of variable after execution END END
You can omit all activation predicates and dependencies and also the dummy value if they are not needed. After the execution of a computation, the value of the corresponding variable computation_name
is changed from NOT_EXECUTED
to EXECUTED
.
FUNCTION output <-- function_name(list of input parameters) PRECONDITION predicate POSTCONDITION predicate BODY some B statements output := ... END
If you want to validate data, for example from a CSV or XML file, you can use the rule language. Set up a rules machine as described above and add your data using the appropriate definition. For an XML file, this could look as follows:
RULES_MACHINE XML_import DEFINITIONS "LibraryXML.def" CONSTANTS xml_data PROPERTIES xml_data = READ_XML("xml_file.xml", "auto") END
Currently, it is not possible to include rules machines directly into any other machines. Instead, use the rules machine at the top of the hierarchy (of the rules project) and save the internal generated machine as .mch
. After changing the machine name accordingly, the rules can be included and used via this machine.