Region Decomposition

Region decomposition takes a function and returns every distinct behaviour it has, as a finite list. Each entry describes a set of inputs and the exact output for all of them. It is the analysis most of CodeLogician is built around: test generation reads its results, and "have I covered the edge cases?" becomes a question with a number for an answer.

This guide covers running one, reading the output, and cutting it down to size when it comes back too large.

Step 1: Attach a decomposition request

Add a [@@decomp top ()] attribute to the function you want decomposed. Add ~prune:true as well if you want concrete sample inputs, which you almost always do:

type payment_method =
  | Card
  | BankTransfer
 
let calculate_fee m amount =
  match m with
  | Card -> if amount >. 10000.0 then 0.019 *. amount else 0.029 *. amount +. 0.30
  | BankTransfer -> 0.008 *. amount +. 1.50
[@@decomp top ~prune:true ()]
codelogician eval check-decomp fee-regions.iml
$ codelogician eval check-decomp fee-regions.iml
eval_res: Success
decomp_res_list:
- decomp_req_index: 0
  function_name: calculate_fee
  decomp_res:
    description: Decomp succeeded with 3 regions
    regions:
    - label_path: '1.1'
      weight: 1
      constraints:
      - m <> BankTransfer
      - amount <=. 10000.0
      invariant: 3.0 /. 10.0 +. 29.0 /. 1000.0 *. amount
      model:
        amount: '10000.0'
        m: Card
      model_eval: (2903.0 /. 10.0)
    - label_path: '1.2'
      weight: 1
      constraints:
      - m <> BankTransfer
      - amount >. 10000.0
      invariant: 19.0 /. 1000.0 *. amount
      model:
        amount: '10001.0'
        m: Card
      model_eval: (190019.0 /. 1000.0)
    - label_path: '2'
      weight: 1
      constraints:
      - m = BankTransfer
      invariant: 3.0 /. 2.0 +. 1.0 /. 125.0 *. amount
      model:
        amount: '0.0'
        m: BankTransfer
      model_eval: (3.0 /. 2.0)

Three regions. The amount parameter is a real, so the function has infinitely many possible inputs. It has only three behaviours, and every one of those inputs falls into one of them.

Step 2: Read the regions

Each region has two parts:

  • constraints: conditions on the inputs, conjoined (all must hold). Together they describe a set of inputs, usually an infinite one.
  • invariant: a symbolic expression for the output, valid for every input satisfying those constraints.

So region 1.1 reads: for any card payment of at most 10,000, the fee is 0.3 + 0.029 × amount. That is a statement about infinitely many transactions, and it is proved rather than sampled.

With ~prune:true you also get:

  • model: a concrete input inside the region.
  • model_eval: the function's output at that input.

What the region list guarantees

Two properties are what make the output trustworthy rather than merely suggestive:

Coverage. Every input in the domain satisfies the constraints of at least one region. Nothing falls through.

Disjointness. For a decomposition from a plain top (), an input satisfies the constraints of at most one region. Regions do not overlap.

Together these mean the region list is the function, re-expressed: the body is equivalent to if cs_0 then inv_0 else if cs_1 then inv_1 … else inv_n over the whole domain, and ImandraX proves that equivalence rather than asserting it. The technique descends from Cylindrical Algebraic Decomposition, lifted from polynomial constraints to programs at large.

Both properties can be given up on purpose. ~assuming weakens coverage, as described below, and composition operators applied to a finished decomposition can produce overlapping regions.

What to look for

The region count. If you expected five behaviours and got eight, the disagreement is the most valuable thing on the screen, and it is worth resolving before you write a test.

Where the boundaries sit. Not "the function returns Review for 10,001" but "the function returns 0.019 × amount for every amount strictly above 10,000". The constraint tells you where the cliff is, so you can ask whether it is where you meant to put it.

Sample points against the boundaries. 10000.0 and 10001.0 above are not arbitrary. The solver picks points satisfying the constraints, and constraints derived from branch conditions have their solutions up against the boundary. This is why the derived tests come out boundary-hugging.

Step 3: Cut it down to size

Region counts grow quickly when independent decisions interact. A function that branches three ways on one input, four on another and four on a third has forty-eight distinct behaviours, in thirty lines:

type customer = Standard | Premium | Partner
 
