28 wf_mdecl :: "'c wf_mb => 'c wf_mb" |
28 wf_mdecl :: "'c wf_mb => 'c wf_mb" |
29 "wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)" |
29 "wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)" |
30 |
30 |
31 wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" |
31 wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool" |
32 "wf_cdecl wf_mb G == |
32 "wf_cdecl wf_mb G == |
33 \\<lambda>(C,(sc,fs,ms)). |
33 \\<lambda>(C,(D,fs,ms)). |
34 (\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and> |
34 (\\<forall>f\\<in>set fs. wf_fdecl G f) \\<and> unique fs \\<and> |
35 (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and> |
35 (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and> |
36 (case sc of None => C = Object |
36 (C \\<noteq> Object \\<longrightarrow> is_class G D \\<and> \\<not>G\\<turnstile>D\\<preceq>C C \\<and> |
37 | Some D => |
37 (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. |
38 is_class G D \\<and> \\<not> G\\<turnstile>D\\<preceq>C C \\<and> |
38 method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))" |
39 (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. |
|
40 method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))" |
|
41 |
39 |
42 wf_prog :: "'c wf_mb => 'c prog => bool" |
40 wf_prog :: "'c wf_mb => 'c prog => bool" |
43 "wf_prog wf_mb G == |
41 "wf_prog wf_mb G == |
44 let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G" |
42 let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G" |
45 |
43 |