Refinement for Monadic Programs

Title:	Refinement for Monadic Programs
Author:	Peter Lammich
Submission date:	2012-01-30
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.
Change history:	[2012-04-23] Introduced ordered FOREACH loops [2012-06] New features: REC_rule_arb and RECT_rule_arb allow for generalizing over variables. prepare_code_thms - command extracts code equations for recursion combinators. [2012-07] New example: Nested DFS for emptiness check of Buchi-automata with witness. New feature: fo_rule method to apply resolution using first-order matching. Useful for arg_conf, fun_cong. [2012-08] Adaptation to ICF v2. [2012-10-05] Adaptations to include support for Automatic Refinement Framework. [2013-09] This entry now depends on Automatic Refinement [2014-06] New feature: vc_solve method to solve verification conditions. Maintenace changes: VCG-rules for nfoldli, improved setup for FOREACH-loops. [2014-07] Now defining recursion via flat domain. Dropped many single-valued prerequisites. Changed notion of data refinement. In single-valued case, this matches the old notion. In non-single valued case, the new notion allows for more convenient rules. In particular, the new definitions allow for projecting away ghost variables as a refinement step. [2014-11] New features: le-or-fail relation (leof), modular reasoning about loop invariants.
BibTeX:	@article{Refine_Monadic-AFP, author = {Peter Lammich}, title = {Refinement for Monadic Programs}, journal = {Archive of Formal Proofs}, month = jan, year = 2012, note = {\url{http://isa-afp.org/entries/Refine_Monadic.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Automatic_Refinement
Used by:	Collections, JinjaThreads, Kruskal
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry