Abstract
In this entry, we verify the correctness of: Depth-first search and Breadth-first search
The entry's main aim is pedagogical.
It has the formal material presented in one chapter of the book Functional Data Structures and Algorithms:
A Proof Assistant Approach.
The verification is based on a simple set-based representation of directed graphs. The main feature
is that a graph's set of vertices is implicitly represented by its edges. The main focus of the
development is to develop a representation suitable for mathematical reasoning and for executable
algorithms.
The entry also shows the verification of executable algorithms that need background mathematical
libraries with basic Isabelle tools.
Two main features are its automation setup aimed at verifying executable graph algorithms in
a human-readable way and to verify the algorithms w.r.t.\ the same graph representation, making all
of them compatible.
The setup we use here includes using the function package to model loops and reason about their
termination, using records to model program states, and using locales to implement parametric
as well as step-wise refinement based verification.
The material presented here is a part of an ongoing development of formal results on graphs and graph
algorithms in Isabelle/HOL: https://github.com/mabdula/Isabelle-Graph-Library.
License
Topics
Session Graph_Algorithms
- More_Lists
- Pair_Graph
- Vwalk
- Enat_Misc
- Dist
- Set_Addons
- Map_Addons
- Set2_Addons
- Pair_Graph_Specs
- DFS
- BFS_2