Methodical Programming (Programación Metódica)

Apply rigorous, mathematically-grounded program construction and verification techniques. Programs are derived from formal specifications rather than written ad-hoc and tested afterwards. This skill is language-agnostic and applies to any programming paradigm.

Core Principles

1. Specification Before Code

Every function/procedure MUST be specified with:

• Precondition (Pre): Conditions the inputs must satisfy.
• Postcondition (Post): Relations that must hold between inputs and outputs.

function f(params) returns results
  {Pre: conditions on params}
  {Post: relations between params and results}

A program is correct when its actual behavior matches its specification. The weaker the precondition, the more reusable the function. The stronger the postcondition, the more useful the function.

2. Derivation Over Verification

• Verification: Proving an existing program meets its specification (post-hoc).
• Derivation: Constructing a program that is correct by construction from its specification.

Always prefer derivation. Derive code from the postcondition analysis:

• Equalities between program variables and expressions → solve via assignments.
• Disjunctions in postcondition → design an alternative/conditional (if/match/switch).
• Conjunctions in postcondition → attempt sequential composition or conditional branches.

3. States, Assertions and Substitutions

• A state is the mapping of all variables to their current values at a given program point.
• An assertion (aserto) is a logical expression over program variables describing a set of valid states.
• Substitution A[x ← E]: replace every free occurrence of x in assertion A with expression E. This is the key operation for reasoning about assignments.

Instruction Semantics (Axiomatic)

Apply these rules regardless of language syntax.

Skip / No-op

{A} skip {A}

Everything true before is true after.

Assignment

{A[x ← E]} x := E {A}

To prove {P} x := E {Q}, demonstrate:

1. Expression E can be evaluated without errors.
2. P ⟹ Q[x ← E] (the precondition implies the postcondition with x replaced by E).

Multiple Assignment (Simultaneous)

<x₁, x₂, ..., xₙ> := <E₁, E₂, ..., Eₙ>

All expressions are evaluated using values before the assignment. This is important when variables appear in expressions on the right side.

Sequential Composition

{A₁} P₁ ; P₂ {A₃}

Find an intermediate assertion A₂ such that {A₁} P₁ {A₂} and {A₂} P₂ {A₃}.

Conditional / Alternative

{Pre}
if B₁ → S₁
   B₂ → S₂
   ...
   Bₙ → Sₙ
end if
{Post}

Verify:

1. Completeness: Pre ⟹ B₁ ∨ B₂ ∨ ... ∨ Bₙ (at least one branch is open).
2. Correctness per branch: {Pre ∧ Bᵢ} Sᵢ {Post} for each i.

Function Call

<x₁, ..., xₘ> := f(e₁, ..., eₖ)

1. Before the call: prove the arguments satisfy the function's precondition.
2. After the call: the result variables satisfy the postcondition (with parameter/result renaming).

Quantifiers and Hidden Operations

Use quantifiers to express specifications concisely. Each has a neutral element (value on empty domain):

Splitting a quantifier — separate one element from the domain and combine with the binary operation:

Σ(a: 1≤a≤n: f(a)) = Σ(a: 1≤a≤n-1: f(a)) + f(n)
MAX(a: 1≤a≤n: f(a)) = max(MAX(a: 1≤a≤n-1: f(a)), f(n))

The neutral element defines the base case for recursion and the initialization for iteration.

Algebraic Data Types

When using a data type, reason through its algebraic specification:

1. Signature: Types (genres) and operations with their arities.
2. Equations: Algebraic identities that define operation behavior.
3. Constructors: Minimal set of operations that can build any value of the type (used as the basis for induction).

Common Structures

List: Constructors [] (empty) and e:l (cons). Operations: ++ (concat), length.

[] ++ l₂ ≡ l₂
(e:l₁) ++ l₂ ≡ e:(l₁ ++ l₂)
length([]) ≡ 0
length(e:l) ≡ 1 + length(l)

