← Policy gallery

decomposition_drives_tests

formal-reasoning reasoning pure_temporal decompositiontestingcoverageformal-verification

A region decomposition should be followed by generated tests, so the behavioral breakdown actually yields high-coverage checks rather than being left unused.

Formula

G(Decompose → F(GenerateTests))

Hover any operator or symbol for what it means.

Requires a reasoner

This policy is satisfied by verification from codelogician — an automated-reasoning tool in the reasoner registry.

Why it matters

Region decomposition maps a function's disjoint behavioral cases; its payoff is a high-coverage test per region. A decomposition with no tests generated from it leaves that value on the table.

Examples

passes Decompose(price) → GenerateTests(price)

fails Decompose(price) with no subsequent test generation

Use it

ponens policies add decomposition_drives_tests --into ./trace.json
ponens trace check ./trace.json