The Autoref Tool
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.
Autoref for Isabelle-2013
(See file README for further instructions)
The proof outline and the proof document
witness a successful verification with Isabelle/HOL, and contain the
theories in human-readable format.
Isabelle/HOL also supports browsing the theories
The Autoref-Tool is described in the ITP-2013 paper Automatic Data Refinement
The components described in the paper can be found as follows:
A standard collection of relators is implemented in
A basic parametricity prover, that does not do synthesis however,
is implemented in the folder /Parametricity, it's main theory being
It is a leightweight
alternative to using the Autoref-tool for some parametricity proofs.
Ultimately, it will be integrated with the Autoref-tool.
The Autoref-Tool is contained in the folder /Autoref, its main theory being
The operator-identification phase is in
The sub-phases for selection of the implementation types are located in
The synthesis phase and side-condition solving is in
Some setup to support generic programming is in
The Refinement Framework that contains setup for Autoref is in the
folder /Monadic. Its entry point is
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:
The generic map and set algorithm library is in /Collections/Gen:
The case studies are in /Examples. The entry points are the following:
- 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
- The nested depth-first search algorithm. The Autoref-part
is at the end of this file.
- A simplistic depth-first search algorithm,
used to demonstrate some features of Autoref.
- Collection of small test-cases for Autoref.