Rules-DSL: Difference between revisions

B-Rules DSL

The B-Rules domain-specific language (B-Rules DSL) 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 the inclusion of other rules machines and ordinary B machines that contain only constants, but not yet any other B machines. Below, SETS, DEFINITIONS, PROPERTIES or CONSTANTS can be used 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
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

The specified rule_name will be the name of the operation and variable storing the result. 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 bodies 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 specifying 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.

Also valid for the rules header, but not currently used, are:

RULE_ID id
CLASSIFICATION identifier
TAGS identifier

Computations

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. Furthermore, a DUMMY_VALUE can be set, which initialises the variable with the specified value instead of the empty set before execution of the computation. A computation can be replaced by a previously defined computation if it sets the same variable (of the same type). The general syntax for computations:

COMPUTATION computation_name
DEPENDS_ON_RULE list of rules
DEPENDS_ON_COMPUTATION list of computations
ACTIVATION predicate
REPLACES identifier of exactly one computation
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.

Since the result of each computation is written into a variable, it is also possible to formulate invariants for these variables.

Functions

Functions can be called from any rules machine that references the machine containing the function. Depending on input parameters that must fulfil specified preconditions, the functions returns output value(s) that must fulfil optional postconditions. In the body you can use any B statements to calculate the output value.

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

Additional Syntax

There are some useful predicates available in rules machines that can be used to check the success or failure of rules. It is also possible to check whether a certain error type was returned by a rule. They are listed below:

• SUCCEEDED_RULE(rule1): TRUE, if the check of rule1 succeeded
• SUCCEEDED_RULE_ERROR_TYPE(rule1,1): TRUE, if the check of rule1 did not fail with error type 1
• GET_RULE_COUNTEREXAMPLES(rule1): set of counterexamples of rule1
• FAILED_RULE(rule1): TRUE, if the check of rule1 failed
• FAILED_RULE_ERROR_TYPE(rule1,2): TRUE, if the check of rule1 failed with error type 2
• FAILED_RULE_ALL_ERROR_TYPES(rule1): TRUE, if the check of rule1 failed with all possible error types for rule1
• NOT_CHECKED_RULE(rule1): TRUE, if rule1 has not yet been checked
• DISABLED_RULE(rule1): TRUE, if rule1 is disabled (i.e., the preconditions are not fulfilled)

Another functionality of rules machines are FOR-loops. Their syntax is:

FOR variable(s) IN set
DO
    operation(s)
END

An example:

RULE example_rule
BODY
    FOR x,y IN {1 |-> TRUE, 2 |-> FALSE, 3 |-> FALSE} DO 
        RULE_FAIL 
        WHEN y = FALSE
        COUNTEREXAMPLE STRING_FORMAT("example_rule_fail: ~w", x)
    END
END

This rule always fails and returns {1 |-> "example_rule_fail: 2", 1 |-> "example_rule_fail: 3"}.

Use Rules for Data Validation

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

Now some properties can be validated. For example:

RULE is_supported_version_of_type_xyz
ERROR_TYPES 2
BODY
    RULE_FAIL e
    WHEN
        1 : dom(xml_data) & e = data(1)'element & e /= "xyz"
    ERROR_TYPE 1 // optional: 1 is standard type
    COUNTEREXAMPLE
        STRING_FORMAT("Error: could not find element 'xyz', was '"^e^"'")
    END;
    RULE_FAIL v
    WHEN
        v = xml_data(1)'attributes("version") & v /: supported_versions
    ERROR_TYPE 2
    COUNTEREXAMPLE
        "xyz of version "^v^" is currently not supported"
    END
END;

Include Rules Machines into other Projects

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.