orchestrata_ultimate.verification.constraints

Reference › orchestrata_ultimate › verification › constraints

Constraint definitions and evaluation.

The constraints package holds the two pieces that work directly on Constraint objects in the verification subsystem. evaluator contains ConstraintEvaluator, which decides whether a constraint holds by querying the Prolog rulebase and returns VerificationResult objects, singly, in bulk or in dependency order. definitions holds pure helpers for grouping, filtering, sorting and classifying constraints as blocking.

Data flows from a list of constraints plus a context of actual values into the evaluator, which returns results; the checkpoint verifier, the verification agent and the verification engine call it. Start with the evaluator. The package has no entry point of its own.

3 modules, 274 lines of code.

Modules

Dependency diagram