let volume_tier (units : int) : int =
  if units < 10 then 1
  else if units < 100 then 2
  else if units < 1000 then 3
  else 4
 
let loyalty_bonus (years : int) : real =
  if years < 1 then 0.0
  else if years < 3 then 0.02
  else if years < 10 then 0.05
  else 0.08
 
let discount (c : customer) (units : int) (years : int) : real =
  let base =
    match c with
    | Standard -> 0.0
    | Premium -> 0.05
    | Partner -> 0.10
  in
  let tier = volume_tier units in
  let tier_bonus =
    if tier = 1 then 0.0
    else if tier = 2 then 0.01
    else if tier = 3 then 0.03
    else 0.06
  in
  base +. tier_bonus +. loyalty_bonus years
[@@decomp top ()]
$ codelogician eval check-decomp tiers.iml | grep description
description: Decomp succeeded with 48 regions

Three customer types, four volume tiers and four loyalty bands, and every combination behaves differently. Real code reaches four figures. Such a decomposition is a faithful account of the function, and if you want a test per behaviour that is exactly what you need. Often, though, you are after one part of the picture, and a smaller decomposition that focuses on it is more useful.

Three ways to shape it.

~basis: hold a function symbolic

If a helper's internal branching is not what you are investigating, put it in the ~basis list. It is left unexpanded and appears symbolically in the invariants:

[@@decomp top ~basis:[ [%id loyalty_bonus] ] ()]
$ codelogician eval check-decomp tiers-basis.iml | grep description
description: Decomp succeeded with 12 regions

Forty-eight to twelve. The loyalty logic has not been ignored. It is carried through the regions unevaluated, appearing in the invariants as a call:

$ codelogician eval check-decomp tiers-basis.iml | grep invariant
invariant: loyalty_bonus years
invariant: 1.0 /. 100.0 +. loyalty_bonus years
invariant: 3.0 /. 100.0 +. loyalty_bonus years
invariant: 3.0 /. 50.0 +. loyalty_bonus years
invariant: 1.0 /. 20.0 +. loyalty_bonus years
invariant: 3.0 /. 50.0 +. loyalty_bonus years
invariant: 2.0 /. 25.0 +. loyalty_bonus years
invariant: 11.0 /. 100.0 +. loyalty_bonus years
invariant: 1.0 /. 10.0 +. loyalty_bonus years
invariant: 11.0 /. 100.0 +. loyalty_bonus years
invariant: 13.0 /. 100.0 +. loyalty_bonus years
invariant: 4.0 /. 25.0 +. loyalty_bonus years

Each invariant is now an expression in loyalty_bonus years rather than four separate numeric cases. The twelve regions still cover the whole input domain and are still exact; they are simply stated in terms of a function you have chosen not to unfold here.

Use this when a helper is already tested, is a leaf utility, or is genuinely someone else's problem.

~assuming: decompose under a precondition

If you only care about part of the input domain, say so. ~assuming takes a boolean function and restricts the analysis to inputs satisfying it:

let is_premium (c : customer) (_units : int) (_years : int) : bool = c = Premium
 
let discount c units years = ...
[@@decomp top ~assuming:[%id is_premium] ()]
$ codelogician eval check-decomp tiers-assuming.iml | grep description
description: Decomp succeeded with 16 regions

Sixteen regions: four volume tiers × four loyalty bands, for premium customers only.

Use this when parts of the input space are unreachable in production, or you are investigating one code path. Note that coverage is now conditional: the regions cover only where the assumption holds, so a suite derived from them says nothing about non-premium customers. Restricting the domain and forgetting you did is a real way to be misled.

Tighten the types

A decomposition covers every value a parameter's type allows, not just the values the code means. So a parameter typed int or string that really takes a fixed handful of values brings extra regions with it. A status encoded as 0, 1, 2 or 3 carries a catch-all region for every other integer, and each such parameter adds its own. Replace the encoding with a variant type, Pending | Active | Suspended | Closed, and those regions disappear.

The regions that remain are also better regions:

  • Constraints read status = Pending rather than status = 0, so the region list is legible without a decoder.
  • No region asserts behaviour for values that cannot occur, so no test is generated for them.
  • The match over the variant is exhaustive, so a missing case is a compile error rather than a silent fall-through.

Next

Previous← How-to Guides
NextGenerate Test Cases →