Tutorial

In this tutorial, you will build a domain model for a business trip expense application using Souther. You begin by modeling record fields and the core operations: submission, approval, and settlement. By the end, your types and behaviors will express which operations are valid in each state, why approval is required, what is reimbursed, and how invalid domain requests are rejected.

You do not build the entire model at once. First, you represent the current fields and operations as data and behavior. Next, you write scenarios that reflect real business situations and expected outcomes as test examples. Whenever you encounter missing test cases or gaps identified in the souther examples report, you refine your types, states, and behaviors. Through this iterative process, business rules evolve into a structured model.

In this tutorial, we call this approach Example-Driven Domain Modeling. Like BDD, it validates business logic through concrete scenarios, but its goal extends beyond agreeing on UI behavior. Through test cases, you discover and verify the types, states, and operations of the domain model itself.

This tutorial covers the happy path from submission to final approval. Rejections and send-backs are omitted here. Once you complete the tutorial, you can compare your model with the full version in businesstrip/src/main/souther/businesstrip.sou.

Before You Begin

This document does not provide a complete file for each section. Code blocks show only the code to add or replace in the businesstrip.sou file you built through the previous section. Unless noted otherwise, keep existing definitions, let bindings, and example blocks intact. Use the Update summary at the start of each section to confirm what to add, replace, or remove.

As a result, copying and pasting a single isolated code block will not work. Follow these steps for each section:

Read the “What You Will Learn” and “Update” sections, then edit your current businesstrip.sou.
Run souther examples businesstrip.sou while keeping the test cases added in that section.
Compare the generated report with the report shown in the text. Line and column numbers may vary based on file length.

The goal of this tutorial is the happy path from submission to final approval. Even if the report shows adequacy: satisfied along the way, it only means the model rules and test cases written up to that point are consistent. It does not mean the entire business domain is fully implemented.

Souther Basics

Souther is a language for defining data structures and functions that implement decision logic in the same file. In this tutorial, you define the structure of a business trip application and operations such as submission and approval in businesstrip.sou.

Here are the first six language constructs:

Syntax	Meaning in This Tutorial
`data`	Declares a type. For example, `data Amount = Int` names `Int` as an `Amount`. `A \| B` represents the type of A or B.
`Option<Type>`	Represents an optional value. In the initial model, it represents fields that have not yet been recorded. In later sections, you split types by state to reduce `Option`.
`behavior`	Declares input and output contracts for domain operations. For example, `(app: Draft) -> Submitted` represents an operation that takes a draft application and returns a submitted application.
`constructs`	Declares the `data` types that a behavior implementation is permitted to instantiate. If a behavior calls another `let`, include values instantiated within that nested call as well.
`let`	Binds a name to a value or provides a behavior implementation. `let submitTrip (...) = ...` provides decision logic for the matching behavior.
`example`	Defines a test scenario executing a behavior and its expected output. A single `input -> output` pair serves as both specification and automated test.

For example, the following example asserts that submitting a Fukuoka trip application at a specific timestamp results in the Submitted state. This is a preview to explain the syntax. The fixture and state types are defined in Section 2.

example submitTrip
    | "Submit a small trip to Fukuoka" :
        (fukuokaTripDraft, DateTime("2026-07-27T09:00:00"))
            -> Submitted

The name submitTrip at the start of example is the target behavior. The input follows : and is enclosed in ( ... ); the expected output follows ->. Adding lines that start with | adds test cases for different inputs and expectations. In this tutorial, each |-to--> entry is called a test case.

invariant and guard appear in later sections. invariant defines valid value boundaries for a data type. guard condition else Failure branches to a failure output when a condition is not met. Both inform souther examples about which test cases to generate.

Prerequisites

Souther requires JDK 25 or later. The compiler and the code it generates are pinned to the Java 25 class-file version, so an earlier JDK cannot run them. Check what you have:

java -version

On WSL2, install the JDK inside WSL and confirm that java -version answers there, not only in Windows.

