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