1(* Title: HOL/Hoare/Separation.thy 2 Author: Tobias Nipkow 3 Copyright 2003 TUM 4 5A first attempt at a nice syntactic embedding of separation logic. 6Already builds on the theory for list abstractions. 7 8If we suppress the H parameter for "List", we have to hardwired this 9into parser and pretty printer, which is not very modular. 10Alternative: some syntax like <P> which stands for P H. No more 11compact, but avoids the funny H. 12 13*) 14 15theory Separation imports Hoare_Logic_Abort SepLogHeap begin 16 17text\<open>The semantic definition of a few connectives:\<close> 18 19definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) 20 where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}" 21 22definition is_empty :: "heap \<Rightarrow> bool" 23 where "is_empty h \<longleftrightarrow> h = Map.empty" 24 25definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" 26 where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y" 27 28definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" 29 where "star P Q = (\<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2)" 30 31definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" 32 where "wand P Q = (\<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h'))" 33 34text\<open>This is what assertions look like without any syntactic sugar:\<close> 35 36lemma "VARS x y z w h 37 {star (%h. singl h x y) (%h. singl h z w) h} 38 SKIP 39 {x \<noteq> z}" 40apply vcg 41apply(auto simp:star_def ortho_def singl_def) 42done 43 44text\<open>Now we add nice input syntax. To suppress the heap parameter 45of the connectives, we assume it is always called H and add/remove it 46upon parsing/printing. Thus every pointer program needs to have a 47program variable H, and assertions should not contain any locally 48bound Hs - otherwise they may bind the implicit H.\<close> 49 50syntax 51 "_emp" :: "bool" ("emp") 52 "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]") 53 "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60) 54 "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60) 55 56(* FIXME does not handle "_idtdummy" *) 57ML \<open> 58\<comment> \<open>\<open>free_tr\<close> takes care of free vars in the scope of separation logic connectives: 59 they are implicitly applied to the heap\<close> 60fun free_tr(t as Free _) = t $ Syntax.free "H" 61\<^cancel>\<open>| free_tr((list as Free("List",_))$ p $ ps) = list $ Syntax.free "H" $ p $ ps\<close> 62 | free_tr t = t 63 64fun emp_tr [] = Syntax.const \<^const_syntax>\<open>is_empty\<close> $ Syntax.free "H" 65 | emp_tr ts = raise TERM ("emp_tr", ts); 66fun singl_tr [p, q] = Syntax.const \<^const_syntax>\<open>singl\<close> $ Syntax.free "H" $ p $ q 67 | singl_tr ts = raise TERM ("singl_tr", ts); 68fun star_tr [P,Q] = Syntax.const \<^const_syntax>\<open>star\<close> $ 69 absfree ("H", dummyT) (free_tr P) $ absfree ("H", dummyT) (free_tr Q) $ 70 Syntax.free "H" 71 | star_tr ts = raise TERM ("star_tr", ts); 72fun wand_tr [P, Q] = Syntax.const \<^const_syntax>\<open>wand\<close> $ 73 absfree ("H", dummyT) P $ absfree ("H", dummyT) Q $ Syntax.free "H" 74 | wand_tr ts = raise TERM ("wand_tr", ts); 75\<close> 76 77parse_translation \<open> 78 [(\<^syntax_const>\<open>_emp\<close>, K emp_tr), 79 (\<^syntax_const>\<open>_singl\<close>, K singl_tr), 80 (\<^syntax_const>\<open>_star\<close>, K star_tr), 81 (\<^syntax_const>\<open>_wand\<close>, K wand_tr)] 82\<close> 83 84text\<open>Now it looks much better:\<close> 85 86lemma "VARS H x y z w 87 {[x\<mapsto>y] ** [z\<mapsto>w]} 88 SKIP 89 {x \<noteq> z}" 90apply vcg 91apply(auto simp:star_def ortho_def singl_def) 92done 93 94lemma "VARS H x y z w 95 {emp ** emp} 96 SKIP 97 {emp}" 98apply vcg 99apply(auto simp:star_def ortho_def is_empty_def) 100done 101 102text\<open>But the output is still unreadable. Thus we also strip the heap 103parameters upon output:\<close> 104 105ML \<open> 106local 107 108fun strip (Abs(_,_,(t as Const("_free",_) $ Free _) $ Bound 0)) = t 109 | strip (Abs(_,_,(t as Free _) $ Bound 0)) = t 110\<^cancel>\<open>| strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps\<close> 111 | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t 112 | strip (Abs(_,_,P)) = P 113 | strip (Const(\<^const_syntax>\<open>is_empty\<close>,_)) = Syntax.const \<^syntax_const>\<open>_emp\<close> 114 | strip t = t; 115 116in 117 118fun is_empty_tr' [_] = Syntax.const \<^syntax_const>\<open>_emp\<close> 119fun singl_tr' [_,p,q] = Syntax.const \<^syntax_const>\<open>_singl\<close> $ p $ q 120fun star_tr' [P,Q,_] = Syntax.const \<^syntax_const>\<open>_star\<close> $ strip P $ strip Q 121fun wand_tr' [P,Q,_] = Syntax.const \<^syntax_const>\<open>_wand\<close> $ strip P $ strip Q 122 123end 124\<close> 125 126print_translation \<open> 127 [(\<^const_syntax>\<open>is_empty\<close>, K is_empty_tr'), 128 (\<^const_syntax>\<open>singl\<close>, K singl_tr'), 129 (\<^const_syntax>\<open>star\<close>, K star_tr'), 130 (\<^const_syntax>\<open>wand\<close>, K wand_tr')] 131\<close> 132 133text\<open>Now the intermediate proof states are also readable:\<close> 134 135lemma "VARS H x y z w 136 {[x\<mapsto>y] ** [z\<mapsto>w]} 137 y := w 138 {x \<noteq> z}" 139apply vcg 140apply(auto simp:star_def ortho_def singl_def) 141done 142 143lemma "VARS H x y z w 144 {emp ** emp} 145 SKIP 146 {emp}" 147apply vcg 148apply(auto simp:star_def ortho_def is_empty_def) 149done 150 151text\<open>So far we have unfolded the separation logic connectives in 152proofs. Here comes a simple example of a program proof that uses a law 153of separation logic instead.\<close> 154 155\<comment> \<open>a law of separation logic\<close> 156lemma star_comm: "P ** Q = Q ** P" 157 by(auto simp add:star_def ortho_def dest: map_add_comm) 158 159lemma "VARS H x y z w 160 {P ** Q} 161 SKIP 162 {Q ** P}" 163apply vcg 164apply(simp add: star_comm) 165done 166 167 168lemma "VARS H 169 {p\<noteq>0 \<and> [p \<mapsto> x] ** List H q qs} 170 H := H(p \<mapsto> q) 171 {List H p (p#qs)}" 172apply vcg 173apply(simp add: star_def ortho_def singl_def) 174apply clarify 175apply(subgoal_tac "p \<notin> set qs") 176 prefer 2 177 apply(blast dest:list_in_heap) 178apply simp 179done 180 181lemma "VARS H p q r 182 {List H p Ps ** List H q Qs} 183 WHILE p \<noteq> 0 184 INV {\<exists>ps qs. (List H p ps ** List H q qs) \<and> rev ps @ qs = rev Ps @ Qs} 185 DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD 186 {List H q (rev Ps @ Qs)}" 187apply vcg 188apply(simp_all add: star_def ortho_def singl_def) 189 190apply fastforce 191 192apply (clarsimp simp add:List_non_null) 193apply(rename_tac ps') 194apply(rule_tac x = ps' in exI) 195apply(rule_tac x = "p#qs" in exI) 196apply simp 197apply(rule_tac x = "h1(p:=None)" in exI) 198apply(rule_tac x = "h2(p\<mapsto>q)" in exI) 199apply simp 200apply(rule conjI) 201 apply(rule ext) 202 apply(simp add:map_add_def split:option.split) 203apply(rule conjI) 204 apply blast 205apply(simp add:map_add_def split:option.split) 206apply(rule conjI) 207apply(subgoal_tac "p \<notin> set qs") 208 prefer 2 209 apply(blast dest:list_in_heap) 210apply(simp) 211apply fast 212 213apply(fastforce) 214done 215 216end 217