Applications

Region decomposition has been used extensively in production for financial systems, regulatory compliance, and safety-critical applications. Here are some key application patterns.

Automated test generation

The most immediate application: generate one test case per region for complete behavioral coverage.

let d = my_function
[@@decomp top () |>> prune |>> enumerate]

Each enumerated instance is a concrete test case. Since the regions are exhaustive and disjoint, this set of tests covers every distinct behavior of the function.

Compare this with traditional testing approaches:

  • Random testing may miss rare code paths
  • Manual test suites depend on the developer's intuition
  • Region-based testing is mathematically guaranteed to cover every behavioral region

Coverage analysis

Region decomposition reveals the exact number of distinct behaviors a function has. This is a much more meaningful metric than code-line or branch coverage:

  • A function with 100 lines might have only 3 behavioral regions
  • A 10-line function might have 20 regions due to complex interactions between conditions

By comparing the number of regions against your specification, you can identify:

  • Missing cases — Regions your specification doesn't account for
  • Redundant cases — Multiple specification cases that map to the same behavior
  • Dead code — Regions with infeasible constraints (code that can never be reached)

Regulatory compliance

In financial services, regulators often require evidence that systems handle all possible scenarios. Region decomposition provides this evidence rigorously:

  • MiFID II transaction reporting — Decompose the reporting logic to show every possible classification is handled
  • Exchange pricing — Show that fee calculations cover every possible order type and venue combination
  • Risk calculations — Prove exhaustive coverage of margin and collateral scenarios

Several of the case studies demonstrate this application.

Specification discovery

When working with unfamiliar or complex code, region decomposition serves as a specification extraction tool:

  1. Decompose the function
  2. Read the regions and invariants
  3. The decomposition is the specification — it tells you exactly what the function does for every possible input

This is particularly valuable for:

  • Legacy systems where documentation is outdated or missing
  • Complex business rules where the code is the only source of truth
  • Auditing where you need to understand system behavior without trusting documentation

Model comparison

Decompose two implementations of the same specification and compare their regions. If the regions and invariants match, the implementations are equivalent. If they differ, the differing regions pinpoint exactly where behavior diverges.

Integration with AI agents

Region decompositions can be serialized and provided to AI agents as structured descriptions of function behavior. An agent can use this to:

  • Understand what a function does without reading the source code
  • Generate test cases systematically
  • Reason about edge cases and boundary conditions
  • Verify that changes preserve existing behavior