Common Refinement Patterns

Common Refinement Patterns

Catalog of frequently used refinement patterns across different domains.

Data Structure Refinement

Set Refinements

Set → List

When to use: Simple set operations, small sets, order doesn't matter.

Abstraction:

α(xs) = set(xs)

Operations:

• Empty: [] ↔ ∅
• Insert: x :: xs ↔ {x} ∪ S
• Member: x ∈ set(xs) ↔ x ∈ S
• Union: xs ++ ys ↔ S₁ ∪ S₂

Proof obligations:

• Preserve set semantics
• Handle duplicates correctly

Example (Isabelle):

definition set_insert_list :: "'a ⇒ 'a list ⇒ 'a list" where
  "set_insert_list x xs = (if x ∈ set xs then xs else x # xs)"

lemma "set (set_insert_list x xs) = insert x (set xs)"
  by (auto simp: set_insert_list_def)

Set → Sorted List

When to use: Need efficient membership testing, maintain order.

Abstraction:

α(xs) = set(xs) where sorted(xs)

Operations:

• Insert: Binary search insertion
• Member: Binary search
• Union: Merge operation

Invariant: List remains sorted after each operation.

Set → Binary Search Tree

When to use: Efficient insert/lookup, balanced operations.

Abstraction:

α(tree) = {x | x in tree}

Operations:

• Insert: O(log n) average
• Member: O(log n) average
• Delete: O(log n) average

Invariant: BST property maintained.

Set → Hash Set

When to use: Very large sets, constant-time operations needed.

Abstraction:

α(buckets) = ⋃ᵢ set(buckets[i])

Operations:

• Insert: O(1) average
• Member: O(1) average
• Collision handling required

Map Refinements

Map → Association List

When to use: Small maps, simple implementation.

Abstraction:

α([(k₁,v₁), ..., (kₙ,vₙ)]) = {k₁ ↦ v₁, ..., kₙ ↦ vₙ}

Operations:

• Lookup: Linear search
• Update: Prepend new binding
• Delete: Filter out key

Example (Coq):

