### Abstract

We present the Imperative Refinement Framework (IRF), a tool that supports a stepwise refinement based approach to imperative programs. This entry is based on the material we presented in [ITP-2015, CPP-2016]. It uses the Monadic Refinement Framework as a frontend for the specification of the abstract programs, and Imperative/HOL as a backend to generate executable imperative programs. The IRF comes with tool support to synthesize imperative programs from more abstract, functional ones, using efficient imperative implementations for the abstract data structures. This entry also includes the Imperative Isabelle Collection Framework (IICF), which provides a library of re-usable imperative collection data structures. Moreover, this entry contains a quickstart guide and a reference manual, which provide an introduction to using the IRF for Isabelle/HOL experts. It also provids a collection of (partly commented) practical examples, some highlights being Dijkstra's Algorithm, Nested-DFS, and a generic worklist algorithm with subsumption. Finally, this entry contains benchmark scripts that compare the runtime of some examples against reference implementations of the algorithms in Java and C++. [ITP-2015] Peter Lammich: Refinement to Imperative/HOL. ITP 2015: 253--269 [CPP-2016] Peter Lammich: Refinement based verification of imperative data structures. CPP 2016: 27--36

### License

BSD License

### Topics

- Computer science/Semantics and reasoning
- Computer science/Data structures

### Session Sepref_Prereq

### Session Refine_Imperative_HOL

- Concl_Pres_Clarification
- Named_Theorems_Rev
- Pf_Add
- Pf_Mono_Prover
- PO_Normalizer
- Sepref_Misc
- Structured_Apply
- Term_Synth
- User_Smashing
- Sepref_Chapter_Tool
- Sepref_Id_Op
- Sepref_Basic
- Sepref_Monadify
- Sepref_Constraints
- Sepref_Frame
- Sepref_Rules
- Sepref_Combinator_Setup
- Sepref_Translate
- Sepref_Definition
- Sepref_Intf_Util
- Sepref_Tool
- Sepref_Chapter_Setup
- Sepref_HOL_Bindings
- Sepref_Foreach
- Sepref_Improper
- Sepref
- Sepref_Chapter_IICF
- IICF_Set
- IICF_List_SetO
- IICF_Multiset
- IICF_Prio_Bag
- IICF_List_Mset
- IICF_List_MsetO
- IICF_List
- IICF_Abs_Heap
- IICF_HOL_List
- IICF_Array_List
- IICF_Impl_Heap
- IICF_Map
- IICF_Prio_Map
- IICF_Abs_Heapmap
- IICF_Array
- IICF_MS_Array_List
- IICF_Indexed_Array_List
- IICF_Impl_Heapmap
- IICF_Matrix
- IICF_Array_Matrix
- IICF_Sepl_Binding
- IICF
- Sepref_Chapter_Userguides
- Sepref_Guide_Quickstart
- Sepref_Guide_Reference
- Sepref_Guide_General_Util
- Sepref_ICF_Bindings
- Sepref_WGraph
- Sepref_Chapter_Examples
- Sepref_Graph
- Sepref_DFS
- Sepref_Dijkstra
- Sepref_NDFS
- Sepref_Minitests
- Worklist_Subsumption
- Worklist_Subsumption_Impl
- Sepref_Snip_Datatype
- Sepref_Snip_Combinator
- Sepref_All_Examples
- Sepref_Chapter_Benchmarks
- Heapmap_Bench
- Dijkstra_Benchmark
- NDFS_Benchmark

### Session Sepref_Basic

### Session Sepref_IICF

### Depends on

- Collections Framework
- A Separation Logic Framework for Imperative HOL
- A Framework for Verifying Depth-First Search Algorithms
- Dijkstra’s Shortest Path Algorithm
- List Index

### Used by

- Simplicial Complexes and Boolean functions
- A Verified Imperative Implementation of B-Trees
- Practical Algebraic Calculus Checker
- VerifyThis 2019 – Polished Isabelle Solutions
- Kruskal’s Algorithm for Minimum Spanning Forest
- VerifyThis 2018 - Polished Isabelle Solutions
- The string search algorithm by Knuth, Morris and Pratt
- Flow Networks and the Min-Cut-Max-Flow Theorem
- The Floyd-Warshall Algorithm for Shortest Paths
- Algorithms for Reduced Ordered Binary Decision Diagrams

## Cite

×

Refine_Imperative_HOL-AFP

    @article{Refine_Imperative_HOL-AFP,
      author  = {Peter Lammich},
      title   = {The Imperative Refinement Framework},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Refine_Imperative_HOL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Aug 8, 2016 : Isabelle2016