18 |
18 |
19 types 'c wf_mb = 'c prog => cname => 'c mdecl => bool |
19 types 'c wf_mb = 'c prog => cname => 'c mdecl => bool |
20 |
20 |
21 constdefs |
21 constdefs |
22 |
22 |
23 wf_fdecl :: "'c prog \\<Rightarrow> fdecl \\<Rightarrow> bool" |
23 wf_fdecl :: "'c prog => fdecl => bool" |
24 "wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft" |
24 "wf_fdecl G == \\<lambda>(fn,ft). is_type G ft" |
25 |
25 |
26 wf_mhead :: "'c prog \\<Rightarrow> sig \\<Rightarrow> ty \\<Rightarrow> bool" |
26 wf_mhead :: "'c prog => sig => ty => bool" |
27 "wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT" |
27 "wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT" |
28 |
28 |
29 wf_mdecl :: "'c wf_mb \\<Rightarrow> 'c wf_mb" |
29 wf_mdecl :: "'c wf_mb => 'c wf_mb" |
30 "wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)" |
30 "wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)" |
31 |
31 |
32 wf_cdecl :: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool" |
32 wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" |
33 "wf_cdecl wf_mb G \\<equiv> |
33 "wf_cdecl wf_mb G == |
34 \\<lambda>(C,(sc,fs,ms)). |
34 \\<lambda>(C,(sc,fs,ms)). |
35 (\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and> |
35 (\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and> |
36 (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and> |
36 (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and> |
37 (case sc of None \\<Rightarrow> C = Object |
37 (case sc of None => C = Object |
38 | Some D \\<Rightarrow> |
38 | Some D => |
39 is_class G D \\<and> \\<not> G\\<turnstile>D\\<preceq>C C \\<and> |
39 is_class G D \\<and> \\<not> G\\<turnstile>D\\<preceq>C C \\<and> |
40 (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. |
40 (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. |
41 method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))" |
41 method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))" |
42 |
42 |
43 wf_prog :: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool" |
43 wf_prog :: "'c wf_mb => 'c prog => bool" |
44 "wf_prog wf_mb G \\<equiv> |
44 "wf_prog wf_mb G == |
45 let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G" |
45 let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G" |
46 |
46 |
47 end |
47 end |