The only other tool this tutorial needs is the souther command. You do not need to create a Maven module.

On macOS, install using the Souther Homebrew tap:

brew install souther-lang/souther/souther

Verify the installation:

souther

If you do not use Homebrew, download the souther executable from GitHub Releases. It is self-contained and needs nothing but the JDK on your PATH. Take the newest release listed there; the commands below use v0.3.0:

mkdir -p ~/.local/bin
curl -L -o ~/.local/bin/souther \
  https://github.com/souther-lang/souther/releases/download/v0.3.0/souther
chmod +x ~/.local/bin/souther
export PATH="$HOME/.local/bin:$PATH"

Each release also publishes SHA256SUMS, so you can check the download before running it. Add the export line to ~/.zshrc or ~/.bashrc. Open a new shell and verify:

souther

For VS Code, install the Souther extension from the Visual Studio Marketplace, or run ext install souther.souther from the command palette. It gives syntax highlighting, diagnostics, completion, go-to-definition, rename, and formatting. The extension bundles its own language server and downloads a Java 25 runtime when the machine has none, so it works whether or not the souther command is installed.

Create a working directory and place a single businesstrip.sou file inside. Run all commands from this directory:

mkdir -p ~/tmp/businesstrip-tutorial
cd ~/tmp/businesstrip-tutorial

1. Creating the First Model from Existing Records

What You Will Learn: Use data and behavior to represent existing record fields and operations as an initial Souther model without implementations or test cases.

Update: Write the code block below to a new businesstrip.sou file.

Assume the following fields are currently recorded for a business trip application:

ApplicantID / Destination / EstimatedExpense / ActualExpense / Status / SubmittedAt / PreApprovedAt / FinalApprovedAt / SettlementAmount

There are four operations: submit, pre-approve, final approve, and settle. Model these fields as data and the operations as behavior. Submission, approval, and settlement timestamps and amounts use Option because they are absent in initial states.

module example.businesstrip

data EmployeeID = String
data Amount = Int

data Status = Draft | Submitted | PendingPreApproval | PreApproved | TripCompleted | Approved

data TripApplication =
    { applicantID: EmployeeID
    , destination: String
    , estimatedExpense: Amount
    , actualExpense: Option<Amount>
    , status: Status
    , submittedAt: Option<DateTime>
    , preApprovedAt: Option<DateTime>
    , finalApprovedAt: Option<DateTime>
    , settlementAmount: Option<Amount>
    }

behavior submitTrip : (app: TripApplication, submittedAt: DateTime) -> TripApplication
    constructs TripApplication

behavior preApprove : (app: TripApplication, preApprovedAt: DateTime) -> TripApplication
    constructs TripApplication

behavior finalApprove : (app: TripApplication, finalApprovedAt: DateTime) -> TripApplication
    constructs TripApplication

behavior calculateSettlement : (app: TripApplication) -> Amount
    constructs Amount

Run souther examples:

souther examples businesstrip.sou

The tool produces a report like this. Only submitTrip is shown here; the other three behaviors report the same shape:

