Theory ExternalCall
section ‹Semantics of method calls that cannot be defined inside JinjaThreads›
theory ExternalCall
imports
"../Framework/FWSemantics"
Conform
begin
type_synonym
('addr,'thread_id,'heap) external_thread_action = "('addr, 'thread_id, cname × mname × 'addr,'heap) Jinja_thread_action"
print_translation ‹
let
fun tr'
[a1, t
, Const (@{type_syntax "prod"}, _) $ Const (@{type_syntax "String.literal"}, _) $
(Const (@{type_syntax "prod"}, _) $ Const (@{type_syntax "String.literal"}, _) $ a2)
, h] =
if a1 = a2 then Syntax.const @{type_syntax "external_thread_action"} $ a1 $ t $ h
else raise Match;
in [(@{type_syntax "Jinja_thread_action"}, K tr')]
end
›
typ "('addr,'thread_id,'heap) external_thread_action"
subsection ‹Typing of external calls›
inductive external_WT_defs :: "cname ⇒ mname ⇒ ty list ⇒ ty ⇒ bool" (‹(_∙_'(_')) :: _› [50, 0, 0, 50] 60)
where
"Thread∙start([]) :: Void"
| "Thread∙join([]) :: Void"
| "Thread∙interrupt([]) :: Void"
| "Thread∙isInterrupted([]) :: Boolean"
| "Object∙wait([]) :: Void"
| "Object∙notify([]) :: Void"
| "Object∙notifyAll([]) :: Void"
| "Object∙clone([]) :: Class Object"
| "Object∙hashcode([]) :: Integer"
| "Object∙print([Integer]) :: Void"
| "Object∙currentThread([]) :: Class Thread"
| "Object∙interrupted([]) :: Boolean"
| "Object∙yield([]) :: Void"
inductive_cases external_WT_defs_cases:
"a∙start(vs) :: T"
"a∙join(vs) :: T"
"a∙interrupt(vs) :: T"
"a∙isInterrupted(vs) :: T"
"a∙wait(vs) :: T"
"a∙notify(vs) :: T"
"a∙notifyAll(vs) :: T"
"a∙clone(vs) :: T"
"a∙hashcode(vs) :: T"
"a∙print(vs) :: T"
"a∙currentThread(vs) :: T"
"a∙interrupted([]) :: T"
"a∙yield(vs) :: T"
inductive is_native :: "'m prog ⇒ htype ⇒ mname ⇒ bool"
for P :: "'m prog" and hT :: htype and M :: mname
where "⟦ P ⊢ class_type_of hT sees M:Ts→T = Native in D; D∙M(Ts) :: T ⟧ ⟹ is_native P hT M"
lemma is_nativeD: "is_native P hT M ⟹ ∃Ts T D. P ⊢ class_type_of hT sees M:Ts→T = Native in D ∧ D∙M(Ts)::T"
by(simp add: is_native.simps)
inductive (in heap_base) external_WT' :: "'m prog ⇒ 'heap ⇒ 'addr ⇒ mname ⇒ 'addr val list ⇒ ty ⇒ bool"
(‹_,_ ⊢ (_∙_'(_')) : _› [50,0,0,0,50] 60)
for P :: "'m prog" and h :: 'heap and a :: 'addr and M :: mname and vs :: "'addr val list" and U :: ty
where
"⟦ typeof_addr h a = ⌊hT⌋; map typeof⇘h⇙ vs = map Some Ts; P ⊢ class_type_of hT sees M:Ts'→U = Native in D;
P ⊢ Ts [≤] Ts' ⟧
⟹ P,h ⊢ a∙M(vs) : U"
context heap_base begin
lemma external_WT'_iff:
"P,h ⊢ a∙M(vs) : U ⟷
(∃hT Ts Ts' D. typeof_addr h a = ⌊hT⌋ ∧ map typeof⇘h⇙ vs = map Some Ts ∧ P ⊢ class_type_of hT sees M:Ts'→U=Native in D ∧ P ⊢ Ts [≤] Ts')"
by(simp add: external_WT'.simps)
end
context heap begin
lemma external_WT'_hext_mono:
"⟦ P,h ⊢ a∙M(vs) : T; h ⊴ h' ⟧ ⟹ P,h' ⊢ a∙M(vs) : T"
by(auto 5 2 simp add: external_WT'_iff dest: typeof_addr_hext_mono map_typeof_hext_mono)
end
subsection ‹Semantics of external calls›