(* Title: HOL/Hoare/Separation.thy
Author: Tobias Nipkow
Copyright 2003 TUM
A first attempt at a nice syntactic embedding of separation logic.
Already builds on the theory for list abstractions.
If we suppress the H parameter for "List", we have to hardwired this
into parser and pretty printer, which is not very modular.
Alternative: some syntax like <P> which stands for P H. No more
compact, but avoids the funny H.
*)
section ‹Separation logic
›
theory Separation
imports Hoare_Logic_Abort SepLogHeap
begin
text‹The semantic
definition of a few connectives:
›
definition ortho ::
"heap \ heap \ bool" (
infix ‹⊥› 55)
where "h1 \ h2 \ dom h1 \ dom h2 = {}"
definition is_empty ::
"heap \ bool"
where "is_empty h \ h = Map.empty"
definition singl::
"heap \ nat \ nat \ bool"
where "singl h x y \ dom h = {x} & h x = Some y"
definition star::
"(heap \ bool) \ (heap \ bool) \ (heap \ bool)"
where "star P Q = (\h. \h1 h2. h = h1++h2 \ h1 \ h2 \ P h1 \ Q h2)"
definition wand::
"(heap \ bool) \ (heap \ bool) \ (heap \ bool)"
where "wand P Q = (\h. \h'. h' \ h \ P h' \ Q(h++h'))"
text‹This
is what assertions look like without any syntactic sugar:
›
lemma "VARS x y z w h
{star (%h. singl h x y) (%h. singl h z w) h}
SKIP
{x
≠ z}
"
apply vcg
apply(auto simp:star_def ortho_def singl_def)
done
text‹Now we add nice input
syntax.
To suppress the heap parameter
of the connectives, we
assume it
is always called H
and add/remove it
upon parsing/printing.
Thus every pointer program needs
to have a
program variable H,
and assertions should not contain any locally
bound Hs -
otherwise they may bind the implicit H.
›
syntax
"_emp" ::
"bool" (
‹emp
›)
"_singl" ::
"nat \ nat \ bool" (
‹(
‹open_block
notation=
‹mixfix singl
››[_
↦ _])
›)
"_star" ::
"bool \ bool \ bool" (
infixl ‹**
› 60)
"_wand" ::
"bool \ bool \ bool" (
infixl ‹-*
› 60)
syntax_consts
"_emp" ⇌ is_empty
and
"_singl" ⇌ singl
and
"_star" ⇌ star
and
"_wand" ⇌ wand
(* FIXME does not handle "_idtdummy" *)
ML
‹
🍋 ‹‹free_tr
› takes care of free vars
in the scope of separation logic connectives:
they are implicitly applied
to the heap
›
fun free_tr(t as Free _) = t $
Syntax.free
"H"
🍋‹| free_tr((list as Free(
"List",_))$ p $ ps) = list $
Syntax.free
"H" $ p $ ps
›
| free_tr t = t
fun emp_tr [] =
Syntax.const
🍋‹is_empty
› $
Syntax.free
"H"
| emp_tr ts = raise
TERM (
"emp_tr", ts);
fun singl_tr [p, q] =
Syntax.const
🍋‹singl
› $
Syntax.free
"H" $ p $ q
| singl_tr ts = raise
TERM (
"singl_tr", ts);
fun star_tr [P,Q] =
Syntax.const
🍋‹star
› $
absfree (
"H", dummyT) (free_tr P) $ absfree (
"H", dummyT) (free_tr Q) $
Syntax.free
"H"
| star_tr ts = raise
TERM (
"star_tr", ts);
fun wand_tr [P, Q] =
Syntax.const
🍋‹wand
› $
absfree (
"H", dummyT) P $ absfree (
"H", dummyT) Q $
Syntax.free
"H"
| wand_tr ts = raise
TERM (
"wand_tr", ts);
›
parse_translation ‹
[(
🍋‹_emp
›, K emp_tr),
(
🍋‹_singl
›, K singl_tr),
(
🍋‹_star
›, K star_tr),
(
🍋‹_wand
›, K wand_tr)]
›
text‹Now it looks much better:
›
lemma "VARS H x y z w
{[x
↦y] ** [z
↦w]}
SKIP
{x
≠ z}
"
apply vcg
apply(auto simp:star_def ortho_def singl_def)
done
lemma "VARS H x y z w
{emp ** emp}
SKIP
{emp}
"
apply vcg
apply(auto simp:star_def ortho_def is_empty_def)
done
text‹But the
output is still unreadable.
Thus we
also strip the heap
parameters upon
output:
›
ML
‹
local
fun strip (Abs(_,_,(t as Const(
"_free",_) $ Free _) $ Bound 0)) = t
| strip (Abs(_,_,(t as Free _) $ Bound 0)) = t
🍋‹| strip (Abs(_,_,((list as Const(
"List",_))$ Bound 0 $ p $ ps))) = list$p$ps
›
| strip (Abs(_,_,(t as Const(
"_var",_) $ Var _) $ Bound 0)) = t
| strip (Abs(_,_,P)) = P
| strip (Const(
🍋‹is_empty
›,_)) =
Syntax.const
🍋‹_emp
›
| strip t = t;
in
fun is_empty_tr
' [_] = Syntax.const \<^syntax_const>\_emp\
fun singl_tr
' [_,p,q] = Syntax.const \<^syntax_const>\_singl\ $ p $ q
fun star_tr
' [P,Q,_] = Syntax.const \<^syntax_const>\_star\ $ strip P $ strip Q
fun wand_tr
' [P,Q,_] = Syntax.const \<^syntax_const>\_wand\ $ strip P $ strip Q
end
›
print_translation ‹
[(
🍋‹is_empty
›, K is_empty_tr
'),
(
🍋‹singl
›, K singl_tr
'),
(
🍋‹star
›, K star_tr
'),
(
🍋‹wand
›, K wand_tr
')]
›
text‹Now the intermediate
proof states are
also readable:
›
lemma "VARS H x y z w
{[x
↦y] ** [z
↦w]}
y := w
{x
≠ z}
"
apply vcg
apply(auto simp:star_def ortho_def singl_def)
done
lemma "VARS H x y z w
{emp ** emp}
SKIP
{emp}
"
apply vcg
apply(auto simp:star_def ortho_def is_empty_def)
done
text‹So far we
have unfolded the separation logic connectives
in
proofs. Here comes a simple example of a program
proof that
uses a law
of separation logic instead.
›
🍋 ‹a law of separation logic
›
lemma star_comm:
"P ** Q = Q ** P"
by(auto simp add:star_def ortho_def dest: map_add_comm)
lemma "VARS H x y z w
{P ** Q}
SKIP
{Q ** P}
"
apply vcg
apply(simp add: star_comm)
done
lemma "VARS H
{p
≠0
∧ [p
↦ x] ** List H q qs}
H := H(p
↦ q)
{List H p (p#qs)}
"
apply vcg
apply(simp add: star_def ortho_def singl_def)
apply clarify
apply(subgoal_tac
"p \ set qs")
prefer 2
apply(blast dest:list_in_heap)
apply simp
done
lemma "VARS H p q r
{List H p Ps ** List H q Qs}
WHILE p
≠ 0
INV {
∃ps qs. (List H p ps ** List H q qs)
∧ rev ps @ qs = rev Ps @ Qs}
DO r := p; p := the(H p); H := H(r
↦ q); q := r OD
{List H q (rev Ps @ Qs)}
"
apply vcg
apply(simp_all add: star_def ortho_def singl_def)
apply fastforce
apply (clarsimp simp add:List_non_null)
apply(rename_tac ps
')
apply(rule_tac x = ps
' in exI)
apply(rule_tac x =
"p#qs" in exI)
apply simp
apply(rule_tac x =
"h1(p:=None)" in exI)
apply(rule_tac x =
"h2(p\q)" in exI)
apply simp
apply(rule conjI)
apply(rule ext)
apply(simp add:map_add_def split:option.split)
apply(rule conjI)
apply blast
apply(simp add:map_add_def split:option.split)
apply(rule conjI)
apply(subgoal_tac
"p \ set qs")
prefer 2
apply(blast dest:list_in_heap)
apply(simp)
apply fast
apply(fastforce)
done
end