Stack (LIFO): Constructors empty_stack and push(e, s). Operations: top, pop, is_empty.

top(empty_stack) ≡ error
top(push(e, s)) ≡ e
pop(push(e, s)) ≡ s
is_empty(empty_stack) ≡ true
is_empty(push(e, s)) ≡ false

Queue (FIFO): Constructors empty_queue and enqueue(e, q). Operations: front, dequeue, is_empty.

Binary Tree: Constructors empty_tree and plant(e, left, right). Operations: root, left, right, is_empty, height, size.

height(empty_tree) ≡ 0
height(plant(e, a₁, a₂)) ≡ 1 + max(height(a₁), height(a₂))
size(plant(e, a₁, a₂)) ≡ 1 + size(a₁) + size(a₂)

Table/Map: Constructors create and assign(t, index, value). Operations: lookup, defined.

Use the constructor set to identify the induction structure of each type.

Principle of Induction

To prove properties of data types, identify the constructors and reason by structural induction:

[P(base) ∧ ∀x (P(smaller(x)) ⟹ P(x))] ⟹ ∀z P(z)

• Base case: Prove the property for values built with nullary constructors (empty list, empty stack, etc.).
• Inductive step: Assuming the property holds for all sub-structures, prove it for the composed structure.

A well-founded preorder (noetherian) is required: no infinite strictly decreasing sequences exist. This guarantees that induction and recursion terminate.

Recursive Programs

Pattern

Every recursive function follows this structure:

function f(x) returns r
  {Pre: Q(x)}
  if d(x) →          // direct case
    r := h(x)
  ¬d(x) →            // recursive case
    v := f(s(x))
    r := c(x, v)
  end if
  {Post: R(x, r)}
  return r

Verification Steps

1. Direct case correctness: Q(x) ∧ d(x) ⟹ R(x, h(x))
2. Recursive case — legal call: Q(x) ∧ ¬d(x) ⟹ Q(s(x)) (precondition holds for recursive argument)
3. Recursive case — correctness: Q(x) ∧ ¬d(x) ∧ R(s(x), v) ⟹ R(x, c(x, v))
4. Bounding function t(x): Define t: params → ℕ such that:
   • Q(x) ⟹ t(x) ∈ ℕ (always a natural number)
   • Q(x) ∧ ¬d(x) ⟹ t(s(x)) < t(x) (strictly decreases at each recursive call)

Bounding Function Heuristics

Recursion Types

• Linear recursion: Each call generates at most one recursive call.
• Multiple recursion: A call may generate more than one recursive call (e.g., tree traversals).

Methodology for Designing Recursive Programs

1. Specify the function: header, precondition, postcondition.
2. Identify the bounding function t(x) — the expression for induction over ℕ.
3. Analyze cases: Identify at least one direct case and one recursive case. Ensure all cases are covered.
4. Program and verify each case. For recursive cases, assume (by induction hypothesis) that recursive calls satisfy the specification.
5. Validate termination: Prove t(x) decreases strictly at each recursive call.

Algorithm Immersion (Generalization)

When a direct recursive solution is not found, not efficient, or hard to reason about, generalize the function by adding parameters and/or results. This is called immersion.

Techniques

Strengthen the Precondition

1. Weaken the postcondition (possibly introducing new variables).
2. Strengthen the precondition with the weakened postcondition — require a partial version of the result as input.
3. Add immersion parameters so the new precondition makes sense.
4. Keep the original postcondition.

The weakened postcondition provides ideas for:

• Base case guard: The condition that "inverts" the weakening.
• Recursive case: Only immersion parameters change between calls → tail recursion with constant postcondition.

Weaken the Postcondition

1. Introduce new variables replacing sub-expressions in the postcondition.
2. Drop some equalities → weaker requirement.
3. The dropped equalities become the initializations to recover the original function from the immersion.
4. Strengthen the precondition with domain conditions on the new parameters as needed.

Efficiency Immersion

