Abstract
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.
Depends On
Used by
Topics
Theories
- Refine_Chapter
- Refine_Mono_Prover
- files/refine_mono_prover.ML
- Refine_Misc
- RefineG_Transfer
- RefineG_Domain
- RefineG_Recursion
- RefineG_Assert
- Refine_Basic
- Refine_Leof
- Refine_Heuristics
- Refine_More_Comb
- RefineG_While
- Refine_While
- Refine_Det
- Refine_Pfun
- Refine_Transfer
- Refine_Foreach
- Refine_Automation
- Autoref_Monadic
- Refine_Monadic
- Example_Chapter
- Breadth_First_Search
- WordRefine
- Examples