Refinement Step Generator

Refinement Step Generator

Generate systematic refinement steps that transform high-level specifications into concrete, executable implementations while preserving correctness through formal proofs.

Overview

Refinement is the process of transforming abstract specifications into concrete implementations through a series of correctness-preserving steps. Each refinement step:

1. Makes the specification more concrete (closer to executable code)
2. Preserves correctness through formal proof obligations
3. Maintains a clear abstraction relation between levels
4. Can be verified independently

This skill provides guidance for generating refinement steps in Isabelle/HOL and Coq.

Refinement Workflow

Abstract Specification
    ↓ [Data Refinement]
Refined Data Structures
    ↓ [Algorithmic Refinement]
Concrete Algorithm
    ↓ [Implementation Refinement]
Executable Code

Each arrow represents a refinement step with proof obligations.

Core Refinement Types

1. Data Refinement

Transform abstract data types into concrete data structures.

Example: Set → List

Abstract (Isabelle):

definition insert_set :: "'a ⇒ 'a set ⇒ 'a set" where
  "insert_set x S = S ∪ {x}"

definition member_set :: "'a ⇒ 'a set ⇒ bool" where
  "member_set x S = (x ∈ S)"

Concrete (Isabelle):

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

definition member_list :: "'a ⇒ 'a list ⇒ bool" where
  "member_list x xs = (x ∈ set xs)"

Abstraction Relation:

definition abs_list :: "'a list ⇒ 'a set" where
  "abs_list xs = set xs"

Proof Obligations:

lemma insert_refines:
  "abs_list (insert_list x xs) = insert_set x (abs_list xs)"
  by (simp add: insert_list_def insert_set_def abs_list_def)

lemma member_refines:
  "member_list x xs = member_set x (abs_list xs)"
  by (simp add: member_list_def member_set_def abs_list_def)

2. Algorithmic Refinement

Transform specifications into algorithms.

Example: Sorting Specification → Insertion Sort

Abstract (Coq):

Definition is_sorted (l : list nat) : Prop :=
  forall i j, i < j < length l → nth i l 0 ≤ nth j l 0.

Definition sort_spec (input output : list nat) : Prop :=
  is_sorted output ∧ Permutation input output.

Concrete (Coq):

Fixpoint insert (x : nat) (l : list nat) : list nat :=
  match l with
  | [] => [x]
  | h :: t => if x <=? h then x :: l else h :: insert x t
  end.

Fixpoint insertion_sort (l : list nat) : list nat :=
  match l with
  | [] => []
  | h :: t => insert h (insertion_sort t)
  end.

Proof Obligations:

Theorem insertion_sort_correct : forall l,
  sort_spec l (insertion_sort l).
Proof.
  (* Prove is_sorted and Permutation properties *)
Qed.

3. Implementation Refinement

Transform algorithms into efficient implementations.

Example: Naive → Optimized

Abstract:

definition naive_reverse :: "'a list ⇒ 'a list" where
  "naive_reverse xs = rev xs"

Concrete (tail-recursive):

fun reverse_acc :: "'a list ⇒ 'a list ⇒ 'a list" where
  "reverse_acc [] acc = acc" |
  "reverse_acc (x # xs) acc = reverse_acc xs (x # acc)"

definition efficient_reverse :: "'a list ⇒ 'a list" where
  "efficient_reverse xs = reverse_acc xs []"

Proof Obligation:

lemma efficient_reverse_correct:
  "efficient_reverse xs = naive_reverse xs"
  by (simp add: efficient_reverse_def naive_reverse_def reverse_acc_correct)

Refinement Process

Step 1: Identify Abstraction Gap

Analyze the specification and identify what needs refinement:

• Data structures: Abstract types (sets, maps) → Concrete structures (lists, trees)
• Operations: Non-deterministic specs → Deterministic algorithms
• Complexity: Inefficient → Efficient implementations

Step 2: Choose Refinement Strategy

Select appropriate refinement approach:

Data Refinement:

• Define concrete data type
• Define abstraction function
• Prove operations preserve abstraction

Algorithmic Refinement:

• Provide concrete algorithm
• Prove algorithm satisfies specification
• Maintain invariants