Fixpoint alist_lookup {K V} (eq : K -> K -> bool) (k : K) (al : list (K * V)) :=
  match al with
  | [] => None
  | (k', v) :: rest => if eq k k' then Some v else alist_lookup eq k rest
  end.

Map → Binary Search Tree Map

When to use: Ordered keys, efficient operations.

Abstraction:

α(tree) = {k ↦ v | (k,v) in tree}

Operations:

• Lookup: O(log n)
• Update: O(log n)
• Ordered iteration possible

Map → Hash Map

When to use: Large maps, no ordering needed.

Abstraction:

α(buckets) = ⋃ᵢ map_of(buckets[i])

Operations:

• Lookup: O(1) average
• Update: O(1) average
• Hash function required

Sequence Refinements

Sequence → Array

When to use: Random access, fixed size.

Abstraction:

α(arr) = [arr[0], arr[1], ..., arr[n-1]]

Operations:

• Index: O(1)
• Update: O(1)
• Length: O(1)

Constraint: Fixed size after creation.

Sequence → Linked List

When to use: Frequent insertions/deletions at ends.

Abstraction:

α(list) = sequence of elements

Operations:

• Prepend: O(1)
• Head: O(1)
• Tail: O(1)
• Index: O(n)

Sequence → Dynamic Array

When to use: Variable size, amortized constant append.

Abstraction:

α(arr, size, capacity) = arr[0..size-1]

Operations:

• Append: O(1) amortized
• Index: O(1)
• Resize: O(n) when needed

Invariant: size ≤ capacity

Algorithmic Refinement

Specification to Divide-and-Conquer

Pattern: Refine specification to recursive decomposition.

Example: Sorting

Abstract:

sort(xs) = ys where sorted(ys) ∧ perm(xs, ys)

Refined (Merge Sort):

sort(xs) = if |xs| ≤ 1 then xs
           else merge(sort(left), sort(right))
           where (left, right) = split(xs)

Proof obligations:

• Termination: Size decreases
• Correctness: Merge preserves sorting and permutation

Specification to Greedy Algorithm

Pattern: Refine to locally optimal choices.

Example: Minimum Spanning Tree

Abstract:

MST(G) = T where tree(T) ∧ spans(T, G) ∧ minimal_weight(T)

Refined (Kruskal's):

MST(G) =
  edges_sorted = sort_by_weight(edges(G))
  forest = empty
  for e in edges_sorted:
    if not creates_cycle(forest, e):
      forest = forest ∪ {e}
  return forest

Specification to Dynamic Programming

Pattern: Refine to memoized recursion.

Example: Fibonacci

Abstract:

fib(n) = if n ≤ 1 then n else fib(n-1) + fib(n-2)

Refined (Memoized):

fib_memo(n, memo) =
  if n in memo: return memo[n]
  if n ≤ 1: result = n
  else: result = fib_memo(n-1, memo) + fib_memo(n-2, memo)
  memo[n] = result
  return result

Implementation Refinement

Naive to Tail-Recursive

Pattern: Eliminate stack growth with accumulator.

Example: List Reversal

Naive:

reverse([]) = []
reverse(x :: xs) = reverse(xs) ++ [x]

Tail-Recursive:

reverse_acc([], acc) = acc
reverse_acc(x :: xs, acc) = reverse_acc(xs, x :: acc)

reverse(xs) = reverse_acc(xs, [])

Proof obligation:

reverse_acc(xs, acc) = reverse(xs) ++ acc

Functional to Imperative

Pattern: Refine pure functions to stateful procedures.

Example: Array Sum

Functional:

sum([]) = 0
sum(x :: xs) = x + sum(xs)

Imperative:

sum_imperative(arr):
  total = 0
  for i = 0 to length(arr) - 1:
    total = total + arr[i]
  return total

Proof obligation:

Loop invariant: total = sum(arr[0..i-1])

Single-Pass to Multi-Pass

Pattern: Trade time for space or vice versa.

Example: Finding Min and Max

Single-Pass:

min_max(xs):
  min = max = xs[0]
  for x in xs[1..]:
    if x < min: min = x
    if x > max: max = x
  return (min, max)

Multi-Pass:

min_max(xs):
  return (minimum(xs), maximum(xs))

Optimization Refinements

Quadratic to Linear

Pattern: Eliminate nested loops or redundant computation.

Example: Two Sum Problem

Quadratic:

two_sum(arr, target):
  for i in 0..n-1:
    for j in i+1..n-1:
      if arr[i] + arr[j] = target:
        return (i, j)

Linear (with hash map):

two_sum(arr, target):
  seen = {}
  for i in 0..n-1:
    complement = target - arr[i]
    if complement in seen:
      return (seen[complement], i)
    seen[arr[i]] = i

Exponential to Polynomial

Pattern: Memoization or dynamic programming.

Example: Longest Common Subsequence

Exponential:

lcs(s1, s2) =
  if s1 = [] or s2 = []: return 0
  if head(s1) = head(s2):
    return 1 + lcs(tail(s1), tail(s2))
  else:
    return max(lcs(tail(s1), s2), lcs(s1, tail(s2)))

Polynomial (DP):

lcs_dp(s1, s2):
  dp[i][j] = length of LCS of s1[0..i] and s2[0..j]
  for i in 0..len(s1):
    for j in 0..len(s2):
      if s1[i] = s2[j]:
        dp[i+1][j+1] = dp[i][j] + 1
      else:
        dp[i+1][j+1] = max(dp[i][j+1], dp[i+1][j])
  return dp[len(s1)][len(s2)]

Concurrency Refinements

Sequential to Parallel

Pattern: Identify independent computations.

Example: Map Operation

Sequential:

map(f, xs) = [f(x) for x in xs]

Parallel:

parallel_map(f, xs):
  results = array[len(xs)]
  parallel for i in 0..len(xs)-1:
    results[i] = f(xs[i])
  return results

Proof obligation: f must be pure (no side effects).

Blocking to Non-Blocking

Pattern: Refine synchronous to asynchronous operations.

Example: I/O Operations

Blocking:

process_files(files):
  results = []
  for file in files:
    content = read_file(file)  // Blocks
    results.append(process(content))
  return results

Non-Blocking:

async process_files(files):
  tasks = [read_file_async(f) for f in files]
  contents = await gather(tasks)
  return [process(c) for c in contents]

Refinement Composition

Sequential Composition

Pattern: Chain multiple refinement steps.

Abstract Spec
    ↓ [Refinement 1]
Intermediate 1
    ↓ [Refinement 2]
Intermediate 2
    ↓ [Refinement 3]
Concrete Implementation

Proof: Transitivity of refinement relation.

Parallel Composition

Pattern: Refine components independently.

Component A (Abstract) ⊗ Component B (Abstract)
         ↓                        ↓
Component A (Concrete) ⊗ Component B (Concrete)

Proof: Show each component refinement preserves composition.

Refinement Anti-Patterns

Over-Refinement

Problem: Too many small refinement steps.

Solution: Combine related refinements into larger steps.

Under-Specification

Problem: Abstract specification too vague.

Solution: Add precise preconditions and postconditions.

Broken Abstraction

Problem: Concrete implementation exposes details.

Solution: Maintain clear abstraction boundary.

Missing Invariants

Problem: Refinement doesn't preserve key properties.

Solution: Explicitly state and prove invariants.

Refinement Strategies

Top-Down Refinement

1. Start with high-level specification
2. Identify major components
3. Refine each component
4. Compose refined components
5. Prove composition correct

Bottom-Up Refinement

1. Implement concrete operations
2. Define abstraction relation
3. Prove operations refine abstract spec
4. Build larger components
5. Compose and verify

Middle-Out Refinement

1. Start with intermediate abstraction
2. Refine downward to implementation
3. Abstract upward to specification
4. Prove both directions

Verification Patterns

Simulation Proofs

Forward Simulation:

concrete_step(c) = c'
abs(c) = a
⟹ ∃a'. abstract_step(a) = a' ∧ abs(c') = a'

Backward Simulation:

abstract_step(a) = a'
abs(c) = a
⟹ ∃c'. concrete_step(c) = c' ∧ abs(c') = a'

Invariant Preservation

Pattern: Show refinement preserves invariants.

Invariant(abstract_state)
Refinement: concrete_state ⊑ abstract_state
⟹ Invariant(concrete_state)

Equivalence Proofs

Pattern: Show concrete and abstract are equivalent.

∀input. abstract_output(input) = concrete_output(input)