Rules-DSL

Rules DSL

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.

Setting up a Rules Machine

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

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

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

After the execution of a computation, the value of the corresponding variable computation_name is changed from NOT_EXECUTED to EXECUTED.

Functions

FUNCTION output <-- function_name(list of input parameters)
PRECONDITION
    predicate
POSTCONDITION
    predicate
BODY
   some B statements
   output := ...
END