### Abstract

We provide a framework for program and data refinement in Isabelle/HOL. The framework is based on a nondeterminism-monad with assertions, i.e., the monad carries a set of results or an assertion failure. Recursion is expressed by fixed points. For convenience, we also provide while and foreach combinators.

The framework provides tools to automatize canonical tasks, such as verification condition generation, finding appropriate data refinement relations, and refine an executable program to a form that is accepted by the Isabelle/HOL code generator.

This submission comes with a collection of examples and a user-guide, illustrating the usage of the framework.

### License

BSD License

### Topics

- Computer science/Semantics and reasoning

### Session Refine_Monadic

- Refine_Chapter
- Refine_Mono_Prover
- Refine_Misc
- RefineG_Transfer
- RefineG_Domain
- RefineG_Recursion
- RefineG_Assert
- Refine_Basic
- Refine_Leof
- Refine_Heuristics
- Refine_More_Comb
- RefineG_While
- Refine_While
- Refine_Det
- Refine_Pfun
- Refine_Transfer
- Refine_Foreach
- Refine_Automation
- Autoref_Monadic
- Refine_Monadic
- Example_Chapter
- Breadth_First_Search
- WordRefine
- Examples

### Depends on

- Automatic Data Refinement

### Used by

- Kruskal’s Algorithm for Minimum Spanning Forest
- Collections Framework
- Jinja with Threads

### Auto-related entries

- Verification Components for Hybrid Systems
- Complete Non-Orders and Fixed Points
- A Separation Logic Framework for Imperative HOL
- Semantics and Data Refinement of Invariant Based Programs

## Cite

×

Refine_Monadic-AFP

    @article{Refine_Monadic-AFP,
      author  = {Peter Lammich},
      title   = {Refinement for Monadic Programs},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Refine_Monadic.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
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Feb 10, 2012 : Isabelle2011-1