(* Title: HOL/Imperative_HOL/Overview.thy Author: Florian Haftmann, TU Muenchen *) (*<*) theory Overview imports Imperative_HOL "HOL-Library.LaTeXsugar" begin (* type constraints with spacing *) no_syntax (output) "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3) "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3) syntax (output) "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3) (*>*) text ‹ ‹Imperative HOL› is a leightweight framework for reasoning about imperative data structures in ‹Isabelle/HOL› @{cite "Nipkow-et-al:2002:tutorial"}. Its basic ideas are described in @{cite "Bulwahn-et-al:2008:imp_HOL"}. However their concrete realisation has changed since, due to both extensions and refinements. Therefore this overview wants to present the framework \qt{as it is} by now. It focusses on the user-view, less on matters of construction. For details study of the theory sources is encouraged. › section ‹A polymorphic heap inside a monad› text ‹ Heaps (@{type heap}) can be populated by values of class @{class heap}; HOL's default types are already instantiated to class @{class heap}. Class @{class heap} is a subclass of @{class countable}; see theory ‹Countable› for ways to instantiate types as @{class countable}. The heap is wrapped up in a monad @{typ "'a Heap"} by means of the following specification: \begin{quote} @{datatype Heap} \end{quote} Unwrapping of this monad type happens through \begin{quote} @{term_type execute} \\ @{thm execute.simps [no_vars]} \end{quote} This allows for equational reasoning about monadic expressions; the fact collection ‹execute_simps› contains appropriate rewrites for all fundamental operations. Primitive fine-granular control over heaps is available through rule ‹Heap_cases›: \begin{quote} @{thm [break] Heap_cases [no_vars]} \end{quote} Monadic expression involve the usual combinators: \begin{quote} @{term_type return} \\ @{term_type bind} \\ @{term_type raise} \end{quote} This is also associated with nice monad do-syntax. The @{typ string} argument to @{const raise} is just a codified comment. Among a couple of generic combinators the following is helpful for establishing invariants: \begin{quote} @{term_type assert} \\ @{thm assert_def [no_vars]} \end{quote} › section ‹Relational reasoning about @{type Heap} expressions› text ‹ To establish correctness of imperative programs, predicate \begin{quote} @{term_type effect} \end{quote} provides a simple relational calculus. Primitive rules are ‹effectI› and ‹effectE›, rules appropriate for reasoning about imperative operations are available in the ‹effect_intros› and ‹effect_elims› fact collections. Often non-failure of imperative computations does not depend on the heap at all; reasoning then can be easier using predicate \begin{quote} @{term_type success} \end{quote} Introduction rules for @{const success} are available in the ‹success_intro› fact collection. @{const execute}, @{const effect}, @{const success} and @{const bind} are related by rules ‹execute_bind_success›, ‹success_bind_executeI›, ‹success_bind_effectI›, ‹effect_bindI›, ‹effect_bindE› and ‹execute_bind_eq_SomeI›. › section ‹Monadic data structures› text ‹ The operations for monadic data structures (arrays and references) come in two flavours: \begin{itemize} \item Operations on the bare heap; their number is kept minimal to facilitate proving. \item Operations on the heap wrapped up in a monad; these are designed for executing. \end{itemize} Provided proof rules are such that they reduce monad operations to operations on bare heaps. Note that HOL equality coincides with reference equality and may be used as primitive executable operation. › subsection ‹Arrays› text ‹ Heap operations: \begin{quote} @{term_type Array.alloc} \\ @{term_type Array.present} \\ @{term_type Array.get} \\ @{term_type Array.set} \\ @{term_type Array.length} \\ @{term_type Array.update} \\ @{term_type Array.noteq} \end{quote} Monad operations: \begin{quote} @{term_type Array.new} \\ @{term_type Array.of_list} \\ @{term_type Array.make} \\ @{term_type Array.len} \\ @{term_type Array.nth} \\ @{term_type Array.upd} \\ @{term_type Array.map_entry} \\ @{term_type Array.swap} \\ @{term_type Array.freeze} \end{quote} › subsection ‹References› text ‹ Heap operations: \begin{quote} @{term_type Ref.alloc} \\ @{term_type Ref.present} \\ @{term_type Ref.get} \\ @{term_type Ref.set} \\ @{term_type Ref.noteq} \end{quote} Monad operations: \begin{quote} @{term_type Ref.ref} \\ @{term_type Ref.lookup} \\ @{term_type Ref.update} \\ @{term_type Ref.change} \end{quote} › section ‹Code generation› text ‹ Imperative HOL sets up the code generator in a way that imperative operations are mapped to suitable counterparts in the target language. For ‹Haskell›, a suitable ‹ST› monad is used; for ‹SML›, ‹Ocaml› and ‹Scala› unit values ensure that the evaluation order is the same as you would expect from the original monadic expressions. These units may look cumbersome; the target language variants ‹SML_imp›, ‹Ocaml_imp› and ‹Scala_imp› make some effort to optimize some of them away. › section ‹Some hints for using the framework› text ‹ Of course a framework itself does not by itself indicate how to make best use of it. Here some hints drawn from prior experiences with Imperative HOL: \begin{itemize} \item Proofs on bare heaps should be strictly separated from those for monadic expressions. The first capture the essence, while the latter just describe a certain wrapping-up. \item A good methodology is to gradually improve an imperative program from a functional one. In the extreme case this means that an original functional program is decomposed into suitable operations with exactly one corresponding imperative operation. Having shown suitable correspondence lemmas between those, the correctness prove of the whole imperative program simply consists of composing those. \item Whether one should prefer equational reasoning (fact collection ‹execute_simps› or relational reasoning (fact collections ‹effect_intros› and ‹effect_elims›) depends on the problems to solve. For complex expressions or expressions involving binders, the relation style usually is superior but requires more proof text. \item Note that you can extend the fact collections of Imperative HOL yourself whenever appropriate. \end{itemize} › end