When a complex expression f(x) must be recomputed at every recursive call:

• As extra result: Add w = f(x) to the postcondition. After a recursive call with s(x), update w from f(s(x)) to f(x).
• As extra parameter: Add w = f(x) to the precondition. Use w instead of computing f(x). When making recursive calls, compute the new parameter value from the current w.

Unfold/Fold Technique (Tail Recursion Transformation)

Transform linear recursion into tail recursion:

1. Given f(x) = c(f(s(x)), x) (linear recursive case), define immersion g(y, w) = c(f(y), w).
2. Unfold: Substitute f's cases into g's definition.
3. Fold: Manipulate the expression back into g's form.
4. The result is a tail-recursive g, with f(x) = g(x, neutral) where neutral is the identity element of c.

Iterative Programs (Loops)

While Loop Semantics

{Invariant I}
while B do
  S
end while
{Post: Q}

Verification (Two Phases)

Phase 1 — Partial Correctness:

1. Define an invariant I: a condition that holds at the start of every iteration.
2. Initialization: Pre ⟹ I (the precondition implies the invariant).
3. Maintenance: {I ∧ B} S {I} (the body preserves the invariant).
4. Exit: I ∧ ¬B ⟹ Post (invariant + loop exit condition implies postcondition).

Phase 2 — Termination:

1. Define a bounding function t with values in ℕ.
2. Bounded: I ∧ B ⟹ t > 0.
3. Decreasing: {I ∧ B ∧ t = T} S {t < T} (the body strictly decreases the bound).

Transformation: Tail Recursion → Iteration

A tail-recursive function with constant postcondition transforms directly into a while loop:

Direct Iterative Derivation

1. The invariant core is typically a weakened postcondition.
2. Design guarded instructions that preserve the invariant and decrease the bounding function.
3. Sufficient cases are covered when: Invariant ∧ ¬(B₁ ∨ B₂ ∨ ... ∨ Bₙ) ⟹ Post.

Workflow Summary

When writing any function, follow this process:

1. Specify: Write precondition and postcondition. Identify input/output types.
2. Analyze the postcondition: Determine if the solution requires assignment, conditionals, recursion, or iteration.
3. Choose strategy:
   • Simple postcondition with equalities → direct assignment/composition.
   • Disjunctions → conditional/alternative.
   • Inductive structure → recursion or iteration.
4. For recursive solutions:
   • Identify cases (direct + recursive).
   • Define bounding function.
   • Verify each case.
   • Consider immersion if needed for efficiency or tail recursion.
5. For iterative solutions:
   • Derive invariant (weakened postcondition).
   • Define bounding function.
   • Design loop body that preserves invariant and decreases bound.
   • Set initializations and post-loop code.
6. Verify: Ensure all proof obligations are met — or derive code so they hold by construction.

Applying This Skill

When generating or reviewing code in any language:

• Always think in terms of preconditions and postconditions, even if the language doesn't enforce them. Document them as comments, assertions, type constraints, or contracts.
• Use assertions/contracts available in the language (assert, require, ensure, design-by-contract libraries, property-based tests) to encode pre/post conditions.
• When designing recursive functions, explicitly identify the bounding function and verify termination.
• When designing loops, explicitly state the invariant and bounding function.
• Prefer deriving code from specifications over writing code and testing afterwards.
• When a recursive solution is not tail-recursive, consider immersion techniques to transform it.
• Use algebraic reasoning over data structures: define operations by their equations, reason by structural induction.
• Encode bounding functions as decreasing measures where the language supports it (e.g., Dafny's decreases, Coq's structural recursion, or manual assertions).

Connecting Formal Specifications to Tests

Formal specifications (preconditions and postconditions) and tests express the same idea in different languages: one in logic, the other in executable code. Deriving tests from the specification — rather than from the implementation — closes the loop: the tests are correct by the same reasoning that makes the code correct.

1. Specification → Tests

Every element of a formal specification maps to a concrete test:

