The Autoref Tool

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.

Thanks to its integration with the Isabelle Refinement Framework and the Isabelle Collection Framework, Autoref can be used as a backend to a stepwise refinement based development approach, having access to a rich library of verified data structures. We have evaluated the tool by synthesizing efficiently executable refinements for some complex algorithms, as well as by implementing a library of generic algorithms for maps and sets.

Download

Autoref for Isabelle-2013 (See file README for further instructions)

Proof Documents

The proof outline and the proof document witness a successful verification with Isabelle/HOL, and contain the theories in human-readable format.

Theory Browsing

Isabelle/HOL also supports browsing the theories in html-format.

ITP-2013 Paper

The Autoref-Tool is described in the ITP-2013 paper Automatic Data Refinement The components described in the paper can be found as follows:

Basic Idea

A standard collection of relators is implemented in Relators.thy

A basic parametricity prover, that does not do synthesis however, is implemented in the folder /Parametricity, it's main theory being Parametricity.thy. It is a leightweight alternative to using the Autoref-tool for some parametricity proofs. Ultimately, it will be integrated with the Autoref-tool.

Tool Implementation

The Autoref-Tool is contained in the folder /Autoref, its main theory being Autoref.thy

The operator-identification phase is in Autoref_Id_Ops_Alt.thy.

The sub-phases for selection of the implementation types are located in Autoref_Fix_Rel.thy

The synthesis phase and side-condition solving is in Autoref_Translate.thy. Some setup to support generic programming is in Autoref_Gen_Algo.thy

Case Studies

The Refinement Framework that contains setup for Autoref is in the folder /Monadic. Its entry point is Refine.thy

The Isabelle Collection Framework with setup for Autoref is in the folder /Collections/ICF. Parts of the setup are in /Collections/Intf. Its entry-point is Collections.thy

The unrestricted red-black tree and list implementations are in the folder /Collections/Impl: Impl_RBT_Map.thy and Impl_List_Set.thy

The generic map and set algorithm library is in /Collections/Gen: Gen_Map.thy and Gen_Set.thy and Gen_Map2Set.thy.

The case studies are in /Examples. The entry points are the following:

INY/NFA_Simulations_INY.thy
The algorithm of Ilie, Navarro and Yu for computing simulation preorders in NFAs. The Autoref-part is near the end of the file, in subsection Refinement and Code Generation. At the end of this file, we have commented out the original 500 lines required for code-generation.
Nested_DFS.thy
The nested depth-first search algorithm. The Autoref-part is at the end of this file.
Simple_DFS.thy
A simplistic depth-first search algorithm, used to demonstrate some features of Autoref.
Coll_Test.thy
Collection of small test-cases for Autoref.