### Abstract

We present the Autoref tool for Isabelle/HOL, which automatically refines algorithms specified over abstract concepts like maps and sets to algorithms over concrete implementations like red-black-trees, and produces a refinement theorem. It is based on ideas borrowed from relational parametricity due to Reynolds and Wadler. The tool allows for rapid prototyping of verified, executable algorithms. Moreover, it can be configured to fine-tune the result to the user~s needs. Our tool is able to automatically instantiate generic algorithms, which greatly simplifies the implementation of executable data structures.

This AFP-entry provides the basic tool, which is then used by the Refinement and Collection Framework to provide automatic data refinement for the nondeterminism monad and various collection datastructures.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Session Automatic_Refinement

- Refine_Util_Bootstrap1
- Mpat_Antiquot
- Mk_Term_Antiquot
- Refine_Util
- Attr_Comb
- Named_Sorted_Thms
- Prio_List
- Tagged_Solver
- Anti_Unification
- Misc
- Foldi
- Indep_Vars
- Select_Solve
- Mk_Record_Simp
- Refine_Lib
- Param_Chapter
- Relators
- Param_Tool
- Param_HOL
- Parametricity
- Autoref_Phases
- Autoref_Data
- Autoref_Tagging
- Autoref_Id_Ops
- Autoref_Fix_Rel
- Autoref_Relator_Interface
- Autoref_Translate
- Autoref_Gen_Algo
- Autoref_Chapter
- Autoref_Tool
- Autoref_Bindings_HOL
- Automatic_Refinement

### Used by

- van Emde Boas Trees
- Dictionary Construction
- IP Addresses
- Algorithms for Reduced Ordered Binary Decision Diagrams
- Verification of the UpDown Scheme
- Network Security Policy Verification
- Light-weight Containers
- A Separation Logic Framework for Imperative HOL
- Refinement for Monadic Programs
- Jinja with Threads

## Cite

×

Automatic_Refinement-AFP

    @article{Automatic_Refinement-AFP,
      author  = {Peter Lammich},
      title   = {Automatic Data Refinement},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Automatic_Refinement.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 18, 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