Worked example — sum(list)

function sum(list) returns result
  {Pre:  list is a list of numbers}
  {Post: result = Σ(a: a ∈ list: a)}

The neutral element of Σ is 0, so the base case is sum([]) = 0. The inductive constructor e:l produces the minimal test sum([5]) = 5, and the general case sum([1, 2, 3]) = 6.

TypeScript (Jest / Vitest)

// sum.test.ts
import { sum } from "./sum";

it("returns 0 for empty list — neutral element of Σ", () => {
  expect(sum([])).toBe(0);
});

it("returns the element itself for a singleton — minimal inductive case", () => {
  expect(sum([5])).toBe(5);
});

it("returns the total for a general list", () => {
  expect(sum([1, 2, 3])).toBe(6);
});

it("rejects non-numbers — precondition violation", () => {
  expect(() => sum(["a"] as any)).toThrow();
});

Go (testing)

// sum_test.go
func TestSumEmptyList(t *testing.T) {
    // Base case: neutral element of Σ is 0
    if got := Sum([]int{}); got != 0 {
        t.Errorf("Sum([]) = %d, want 0", got)
    }
}

func TestSumSingleton(t *testing.T) {
    // Minimal inductive case: one recursive step falling into base case
    if got := Sum([]int{5}); got != 5 {
        t.Errorf("Sum([5]) = %d, want 5", got)
    }
}

func TestSumGeneralList(t *testing.T) {
    if got := Sum([]int{1, 2, 3}); got != 6 {
        t.Errorf("Sum([1,2,3]) = %d, want 6", got)
    }
}

2. Testing Recursive Cases

Every recursive function has the structure:

function f(x):
  if d(x)  → h(x)           -- direct case
  ¬d(x)    → c(x, f(s(x)))  -- recursive case

This structure directly determines the test suite:

• Direct case (d(x) is true): test the base case. The expected value is the neutral element of the quantifier that the postcondition expresses.
• Minimal recursive case (¬d(x) with s(x) falling into the direct case): test with the smallest input that triggers exactly one recursive call.
• General case: test with an input that triggers multiple recursive calls.
• Bounding function t(x): when termination is non-obvious, use a call counter or spy to confirm the number of recursive calls does not exceed t(x_initial).

Worked example — length(list)

function length(list) returns n
  {Pre:  list is a list}
  {Post: n = N(a: a ∈ list: true)}
  if list = []  → n := 0                      -- d(x): list is empty
  list ≠ []     → n := 1 + length(tail(list)) -- recursive case

Bounding function: t(list) = length(list) (the size of the input structure).

TypeScript (Jest / Vitest)

// length.test.ts
import { length } from "./length";

it("returns 0 for empty list — direct case, neutral of N", () => {
  expect(length([])).toBe(0);
});

it("returns 1 for singleton — one recursive call into base", () => {
  expect(length([7])).toBe(1);
});

it("returns correct length for general list", () => {
  expect(length([1, 2, 3])).toBe(3);
});

Go (testing)

// length_test.go
func TestLengthEmpty(t *testing.T) {
    if got := Length([]int{}); got != 0 {
        t.Errorf("Length([]) = %d, want 0", got)
    }
}

func TestLengthSingleton(t *testing.T) {
    if got := Length([]int{7}); got != 1 {
        t.Errorf("Length([7]) = %d, want 1", got)
    }
}

func TestLengthGeneral(t *testing.T) {
    if got := Length([]int{1, 2, 3}); got != 3 {
        t.Errorf("Length([1,2,3]) = %d, want 3", got)
    }
}

Zig (std.testing + comptime table)

Zig's idiomatic pattern for multiple cases is inline for over a comptime array — zero-cost parametric tests with no external library:

const std = @import("std");
const length = @import("length").length;

