Jan Gruteser (talk | contribs) m (→Rules) |
Jan Gruteser (talk | contribs) |
||
Line 6: | Line 6: | ||
Rules machines are stored in <code>.rmch</code>-files. The general setup for the machine header is: | Rules machines are stored in <code>.rmch</code>-files. The general setup for the machine header is: | ||
<pre> | <pre> | ||
RULES_MACHINE | RULES_MACHINE machine_name | ||
REFERENCES list of rules machines | REFERENCES list of rules machines | ||
</pre> | </pre> | ||
Below, you can use <code>SETS</code>, <code>DEFINITIONS</code>, <code>PROPERTIES</code> or <code>CONSTANTS</code> as in a normal B machine. Note that <code>VARIABLES</code> are not | The latter allows inclusion of other rules machines. Below, you can use <code>SETS</code>, <code>DEFINITIONS</code>, <code>PROPERTIES</code> or <code>CONSTANTS</code> as in a normal B machine. Note that <code>VARIABLES</code> are not allowed as they are set by rule based computations. | ||
====Rules==== | ====Rules==== | ||
Line 15: | Line 15: | ||
In the B Rules-DSL a rule has the following structure: | In the B Rules-DSL a rule has the following structure: | ||
<pre> | <pre> | ||
RULE | RULE rule_name // will be the name of the operation and variable storing the result | ||
RULE_ID id | RULE_ID id | ||
DEPENDS_ON_RULE list of rules | DEPENDS_ON_RULE list of rules | ||
Line 56: | Line 56: | ||
====Computations==== | ====Computations==== | ||
<pre> | <pre> | ||
COMPUTATION | COMPUTATION computation_name | ||
DEPENDS_ON_RULE list of rules | DEPENDS_ON_RULE list of rules | ||
DEPENDS_ON_COMPUTATION list of computations | DEPENDS_ON_COMPUTATION list of computations | ||
Line 68: | Line 68: | ||
END | END | ||
</pre> | </pre> | ||
After the execution of a computation, the value of the corresponding variable <code>computation_name</code> is changed from <code>NOT_EXECUTED</code> to <code>EXECUTED</code>. | |||
====Functions==== | ====Functions==== |
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
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
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
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