example.businesstrip                                     measurement: complete
  submitTrip               injected      rows 0    pending 0
    signature   not applicable (this behavior's output is not a sum)
    partition   axes 6   equivalence partitions 0/0   (6 not measured: no row names this behavior)
      · divided no way: app.applicantID
      · divided no way: app.destination
      · divided no way: app.estimatedExpense
      · divided no way: app.actualExpense@Some
      · divided no way: app.submittedAt@Some
      · divided no way: app.preApprovedAt@Some
      · divided no way: app.finalApprovedAt@Some
      · divided no way: app.settlementAmount@Some
      · divided no way: submittedAt
    border      not applicable (the rules of this behavior draw no line)
    branch      not applicable (this behavior has no body)

4 behaviors: 0 implemented, 0 unimplemented, 4 injected; 0 rows waiting for a `let`.
adequacy: undetermined
  what keeps it open
    may change in a wider run     0
    unaffected by a wider run    24
      app.actualExpense of submitTrip — no row names this behavior
      app.status of submitTrip — no row names this behavior
      app.submittedAt of submitTrip — no row names this behavior
      app.preApprovedAt of submitTrip — no row names this behavior
      app.finalApprovedAt of submitTrip — no row names this behavior
      app.settlementAmount of submitTrip — no row names this behavior

The other three behaviors add six lines each to that list, for the same reason.

In the initial report, submitTrip shows signature not applicable. This indicates that the output type, TripApplication, is a single record type, so the report cannot determine whether test cases cover distinct output states. You can write expected values for the full record, but to distinguish Submitted and PendingPreApproval as output variants, states must be modeled as separate types.

branch not applicable (this behavior has no body) appears because no let implementation exists yet. Once state types are separated and implementation is added, the report can evaluate code branches.

adequacy: undetermined is not a verdict on the model. Adequacy is left open here because no test case names any of these behaviors, and the report says so under what keeps it open: each line is a position it could not answer for and why. unaffected by a wider run means running more of what is written would not settle these — what they wait on is a test case, not a longer search.

The nine divided no way lines include the Option fields as app.actualExpense@Some and so on: an optional field is a position the report reaches only where a value is there. divided no way says the rules of the behavior put no class boundary across the position, so there is nothing for a test case to be on one side or the other of.

2. Modeling States as Types

What You Will Learn: Instead of recording state in a Status field, create distinct types for each state. This expresses state transitions explicitly in behavior inputs and outputs.

Update: Replace Status and TripApplication from Section 1 with three state types and a sum type. Temporarily remove preApprove, finalApprove, and calculateSettlement.

To make output states measurable by signature, turn the output type into a sum type.

What happens after submitting a trip application?

Domain SME: “Applications exceeding 100,000 JPY require pre-approval by a manager. Others go directly to accounting.”

As a test case, this rule looks like:

example submitTrip
    | "Routes to accounting if 100,000 JPY is not exceeded" :
        (fukuokaTripDraft, DateTime("2026-07-27T09:00:00"))
            -> Submitted

The expected output is Submitted. In Section 1, Submitted was a value of type Status, while submitTrip returned TripApplication. Split states into types so that states can be returned directly.

data Draft =
    { applicantID: EmployeeID
    , destination: String
    , estimatedExpense: Amount
    }

data Submitted =
    { applicantID: EmployeeID
    , destination: String
    , estimatedExpense: Amount
    , submittedAt: DateTime
    }

data PendingPreApproval =
    { applicantID: EmployeeID
    , destination: String
    , estimatedExpense: Amount
    , submittedAt: DateTime
    }

data TripApplication = Draft | Submitted | PendingPreApproval

Draft has no submittedAt field because submission timestamp does not exist before submission. Separating state types eliminates Option for fields that are absent in a given state.

Draft | Submitted | PendingPreApproval is a sum type representing exactly one of these three types. For instance, Submitted contains submittedAt, whereas Draft does not. You know this from the type without checking a status field.

This is a modeling hint built into the type system: when an operation accepts Draft, it cannot be called with a Submitted application. Rather than distributing status checks throughout the code, make the valid states of an operation part of its input and output types. As the workflow grows, this keeps impossible transitions out of the model.

submitTrip takes a Draft and returns one of two states:

behavior submitTrip : (app: Draft, submittedAt: DateTime) -> Submitted | PendingPreApproval
    constructs Submitted, PendingPreApproval

Remove the other three behaviors for now; they will be redefined in Sections 7 and 8.

Define fukuokaTripDraft as a test fixture created with let name = value:

let fukuokaTripDraft = Draft
    { applicantID = EmployeeID("e-001")
    , destination = "Fukuoka"
    , estimatedExpense = Amount(28000)
    }

example submitTrip
    | "Routes to accounting if 100,000 JPY is not exceeded" :
        (fukuokaTripDraft, DateTime("2026-07-27T09:00:00"))
            -> Submitted
    | "Requires pre-approval if exceeding 100,000 JPY" :
        (Draft { ...fukuokaTripDraft, estimatedExpense = Amount(120000) },
         DateTime("2026-07-27T09:00:00"))
            -> PendingPreApproval

Draft { ... } constructs a record. { field = value } sets fields, and ...fukuokaTripDraft copies existing record fields while overriding specified fields.

  submitTrip               injected      rows 2    pending 2
    signature   out specified 2/2  observed 0/2  verified 0/2
    partition   not applicable (the rules of this behavior divide no position)
      · divided no way: app.applicantID
      · divided no way: app.destination
      · divided no way: app.estimatedExpense
      · divided no way: submittedAt
    border      not applicable (the rules of this behavior draw no line)
    branch      not applicable (this behavior has no body)

1 behavior: 0 implemented, 0 unimplemented, 1 injected; 2 rows waiting for a `let`.
adequacy: satisfied

signature now shows counts. specified 2/2 means the test cases cover both Submitted and PendingPreApproval. observed 0/2 indicates that the behavior is not yet implemented.

Next, add the behavior let. The threshold 100000 is not yet defined in the model; 120000 in the example is merely one input above the threshold.

3. Implementing the Behavior

What You Will Learn: A behavior declares an input/output contract, and a let provides decision logic. Implement submitTrip to enable test execution.

Update: Keep the submitTrip behavior declaration and add a matching let directly below it.

Express the rule “exceeds 100,000 JPY” as a condition:

let submitTrip (app, submittedAt) =
    if app.estimatedExpense.value > 100000
        then PendingPreApproval { ...app, submittedAt = submittedAt }
        else Submitted { ...app, submittedAt = submittedAt }

  submitTrip               implemented   rows 2    pending 0
    signature   out specified 2/2  observed 2/2  verified 2/2
    partition   axes 1   equivalence partitions 2/2
      · divided no way: app.applicantID
      · divided no way: app.destination
      · divided no way: submittedAt
    border      borders 1   obligations 2/4
      ! no row is at the ON point (comparison@32:35)
          · read as submitTrip/app.estimatedExpense: = 100001
      ! no row is at the OFF point (comparison@32:35)
          · read as submitTrip/app.estimatedExpense: = 100000
    branch      2/2
    decision    rules 2   taken 2

1 behavior: 1 implemented, 0 unimplemented, 0 injected; 0 rows waiting for a `let`.
adequacy: not satisfied
2 gaps marked `!`: what a strict build refuses over.

Now the report metrics show numbers. observed 2/2 verified 2/2 indicates both test cases passed. border obligations 2/4 names the two points no test case stands at: 100001, the first value the condition sends to pre-approval, and 100000, the last one below it. Each names where the line was drawn, comparison@32:35 — the comparison itself, not the if it was written in — and the line under it reads the point back as a value of a position, submitTrip/app.estimatedExpense. Both are marked !, which is what --strict refuses over and what the count on the last line is of.

decision rules 2 taken 2 is about the body rather than the inputs: the if states two rules, and a test case goes through each.

Whether 100000 belongs to pre-approval or direct submission must be confirmed against the business rules.

4. Turning Business Boundaries into Test Cases

What You Will Learn: Confirm exact boundary behavior with domain experts and reflect it in conditions and test cases.

Update: Change > to >= in the submission condition, then add test cases for 100,000 JPY and 99,999 JPY.

What happens at exactly 100,000 JPY?

Domain SME: “The regulations say ‘100,000 JPY or more.’ Exactly 100,000 JPY requires pre-approval.”

> 100000 was incorrect:

if app.estimatedExpense.value >= 100000

Generate boundary test scaffolds:

souther examples businesstrip.sou --generate

The report comes out first, and the rows follow it:

// generated by `souther examples --generate`: 2 rows to fill what nothing covers.
// Replace each `<?>` with what the system actually answers.
example submitTrip
    | (
        Draft {
            applicantID = EmployeeID("x"),
            destination = "x",
            estimatedExpense = Amount(100000)
        },
        DateTime("2000-01-01T00:00:00")
    )
        -> <?>
    | (
        Draft {
            applicantID = EmployeeID("x"),
            destination = "x",
            estimatedExpense = Amount(99999)
        },
        DateTime("2000-01-01T00:00:00")
    )
        -> <?>

The inputs are written for you; <?> is not, and the generator gives the rows no names. <?> is a row whose answer is owed: paste these in and the report counts them as rows waiting for one. Name each case and fill in the expected output from the business rules:

| "Exactly 100,000 JPY requires pre-approval" :
    (Draft { ...fukuokaTripDraft, estimatedExpense = Amount(100000) },
     DateTime("2026-07-27T09:00:00"))
        -> PendingPreApproval
| "99,999 JPY routes directly to accounting" :
    (Draft { ...fukuokaTripDraft, estimatedExpense = Amount(99999) },
     DateTime("2026-07-27T09:00:00"))
        -> Submitted

  submitTrip               implemented   rows 4    pending 0
    signature   out specified 2/2  observed 2/2  verified 2/2
    partition   axes 1   equivalence partitions 2/2
      · divided no way: app.applicantID
      · divided no way: app.destination
      · divided no way: submittedAt
    border      borders 1   obligations 4/4
    branch      2/2
    decision    rules 2   taken 2

1 behavior: 1 implemented, 0 unimplemented, 0 injected; 0 rows waiting for a `let`.
adequacy: satisfied

adequacy becomes satisfied. This means test coverage matches what the model currently declares.

5. Expressing Decision Reasons as Domain Values

What You Will Learn: Extract implicit conditions into explicit domain values named PreApprovalReason. Ensure that new reasons trigger compile-time checks if they are unhandled.

Update: Add Role to state types and fixtures. Replace submission condition logic with a reason-list builder, and add a decision behavior with test cases.

Domain SME: “General employees require manager pre-approval regardless of expense amount.”

Add Role to state types and fixtures:

data Role = Manager | GeneralEmployee

let isGeneralEmployee (role: Role): Bool =
    match role with
        | Manager         -> false
        | GeneralEmployee -> true

let submitTrip (app, submittedAt) =
    if app.estimatedExpense.value >= 100000 || isGeneralEmployee(app.role)
        then PendingPreApproval { ...app, submittedAt = submittedAt }
        else Submitted { ...app, submittedAt = submittedAt }

Next, replace inline boolean checks with explicit reason types:

data HighExpense = { threshold: Amount }
data InsufficientAuthority = { role: Role }
data PreApprovalReason = HighExpense | InsufficientAuthority
data PreApprovalReasonList = List<PreApprovalReason>

Determine the applicable reasons by filtering the candidate list:

let candidateReasons (role: Role): List<PreApprovalReason> =
    [ HighExpense { threshold = Amount(100000) }
    , InsufficientAuthority { role = role }
    ]

let isHighExpense (estimatedExpense: Amount, threshold: Amount): Bool =
    estimatedExpense.value >= threshold.value

let matchesReason (estimatedExpense: Amount, role: Role, reason: PreApprovalReason): Bool =
    match reason with
        | HighExpense { threshold } -> isHighExpense(estimatedExpense, threshold)
        | InsufficientAuthority     -> isGeneralEmployee(role)

let evaluatePreApprovalReasons (estimatedExpense: Amount, role: Role): List<PreApprovalReason> =
    List.filter(reason -> matchesReason(estimatedExpense, role, reason), candidateReasons(role))

behavior determinePreApprovalRequirement : (estimatedExpense: Amount, role: Role) -> PreApprovalReasonList
    constructs PreApprovalReasonList, HighExpense, InsufficientAuthority, Amount

let determinePreApprovalRequirement (estimatedExpense, role) =
    PreApprovalReasonList(evaluatePreApprovalReasons(estimatedExpense, role))

behavior submitTrip : (app: Draft, submittedAt: DateTime) -> Submitted | PendingPreApproval
    constructs Submitted, PendingPreApproval, PreApprovalReasonList, HighExpense, InsufficientAuthority, Amount

let submitTrip (app, submittedAt) = {
    let reasons = evaluatePreApprovalReasons(app.estimatedExpense, app.role)
    if List.isEmpty(reasons)
        then Submitted { ...app, submittedAt = submittedAt }
        else PendingPreApproval { ...app, submittedAt = submittedAt
                                , reasons = PreApprovalReasonList(reasons) }
}

Add test cases for determinePreApprovalRequirement:

example determinePreApprovalRequirement
    | "No reasons for Manager under 100,000 JPY" :
        (Amount(28000), Manager)
            -> PreApprovalReasonList([])
    | "HighExpense reason for exactly 100,000 JPY" :
        (Amount(100000), Manager)
            -> PreApprovalReasonList([ HighExpense { threshold = Amount(100000) } ])
    | "InsufficientAuthority reason for GeneralEmployee" :
        (Amount(28000), GeneralEmployee)
            -> PreApprovalReasonList([ InsufficientAuthority { role = GeneralEmployee } ])

If a new reason variant is added to PreApprovalReason, match expressions trigger exhaustive pattern matching errors (E1201) until handled.

This is another useful modeling signal. If a condition matters enough to explain a decision, give it a domain name and make it a case in a sum type. Adding a new case then identifies every decision that must account for it, instead of relying on searches for repeated boolean expressions.

6. Defining Invariants on Types

What You Will Learn: Write invariant rules on EmployeeID, Amount, and Destination so valid value constraints are enforced uniformly at construction time.

Update: Add invariants to EmployeeID, Amount, and Destination. Replace String destination with Destination type.

data EmployeeID = String
    invariant String.length(value) >= 1
data Amount = Int
    invariant value >= 0
data Destination = String
    invariant String.length(value) >= 1

Invariants add border points to souther examples: a minimum string length or a non-negative amount becomes a point some test case has to stand at. They are reported under declarations rather than under the behavior, because a rule about a value is owed a row wherever that value is constructed rather than in one behavior.

Add boundary test cases for 0 JPY and single-character strings to satisfy the report’s coverage requirements.

Place a rule in an invariant when it defines whether a value can exist, rather than whether a particular workflow step may proceed. This prevents the same validity check from being repeated across behaviors and makes invalid values unrepresentable once construction succeeds.

7. Distinguishing Reimbursement Targets by Type

What You Will Learn: Model expense items and payment responsibilities as explicit sum types so that only out-of-pocket expenses are included in reimbursement calculations.

Update: Replace estimated and actual expenses with detailed item lists. Add types for line items, payment responsibilities, settlement calculation behavior, and matching test cases.

data Origin = String
    invariant String.length(value) >= 1
data DestinationCity = String
    invariant String.length(value) >= 1
data AttendeeCount = Int
    invariant value >= 1
data ExpenseCategoryName = String
    invariant String.length(value) >= 1

data ExpenseCommon = { amount: Amount }

data TransportExpense = { ...ExpenseCommon, origin: Origin, destination: DestinationCity }
data LodgingExpense = { ...ExpenseCommon }
data EntertainmentExpense = { ...ExpenseCommon, attendees: AttendeeCount }
data OtherExpense = { ...ExpenseCommon, categoryName: ExpenseCategoryName }
data ExpenseCategory = TransportExpense | LodgingExpense | EntertainmentExpense | OtherExpense

data CompanyResponsibility = OutOfPocket | AdvancePayment | CorporateCard
data PaymentResponsibility = CompanyResponsibility | ThirdPartyPaid

data ExpenseItem = { category: ExpenseCategory, responsibility: PaymentResponsibility }

data EstimatedExpenses = List<ExpenseItem>
    invariant List.length(value) >= 1
data ActualExpenses = List<ExpenseItem>
    invariant List.length(value) >= 1
data SettlementAmount = Int
    invariant value >= 0

Implement settlement calculation:

let calculateReimbursement (item: ExpenseItem): Int =
    match item.responsibility with
        | CompanyResponsibility as company ->
            match company with
                | OutOfPocket    -> item.category.amount.value
                | AdvancePayment -> 0
                | CorporateCard  -> 0
        | ThirdPartyPaid -> 0

behavior calculateSettlement : (actual: ActualExpenses) -> SettlementAmount
    constructs SettlementAmount

let calculateSettlement (ActualExpenses(items)) =
    SettlementAmount(List.sum(List.map(calculateReimbursement, items)))

Add test cases covering out-of-pocket, corporate card, advance payment, and third-party expenses.

8. Expressing Business Rejections as Output Types

What You Will Learn: Represent business rejections (such as missing authority or a missing trip report) as explicit sum-type outputs rather than unhandled exceptions.

Update: Wrap employee fields in Employee. Add state types and behaviors for approval, trip completion, and final approval with rejection outputs and test cases.

Souther has no exceptions for modeling business outcomes. That constraint is intentional: a rejected approval, missing report, or invalid expense is data that the caller must be able to see and handle. Include each expected outcome in the behavior’s output sum type, and reserve integration failures such as an unavailable external service for the application boundary.

data Employee =
    { employeeID: EmployeeID
    , role: Role
    , managerID: EmployeeID
    }

data TripReport = String
    invariant String.length(value) >= 1

data PreApprovedRecord =
    { preApprovedAt: DateTime
    , preApproverID: EmployeeID
    }

data NoPreApproval
data PreApprovalHistory = NoPreApproval | PreApprovedRecord

data UnauthorizedApproval
data InvalidActualExpenses
data MissingTripReport

data TripCompleted =
    { applicant: Employee
    , destination: Destination
    , estimatedExpenses: EstimatedExpenses
    , submittedAt: DateTime
    , actualExpenses: ActualExpenses
    , completedAt: DateTime
    , report: TripReport
    , preApproval: PreApprovalHistory
    }

data PendingFinalApproval = { ...TripCompleted }

behavior preApprove : (app: PendingPreApproval, approverID: EmployeeID, preApprovedAt: DateTime)
    -> PreApproved | UnauthorizedApproval
    constructs PreApproved, PreApprovedRecord

let preApprove (app, approverID, preApprovedAt) = {
    guard approverID == app.applicant.managerID else UnauthorizedApproval
    PreApproved { ...app
        , preApproval = PreApprovedRecord { preApprovedAt = preApprovedAt, preApproverID = approverID } }
}

behavior completeTrip : (app: InTransitTrip, items: List<ExpenseItem>, reportText: String, completedAt: DateTime)
    -> TripCompleted | InvalidActualExpenses | MissingTripReport
    constructs TripCompleted, ActualExpenses, TripReport

let completeTrip (app, items, reportText, completedAt) = {
    guard ActualExpenses(items) as actual else InvalidActualExpenses
    guard List.sum(List.map(item -> item.category.amount.value, items)) > 0 else InvalidActualExpenses
    guard TripReport(reportText) as report else MissingTripReport

    match app with
        | Submitted as submitted ->
            TripCompleted { ...submitted
                , actualExpenses = actual
                , completedAt = completedAt
                , report = report
                , preApproval = NoPreApproval }
        | PreApproved as preApproved ->
            TripCompleted { ...preApproved
                , actualExpenses = actual
                , completedAt = completedAt
                , report = report
                , preApproval = preApproved.preApproval }
}

behavior requestFinalApproval : (completed: TripCompleted) -> PendingFinalApproval
    constructs PendingFinalApproval

let requestFinalApproval (completed) = PendingFinalApproval { ...completed }

behavior finalApprove : (app: PendingFinalApproval, approverID: EmployeeID, finalApprovedAt: DateTime)
    -> Approved | UnauthorizedApproval
    constructs Approved, SettlementAmount

let finalApprove (app, approverID, finalApprovedAt) = {
    guard approverID == app.applicant.managerID else UnauthorizedApproval
    Approved { ...app
        , finalApprovedAt = finalApprovedAt
        , finalApproverID = approverID
        , settlementAmount = SettlementAmount(List.sum(List.map(calculateReimbursement, app.actualExpenses.value))) }
}

NoPreApproval, UnauthorizedApproval, InvalidActualExpenses, and MissingTripReport are unit data: they carry no fields, and one value is all there is of each. A unit data is not named in constructs, which is about what a behavior is allowed to build; naming one there is E1026.

Add test cases asserting both successful transitions and rejection outputs (UnauthorizedApproval, InvalidActualExpenses, MissingTripReport).

9. Using Report Gaps to Drive the Next Test Cases

What You Will Learn: Read gaps in the report’s partition and border metrics to determine missing test scenarios. Use --strict in CI.

Update: Add a test case for final approval on pre-approved applications. Review --behavior, --generate, and --strict flags.

Filter reports for a single behavior:

souther examples businesstrip.sou --behavior finalApprove

  finalApprove             implemented   rows 2    pending 0
    signature   out specified 2/2  observed 2/2  verified 2/2
    partition   axes 6   equivalence partitions 6/20
      ! no row is in `Manager` at app.applicant.role
      ! no row is in `PreApprovedRecord` at app.preApproval
      · app.applicant.role holds 2 classes and this behavior's rules compose 0 of them
      · no line: comparison@195:22 — it relates two positions rather than dividing one, about `approverID`
    combination pairs 15 covered, 149 unknown; no row is owed at one
      · app.applicant.role × app.preApproval: 1 covered, 3 unknown
    border      borders 24   obligations 0/0
    branch      4/7
      ! no row goes through `case AdvancePayment` (139:13)
    decision    rules 2   taken 2
  declarations   obligations 6/20
  Amount
      ! no row is at the ON point value = 0 (invariant Amount #1)

The rest of the positions, pairs, border points and branch cases the report names one by one are left out above. The counts depend on the types you defined in Section 8, so yours will differ.

no row is in PreApprovedRecord highlights that no test case evaluates final approval for an application that went through pre-approval. Adding that scenario covers the missing path.

no line: comparison@195:22 — it relates two positions rather than dividing one is the report declining to invent a class boundary: approverID == app.applicant.managerID compares two inputs, so neither side has a value the other can be measured against. border obligations 0/0 says the same of this behavior’s own lines, while the invariants of the types it reaches are counted under declarations, where a rule about a value is owed a row wherever that value is constructed.

Treat these gaps as questions about the model, not merely a coverage target. A missing partition can reveal a business case that has not been decided, and a missing border can reveal an ambiguous rule. The report helps turn those questions into the next conversation with a domain expert and the next executable example.

In CI pipelines, run with --strict to enforce zero report gaps. It refuses over the items marked !, which the report counts on its last line:

souther examples businesstrip.sou --strict

Homework

You now have the main pipeline from submission to final approval. In businesstrip/src/main/souther/businesstrip.sou, you can explore these additional domain rules:

Rejections (rejectPreApproval and rejectFinalApproval) handling empty rejection reasons via RejectionReason invariants and MissingRejectionReason output variants.
Remands (sendBack) converting rejected applications back into Draft while ensuring rejection reasons are cleared by type constraints.
Third-party expense coverage as a third pre-approval trigger reason.
Lodging expense invoice registration number validation (InvoiceRegistrationNumber) using string pattern matching in invariant.
Trip start and end dates validated via cross-field invariants in common application data.
Separating test cases into businesstrip.examples.sou using examples for example.businesstrip.