test "length — direct case, recursive case, general" {
    const cases = comptime [_]struct {
        input: []const i32,
        expected: usize,
    }{
        .{ .input = &[_]i32{},        .expected = 0 }, // direct case: d(x)
        .{ .input = &[_]i32{7},       .expected = 1 }, // minimal recursive case
        .{ .input = &[_]i32{ 1, 2, 3 }, .expected = 3 }, // general case
    };

    inline for (cases) |c| {
        try std.testing.expectEqual(c.expected, length(c.input));
    }
}

3. Property-Based Testing for Universal Postconditions

When the postcondition contains a universal quantifier (∀), manual tests verify only finitely many cases of an infinite truth. Property-based testing (PBT) generates random inputs, checks the property for each, and — on failure — shrinks the counterexample to the minimal failing case.

Rule: if the postcondition has the form ∀x ∈ domain: P(x), write a property test, not just examples.

Worked example — algebraic properties of reverse

{Post₁: ∀l: length(reverse(l)) = length(l)}   -- reverse preserves length
{Post₂: ∀l: reverse(reverse(l)) = l}           -- reverse is an involution

TypeScript — fast-check

// reverse.property.test.ts
import * as fc from "fast-check";
import { reverse } from "./reverse";

test("Post₁: reverse preserves length — ∀l", () => {
  fc.assert(
    fc.property(fc.array(fc.integer()), (l) => {
      return reverse(l).length === l.length;
    })
  );
});

test("Post₂: reverse is an involution — ∀l", () => {
  fc.assert(
    fc.property(fc.array(fc.integer()), (l) => {
      const rr = reverse(reverse(l));
      return rr.length === l.length && l.every((v, i) => v === rr[i]);
    })
  );
});

Go — rapid

// reverse_property_test.go
import (
    "testing"
    "pgregory.net/rapid"
)

func TestReversePreservesLength(t *testing.T) {
    // Post₁: ∀l: length(reverse(l)) = length(l)
    rapid.Check(t, func(t *rapid.T) {
        l := rapid.SliceOf(rapid.Int()).Draw(t, "l")
        if len(Reverse(l)) != len(l) {
            t.Fatalf("length(Reverse(%v)) ≠ length(%v)", l, l)
        }
    })
}

func TestReverseIsInvolution(t *testing.T) {
    // Post₂: ∀l: reverse(reverse(l)) = l
    rapid.Check(t, func(t *rapid.T) {
        l := rapid.SliceOf(rapid.Int()).Draw(t, "l")
        got := Reverse(Reverse(l))
        if len(got) != len(l) {
            t.Fatalf("len(Reverse(Reverse(%v))) = %d, want %d", l, len(got), len(l))
        }
        for i := range l {
            if got[i] != l[i] {
                t.Fatalf("Reverse(Reverse(%v)) = %v, want %v", l, got, l)
            }
        }
    })
}

Zig — comptime table + built-in fuzzer

Zig has no idiomatic PBT library. Use two complementary approaches:

1. inline for over comptime array for representative cases derived from the specification (base, minimal inductive, edge values).
2. zig test --fuzz for no-crash / no-panic invariants — the built-in fuzzer feeds arbitrary bytes and catches panics, out-of-bounds accesses, and undefined behavior.

const std = @import("std");
const reverse = @import("reverse").reverse;

// Post₁ + Post₂: representative cases covering base and inductive constructors
test "reverse — spec-derived cases" {
    const allocator = std.testing.allocator;
    const cases = comptime [_]struct {
        input: []const i32,
        expected: []const i32,
    }{
        .{ .input = &[_]i32{},        .expected = &[_]i32{} },
        .{ .input = &[_]i32{1},       .expected = &[_]i32{1} },
        .{ .input = &[_]i32{ 1, 2, 3 }, .expected = &[_]i32{ 3, 2, 1 } },
    };

    inline for (cases) |c| {
        const result = try reverse(allocator, c.input);
        defer allocator.free(result);
        try std.testing.expectEqual(c.expected.len, result.len);
        try std.testing.expectEqualSlices(i32, c.expected, result);
    }
}

