1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/MicroJava/J/WellType.thy Thu Nov 11 12:23:45 1999 +0100
1.3 @@ -0,0 +1,184 @@
1.4 +(* Title: HOL/MicroJava/J/WellType.thy
1.5 + ID: $Id$
1.6 + Author: David von Oheimb
1.7 + Copyright 1999 Technische Universitaet Muenchen
1.8 +
1.9 +Well-typedness of Java programs
1.10 +
1.11 +the formulation of well-typedness of method calls given below (as well as
1.12 +the Java Specification 1.0) is a little too restrictive: Is does not allow
1.13 +methods of class Object to be called upon references of interface type.
1.14 +
1.15 +simplifications:
1.16 +* the type rules include all static checks on expressions and statements, e.g.
1.17 + definedness of names (of parameters, locals, fields, methods)
1.18 +
1.19 +*)
1.20 +
1.21 +WellType = Term + WellForm +
1.22 +
1.23 +types lenv (* local variables, including method parameters and This *)
1.24 + = "vname \\<leadsto> ty"
1.25 + 'c env
1.26 + = "'c prog \\<times> lenv"
1.27 +
1.28 +syntax
1.29 +
1.30 + prg :: "'c env \\<Rightarrow> 'c prog"
1.31 + localT :: "'c env \\<Rightarrow> (vname \\<leadsto> ty)"
1.32 +
1.33 +translations
1.34 +
1.35 + "prg" => "fst"
1.36 + "localT" => "snd"
1.37 +
1.38 +consts
1.39 +
1.40 + more_spec :: "'c prog \\<Rightarrow> (ty \\<times> 'x) \\<times> ty list \\<Rightarrow>
1.41 + (ty \\<times> 'x) \\<times> ty list \\<Rightarrow> bool"
1.42 + m_head :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> (ty \\<times> ty) option"
1.43 + appl_methds :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
1.44 + max_spec :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
1.45 +
1.46 +defs
1.47 +
1.48 + m_head_def "m_head G t sig \\<equiv> case t of NullT \\<Rightarrow> None | ClassT C \\<Rightarrow>
1.49 + option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (cmethd (G,C) sig)"
1.50 +
1.51 + more_spec_def "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
1.52 + list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
1.53 +
1.54 + (* applicable methods, cf. 15.11.2.1 *)
1.55 + appl_methds_def "appl_methds G T \\<equiv> \\<lambda>(mn, pTs). {(mh,pTs') |mh pTs'.
1.56 + m_head G T (mn, pTs') = Some mh \\<and>
1.57 + list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
1.58 +
1.59 + (* maximally specific methods, cf. 15.11.2.2 *)
1.60 + max_spec_def "max_spec G rT sig \\<equiv> {m. m \\<in>appl_methds G rT sig \\<and>
1.61 + (\\<forall>m'\\<in>appl_methds G rT sig.
1.62 + more_spec G m' m \\<longrightarrow> m' = m)}"
1.63 +consts
1.64 +
1.65 + typeof :: "(loc \\<Rightarrow> ty option) \\<Rightarrow> val \\<Rightarrow> ty option"
1.66 +
1.67 +primrec
1.68 + "typeof dt Unit = Some (PrimT Void)"
1.69 + "typeof dt Null = Some NT"
1.70 + "typeof dt (Bool b) = Some (PrimT Boolean)"
1.71 + "typeof dt (Intg i) = Some (PrimT Integer)"
1.72 + "typeof dt (Addr a) = dt a"
1.73 +
1.74 +types
1.75 + javam = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
1.76 + (* method body with parameter names, local variables, block, result expression *)
1.77 +
1.78 +consts
1.79 +
1.80 + ty_expr :: "javam env \\<Rightarrow> (expr \\<times> ty ) set"
1.81 + ty_exprs:: "javam env \\<Rightarrow> (expr list \\<times> ty list) set"
1.82 + wt_stmt :: "javam env \\<Rightarrow> stmt set"
1.83 +
1.84 +syntax
1.85 +
1.86 +ty_expr :: "javam env \\<Rightarrow> [expr , ty ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_" [51,51,51]50)
1.87 +ty_exprs:: "javam env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
1.88 +wt_stmt :: "javam env \\<Rightarrow> stmt \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51 ]50)
1.89 +
1.90 +translations
1.91 + "E\\<turnstile>e \\<Colon> T" == "(e,T) \\<in> ty_expr E"
1.92 + "E\\<turnstile>e[\\<Colon>]T" == "(e,T) \\<in> ty_exprs E"
1.93 + "E\\<turnstile>c \\<surd>" == "c \\<in> wt_stmt E"
1.94 +
1.95 +inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intrs
1.96 +
1.97 +(* well-typed expressions *)
1.98 +
1.99 + (* cf. 15.8 *)
1.100 + NewC "\\<lbrakk>is_class (prg E) C\\<rbrakk> \\<Longrightarrow>
1.101 + E\\<turnstile>NewC C\\<Colon>Class C"
1.102 +
1.103 + (* cf. 15.15 *)
1.104 + Cast "\\<lbrakk>E\\<turnstile>e\\<Colon>T;
1.105 + prg E\\<turnstile>T\\<Rightarrow>? T'\\<rbrakk> \\<Longrightarrow>
1.106 + E\\<turnstile>Cast T' e\\<Colon>T'"
1.107 +
1.108 + (* cf. 15.7.1 *)
1.109 + Lit "\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
1.110 + E\\<turnstile>Lit x\\<Colon>T"
1.111 +
1.112 + (* cf. 15.13.1 *)
1.113 + LAcc "\\<lbrakk>localT E v = Some T; is_type (prg E) T\\<rbrakk> \\<Longrightarrow>
1.114 + E\\<turnstile>LAcc v\\<Colon>T"
1.115 +
1.116 + (* cf. 15.25, 15.25.1 *)
1.117 + LAss "\\<lbrakk>E\\<turnstile>LAcc v\\<Colon>T;
1.118 + E\\<turnstile>e\\<Colon>T';
1.119 + prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
1.120 + E\\<turnstile>v\\<Colon>=e\\<Colon>T'"
1.121 +
1.122 + (* cf. 15.10.1 *)
1.123 + FAcc "\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
1.124 + cfield (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
1.125 + E\\<turnstile>{fd}a..fn\\<Colon>fT"
1.126 +
1.127 + (* cf. 15.25, 15.25.1 *)
1.128 + FAss "\\<lbrakk>E\\<turnstile>{fd}a..fn\\<Colon>T;
1.129 + E\\<turnstile>v \\<Colon>T';
1.130 + prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
1.131 + E\\<turnstile>{fd}a..fn\\<in>=v\\<Colon>T'"
1.132 +
1.133 +
1.134 + (* cf. 15.11.1, 15.11.2, 15.11.3 *)
1.135 + Call "\\<lbrakk>E\\<turnstile>a\\<Colon>RefT t;
1.136 + E\\<turnstile>ps[\\<Colon>]pTs;
1.137 + max_spec (prg E) t (mn, pTs) = {((md,rT),pTs')}\\<rbrakk> \\<Longrightarrow>
1.138 + E\\<turnstile>a..mn({pTs'}ps)\\<Colon>rT"
1.139 +
1.140 +(* well-typed expression lists *)
1.141 +
1.142 + (* cf. 15.11.??? *)
1.143 + Nil "E\\<turnstile>[][\\<Colon>][]"
1.144 +
1.145 + (* cf. 15.11.??? *)
1.146 + Cons "\\<lbrakk>E\\<turnstile>e\\<Colon>T;
1.147 + E\\<turnstile>es[\\<Colon>]Ts\\<rbrakk> \\<Longrightarrow>
1.148 + E\\<turnstile>e#es[\\<Colon>]T#Ts"
1.149 +
1.150 +(* well-typed statements *)
1.151 +
1.152 + Skip "E\\<turnstile>Skip\\<surd>"
1.153 +
1.154 + Expr "\\<lbrakk>E\\<turnstile>e\\<Colon>T\\<rbrakk> \\<Longrightarrow>
1.155 + E\\<turnstile>Expr e\\<surd>"
1.156 +
1.157 + Comp "\\<lbrakk>E\\<turnstile>s1\\<surd>;
1.158 + E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
1.159 + E\\<turnstile>s1;; s2\\<surd>"
1.160 +
1.161 + (* cf. 14.8 *)
1.162 + Cond "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
1.163 + E\\<turnstile>s1\\<surd>;
1.164 + E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
1.165 + E\\<turnstile>If(e) s1 Else s2\\<surd>"
1.166 +
1.167 + (* cf. 14.10 *)
1.168 + Loop "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
1.169 + E\\<turnstile>s\\<surd>\\<rbrakk> \\<Longrightarrow>
1.170 + E\\<turnstile>While(e) s\\<surd>"
1.171 +
1.172 +constdefs
1.173 +
1.174 + wt_java_mdecl :: javam prog => cname => javam mdecl => bool
1.175 +"wt_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
1.176 + length pTs = length pns \\<and>
1.177 + nodups pns \\<and>
1.178 + unique lvars \\<and>
1.179 + (\\<forall>pn\\<in>set pns. map_of lvars pn = None) \\<and>
1.180 + (\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
1.181 + (let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
1.182 + E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res\\<Colon>T \\<and> G\\<turnstile>T\\<preceq>rT))"
1.183 +
1.184 + wf_java_prog :: javam prog => bool
1.185 +"wf_java_prog G \\<equiv> wf_prog wt_java_mdecl G"
1.186 +
1.187 +end