Rules-DSL: Difference between revisions

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 looks like this:

RULES_MACHINE machine name
REFERENCES list of rules machines

Below, you can use SETS, DEFINITIONS, PROPERTIES or CONSTANTS as in a normal B machine. Note that VARIABLES are not supported as they are set by rule based computations.

Use Rules for Data Validation

Rules can be defined 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 can look like this:

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
    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;
    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
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

Functions

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