Refinement for Monadic Programs

Peter Lammich 🌐

January 30, 2012

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We provide a framework for program and data refinement in Isabelle/HOL. The framework is based on a nondeterminism-monad with assertions, i.e., the monad carries a set of results or an assertion failure. Recursion is expressed by fixed points. For convenience, we also provide while and foreach combinators.

The framework provides tools to automatize canonical tasks, such as verification condition generation, finding appropriate data refinement relations, and refine an executable program to a form that is accepted by the Isabelle/HOL code generator.

This submission comes with a collection of examples and a user-guide, illustrating the usage of the framework.

License

BSD License

Topics

Session Refine_Monadic