Collections Framework. This development provides an efficient, extensible, machine checked collections framework. The library adopts the concepts of interface, implementation and generic algorithm from object-oriented programming and implements them in Isabelle/HOL. The framework features the use of data refinement techniques to refine an abstract specification (using high-level concepts like sets) to a more concrete implementation (using collection datastructures, like red-black-trees). The code-generator of Isabelle/HOL can be used to generate efficient code.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Lammich, Peter: Refinement to imperative HOL (2019)
- Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
- Lammich, Peter: Verified efficient implementation of Gabow’s strongly connected component algorithm (2014)
- Lammich, Peter; Tuerk, Thomas: Applying data refinement for monadic programs to Hopcroft’s algorithm (2012)