Compositional Refinement:

• Refine components independently
• Compose refinements
• Prove composition preserves correctness

Step 3: Define Abstraction Relation

Establish connection between abstract and concrete levels:

Isabelle:

definition abs_rel :: "'concrete ⇒ 'abstract ⇒ bool" where
  "abs_rel c a = (abs_fun c = a)"

Coq:

Definition abs_rel (c : concrete) (a : abstract) : Prop :=
  abs_fun c = a.

Step 4: Generate Proof Obligations

For each operation, prove refinement correctness:

Forward Simulation:

If: abs_rel c a
    op_concrete c = c'
Then: ∃a'. op_abstract a = a' ∧ abs_rel c' a'

Backward Simulation:

If: abs_rel c a
    op_abstract a = a'
Then: ∃c'. op_concrete c = c' ∧ abs_rel c' a'

Step 5: Prove Obligations

Use proof tactics to discharge obligations:

Isabelle:

• auto, simp, blast for automation
• induction for recursive structures
• case_tac for case analysis

Coq:

• auto, simpl, reflexivity for automation
• induction for recursive proofs
• destruct for case analysis

Framework-Specific Guidance

Isabelle/HOL Refinement

For Isabelle-specific patterns and the Autoref framework, see references/isabelle_refinement.md.

Key features:

• Refinement framework with ⊑ relation
• Autoref for automatic refinement
• Sepref for imperative refinement
• Code generation support

Coq Refinement

For Coq-specific patterns and refinement tactics, see references/coq_refinement.md.

Key features:

• Program for refinement with obligations
• Equations for well-founded recursion
• Refinement types
• Extraction to OCaml/Haskell

Common Refinement Patterns

For detailed refinement patterns (data structures, algorithms, optimizations), see references/refinement_patterns.md.

Common patterns include:

• Set → List/Tree refinement
• Map → Association list/Hash table
• Non-deterministic choice → Deterministic selection
• Specification → Divide-and-conquer algorithm
• Naive → Tail-recursive implementation

Example: Complete Refinement

Abstract Specification (Isabelle):

definition find_spec :: "'a list ⇒ ('a ⇒ bool) ⇒ 'a option" where
  "find_spec xs P = (if ∃x ∈ set xs. P x
                     then Some (SOME x. x ∈ set xs ∧ P x)
                     else None)"

Refinement Step 1: Deterministic Algorithm

fun find_impl :: "'a list ⇒ ('a ⇒ bool) ⇒ 'a option" where
  "find_impl [] P = None" |
  "find_impl (x # xs) P = (if P x then Some x else find_impl xs P)"

Proof Obligation:

lemma find_impl_refines:
  "find_impl xs P = find_spec xs P"
proof (induction xs)
  case Nil
  then show ?case by (simp add: find_spec_def)
next
  case (Cons x xs)
  then show ?case
    by (auto simp add: find_spec_def split: if_splits)
qed

Refinement Step 2: Tail-Recursive Implementation

fun find_tail :: "'a list ⇒ ('a ⇒ bool) ⇒ 'a option" where
  "find_tail [] P = None" |
  "find_tail (x # xs) P = (if P x then Some x else find_tail xs P)"

lemma find_tail_correct:
  "find_tail xs P = find_impl xs P"
  by (induction xs) auto

Best Practices

1. Small Steps: Make incremental refinements rather than large jumps
2. Clear Abstractions: Define explicit abstraction relations
3. Modular Proofs: Prove refinement for each operation separately
4. Reuse Lemmas: Build library of refinement lemmas
5. Automation: Use tactics and automation where possible
6. Documentation: Document refinement decisions and invariants

Verification Checklist

Before finalizing refinement:

• Abstraction relation is well-defined
• All operations have refinement proofs
• Invariants are preserved
• Termination is proven (if applicable)
• Concrete implementation is executable
• Code can be extracted/generated
• Performance characteristics are acceptable

Additional Resources

For detailed guidance on specific aspects:

• Isabelle Refinement - Isabelle/HOL refinement framework
• Coq Refinement - Coq refinement techniques
• Refinement Patterns - Common refinement patterns