Refinement Monadic (Q40265)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Refine_Monadic
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Refinement Monadic |
AFP entry Refine_Monadic |
Statements
Peter Lammich
0 references
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.
0 references
0 references
30 January 2012
0 references
Refinement for Monadic Programs (English)
0 references
