(* Title: HOL/Imperative_HOL/Overview.thy
Author: Florian Haftmann, TU Muenchen
*)
(*<*)
theory Overview
imports Imperative_HOL LaTeXsugar
begin
(* type constraints with spacing *)
setup {*
let
val typ = Simple_Syntax.read_typ;
val typeT = Syntax.typeT;
val spropT = Syntax.spropT;
in
Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
*}(*>*)
text {*
@{text "Imperative HOL"} is a leightweight framework for reasoning
about imperative data structures in @{text "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 constructions. 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}.
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 @{text execute_simps} contains appropriate rewrites
for all fundamental operations.
Primitive fine-granular control over heaps is avialable through rule
@{text 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 crel}
\end{quote}
provides a simple relational calculus. Primitive rules are @{text
crelI} and @{text crelE}, rules appropriate for reasoning about
imperative operation are available in the @{text crel_intros} and
@{text crel_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
@{text success_intro} fact collection.
@{const execute}, @{const crel}, @{const success} and @{const bind}
are related by rules @{text execute_bind_success}, @{text
success_bind_executeI}, @{text success_bind_crelI}, @{text
crel_bindI}, @{text crel_bindE} and @{text 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.
*}
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 @{text Haskell}, a suitable @{text ST} monad is used;
for @{text SML}, @{text Ocaml} and @{text 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 @{text SML_imp}, @{text Ocaml_imp} and
@{text 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 @{text execute_simps} or relational reasoning (fact
collections @{text crel_intros} and @{text crel_elims}) dependes
on the problems. 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.
\end{itemize}
*}
end