Refinement based Algorithm Development

with Isabelle/HOL

Abstract

Isabelle/HOL is an interactive theorem prover for higher-order logic, that is, a tool that assists the user in conducting mathematically rigorous proofs that are verified by the computer. Isabelle/HOL comes with a large library of formalized mathematics and computer science, which can readily be used for new formalizations. One interesting application of theorem provers is to verify algorithms and their implementations. Stepwise refinement allows to structure such a proof along natural concepts known to most programmers: First, the mathematical idea of the algorithm is verified using adequate mathematical concepts like sets and functions. This results in a pseudo-code like algorithm as one may find in algorithm textbooks. Then, the mathematical concepts are implemented using appropriate data structures (e.g. Hash-table) and sub-algorithms (e.g. quicksort), which can be verified independently. Also, implementation specific optimizations can be added. The Isabelle Refinement Framework supports stepwise refinement in Isabelle/HOL. It comes with a large library of verified data structures and algorithms, and supports both functional and imperative features, as well as the generation of actual source code in various target languages (Haskell, Scala, OCaML, SML). In this lecture, we present stepwise refinement using network flow algorithms as running example. We will use the Isabelle Refinement Framework, but the presented formal tools and techniques are generally applicable, and prior knowledge of Isabelle is not required.

Material

Slides

Demo Theories referred to on slides (Tested with Isabelle-2018)

Installing Isabelle and the Archive of Formal Proofs

In order to view or experiment with the demo theories, you will need to install Isabelle/HOL and the Archive of Formal Proofs:

QUICK INSTALLATION INSTRUCTIONS

  1. Download and Install Isabelle 2018 as described on the Isabelle Homepage
  2. Start up the Isabelle/jEdit Prover IDE, and wait until it has compiled its base theories (This takes some time, but only happens on first startup)
  3. Quit Isabelle again
  4. Install the Archive of Formal Proofs as described on its installation page It is important that Isabelle has been started at least once before this step because the ~/.isabelle directory must have been created!
  5. Start up Isabelle with command line arguments
    Linux/Mac: isabelle jedit -l EdmondsKarp_Maxflow
    wait until Isabelle compiles these theories (takes long, but only happens once