equal
deleted
inserted
replaced
17 imports Hoare_Logic_Abort SepLogHeap |
17 imports Hoare_Logic_Abort SepLogHeap |
18 begin |
18 begin |
19 |
19 |
20 text\<open>The semantic definition of a few connectives:\<close> |
20 text\<open>The semantic definition of a few connectives:\<close> |
21 |
21 |
22 definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) |
22 definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix \<open>\<bottom>\<close> 55) |
23 where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}" |
23 where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}" |
24 |
24 |
25 definition is_empty :: "heap \<Rightarrow> bool" |
25 definition is_empty :: "heap \<Rightarrow> bool" |
26 where "is_empty h \<longleftrightarrow> h = Map.empty" |
26 where "is_empty h \<longleftrightarrow> h = Map.empty" |
27 |
27 |
49 upon parsing/printing. Thus every pointer program needs to have a |
49 upon parsing/printing. Thus every pointer program needs to have a |
50 program variable H, and assertions should not contain any locally |
50 program variable H, and assertions should not contain any locally |
51 bound Hs - otherwise they may bind the implicit H.\<close> |
51 bound Hs - otherwise they may bind the implicit H.\<close> |
52 |
52 |
53 syntax |
53 syntax |
54 "_emp" :: "bool" ("emp") |
54 "_emp" :: "bool" (\<open>emp\<close>) |
55 "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]") |
55 "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" (\<open>[_ \<mapsto> _]\<close>) |
56 "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60) |
56 "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>**\<close> 60) |
57 "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60) |
57 "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>-*\<close> 60) |
58 |
58 |
59 (* FIXME does not handle "_idtdummy" *) |
59 (* FIXME does not handle "_idtdummy" *) |
60 ML \<open> |
60 ML \<open> |
61 \<comment> \<open>\<open>free_tr\<close> takes care of free vars in the scope of separation logic connectives: |
61 \<comment> \<open>\<open>free_tr\<close> takes care of free vars in the scope of separation logic connectives: |
62 they are implicitly applied to the heap\<close> |
62 they are implicitly applied to the heap\<close> |