// Post₁ no-panic invariant: reverse must not crash on any input
test "reverse — fuzz no-panic" {
    const input = std.testing.fuzzInput(.{});
    const allocator = std.testing.allocator;
    const n = input.len / @sizeOf(i32);

    // Decode fuzz bytes into i32 values without assuming alignment.
    var buf = std.ArrayList(i32).init(allocator);
    defer buf.deinit();
    try buf.ensureTotalCapacity(n);

    var i: usize = 0;
    while (i < n) : (i += 1) {
        const base = i * @sizeOf(i32);
        const chunk = input[base .. base + @sizeOf(i32)];
        const value = std.mem.bytesToValue(i32, chunk);
        buf.appendAssumeCapacity(value);
    }

    const data: []const i32 = buf.items;
    const result = reverse(allocator, data) catch return;
    defer allocator.free(result);
    try std.testing.expectEqual(data.len, result.len);
}
// Run with: zig test reverse_test.zig --fuzz

Terraform — native terraform test (.tftest.hcl)

Terraform has no PBT. Universal postconditions (∀) are expressed with alltrue([for ... : ...]) inside an assert block. Boundary cases and precondition violations each get a separate run block — there are no loops in .tftest.hcl.

# tests/subnets_unit_test.tftest.hcl

# Post: ∀subnet ∈ aws_subnet.private: subnet.cidr_block ∈ "10.0.0.0/8"
run "all_private_subnets_in_range" {
  command = plan

  assert {
    condition = alltrue([
      for s in aws_subnet.private : can(regex("^10\\.0\\.", s.cidr_block))
    ])
    error_message = "All private subnets must be in the 10.0.x.x range."
  }
}

# Pre violated: cidr_block outside allowed range must be rejected
run "invalid_cidr_rejected" {
  command = plan

  variables {
    cidr_block = "192.168.1.0/24"
  }

  expect_failures = [var.cidr_block]
}

# Boundary: minimum allowed subnet count
run "minimum_subnet_count" {
  command = plan
  variables { subnet_count = 1 }

  assert {
    condition     = length(aws_subnet.private) == 1
    error_message = "Expected exactly 1 subnet."
  }
}

# Boundary: zero subnets must be rejected by variable validation
run "zero_subnets_rejected" {
  command = plan
  variables { subnet_count = 0 }

  expect_failures = [var.subnet_count]
}

4. The Combined Workflow

Formal derivation and TDD are not alternatives — they are two layers of the same process. The specification is the source of truth; both the code and the tests are derived from it independently.

1. Specify   Write Pre and Post formally.
             Identify the quantifier structure (Σ, ∀, N, ...) and its neutral element.
             Identify constructors of the input type (base + inductive).

2. Red       Translate Pre/Post into tests — all must fail (code does not exist yet):
             · Pre violated              → unhappy-path test / expect_failures
             · Base constructor          → test of the quantifier's neutral element
             · Minimal inductive case    → test with one recursive step into base
             · Postcondition with ∀      → property test (fast-check / rapid)
                                           or alltrue([for...]) in Terraform
             · Each postcondition branch → one test per disjunct

3. Derive    Construct the code from the postcondition analysis (not from the tests).
             Choose the strategy that matches the postcondition structure:
             equalities → assignment, disjunctions → conditional, inductive → recursion/loop.

4. Green     The tests pass on the first run — by construction, not by adjustment.
             If a test fails, the derivation has a gap: re-examine the proof obligation.

5. Refactor  Improve structure, names, efficiency. The tests stay green.
             The formal invariant guarantees that refactoring preserves correctness.
             Immersion (tail-recursion transformation) is a safe refactoring step
             because the postcondition is unchanged.

Key insight: when code and tests are both derived from the same specification, the red-green-refactor cycle collapses into specify → derive → verify. Tests written against the specification — not against the implementation — cannot be accidentally made to pass by wrong code that happens to match the test. They fail for the right reason and pass for the right reason.