%{ This is part of a proof of the soundness of Featherweight Java (Atsushi Igarashi, Benjamin Pierce and Philip Wadler) in the Twelf logical Framework. It was developed by Stephanie Weirich and Geoffrey Washburn . }% %% Semantics of FJ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Abstract syntax %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% className : type. %name className C c. methodName : type. %name methodName M m. % Method and class names are just natural numbers methodName_nat : nat -> methodName. cn : nat -> className. % Object is the only pre-existing class, defined to be natural number zero. object : className = cn z. % Class name lists. Indexed by length cnlist : nat -> type. %name cnlist CS cs. cnnil : cnlist z. % Empty class name list cncons : className -> cnlist N -> cnlist (s N). % Class name list cons % Expressions and expression lists exp : type. %name exp E e. elist : nat -> type. %name elist ES es. % lists are indexed by length fieldProj : exp -> nat -> exp. methodInvk : exp -> methodName -> elist N -> exp. new : className -> elist N -> exp. cast : className -> exp -> exp. % and enil : elist z. econs : exp -> elist N -> elist (s N). %% a simple expression unit : exp = new object enil. % Expressions with binders (used for method bodies), indexed by className lists for % convenience. Idea mostly taken from CMU POPLmark solution % Base case abstract a single variable for "this" % Bind case binds an additional argument. bexp : cnlist N -> type. %name bexp BE be. base : (exp -> exp) -> bexp cnnil. bind : {C:className} (exp -> bexp CS) -> bexp (cncons C CS). % Method declaration methodDef : methodName -> type. %name methodDef MD md. method : className -> {M :methodName} bexp CS -> methodDef M. % Assoc tables of methods methodTable : type. %name methodTable MR mr. %% definition of methodTable is below. We are using a representation of method %% tables that includes a proof that labels are not repeated. However, we have %% to define equality for method names first. We could drop this proof and still %% prove the soundness of FJ, but adding this to our representation makes the %% adequacy proof easier. % Class definition classDef : className -> type. %name classDef CD cd. class : {C :className } className -> cnlist N -> methodTable -> classDef C. % class table %% The invariant is "object" cannot be a part of the class table. %% This is satisfied by the well-formedness rule for class tables. %% the "cons" constructor also ensures that all class definitions in the table are unique. %% For type soundness, this isn't actually necessary, but it does make our adequacy proof %% a little easier. classTable : type. %name classTable CT cr. %% definition of classTable is also below %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Relations and functions on the abstract syntax %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Equality relation for class names className_eq : className -> className -> type. %name className_eq CNEQ cneq. %mode className_eq +CN1 +CN2. % FIX - Do I need this mode declaration? % className_refl : nat_eq N1 N2 -> % % -------------------------------------- % className_eq (cn N1) (cn N2). className_refl: className_eq N N. %worlds () (className_eq CN1 CN2). %terminates {CN1 CN2} (className_eq CN1 CN2). %%%%%%%%%%%%% % Not equals relation for class names className_neq : className -> className -> type. %name className_neq CNNEQ cnneq. %mode className_neq +CN1 +CN2. % FIX - Do I need this mode declaration? className_neq_natnat : nat_neq N1 N2 -> % ---------------------------------------- className_neq (cn N1) (cn N2). %worlds () (className_neq CN1 CN2). %terminates {CN1 CN2} (className_neq CN1 CN2). %%%%%%%%%%%%% % Equality relation for method names methodName_eq : methodName -> methodName -> type. %name methodName_eq MNEQ mneq. %mode methodName_eq +MN1 +MN2. % FIX - Do I need this mode declaration? % methodName_eq_base : nat_eq N1 N2 -> % % -------------------------------------- % methodName_eq (methodName_nat N1) (methodName_nat N2). methodName_refl : methodName_eq M1 M1. %worlds () (methodName_eq MN1 MN2). %terminates {MN1 MN2} (methodName_eq MN1 MN2). %%%%%%%%%%%%% % Not equals relation for method names methodName_neq : methodName -> methodName -> type. %name methodName_neq MNNEQ mnneq. %mode methodName_neq +MN1 +MN2. % FIX - Do I need this mode declaration? methodName_neq_base : nat_neq N1 N2 -> % --------------------------------------- methodName_neq (methodName_nat N1) (methodName_nat N2). %worlds () (methodName_neq MN1 MN2). %terminates {MN1 MN2} (methodName_neq MN1 MN2). %%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % List manipulation functions for expression and class name lists. % Nth for expression lists enth_opt : nat -> elist N -> exp -> type. %mode enth_opt +N +ES -E. enth_sz: enth_opt z (econs E _) E. enth_sn: enth_opt N TL E -> enth_opt (s N) (econs E' TL) E. %worlds () (enth_opt N EL E). %terminates N (enth_opt N EL E). %%%%%%%%%%%%% % Nth for classname lists cnnth_opt : nat -> cnlist N -> className -> type. %mode cnnth_opt +N +CL -C. %name cnnth_opt CNTH cnth. cnnth_sz: cnnth_opt z (cncons C CS) C. cnnth_sn: cnnth_opt N CS C -> cnnth_opt (s N) (cncons D CS) C. %worlds () (cnnth_opt N CL C). %terminates N (cnnth_opt N CL C). %%%%%%%%%%%%% % Append for class name lists cnappend : cnlist N1 -> cnlist N2 -> cnlist N3 -> plus N1 N2 N3 -> type. %mode cnappend +CNL1 +CNL2 -CNL3 -PL. cnappend_cnnil : cnappend cnnil CS CS plus_z. cnappend_cncons : cnappend CS1 CS2 CS3 PL -> % ---------------------------------------------------------- cnappend (cncons CN CS1) CS2 (cncons CN CS3) (plus_s PL). %worlds () (cnappend CS1 CS2 CS3 PL). %terminates CS1 (cnappend CS1 CS2 CS3 PL). %unique cnappend +CS1 +CS2 -1CS3 -1PL. %covers cnappend +CS1 +CS2 -CS3 -PL. %total CS1 (cnappend CS1 CS2 CS3 PL). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Helper functions for method and class tables as well as % class table and method table abstract syntax. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % method and class tables embed proofs that each new name is not already added % to the class table. Therefore, we have to define names not appearing in tables % simultaneously with the tables themselves. notInMT : methodTable -> methodName -> type. %mode notInMT +M +MT. %name notInMT NI ni. notInCT : classTable -> className -> type. %mode notInCT +C +CT. % Empty method record mrnil : methodTable. % Method record cons mrcons : {MD : methodDef M}{MT: methodTable} notInMT MT M -> methodTable. % Empty class table crnil : classTable. % class table cons. crcons : {CD : classDef C}{ CT: classTable} notInCT CT C -> classTable. %%%%%%%%%%%%% %% a method name is NOT defined in a method table notInMT_mrnil : notInMT mrnil M. notInMT_mrcons: notInMT MT M -> methodName_neq M M' -> notInMT (mrcons (method _ M' _) MT NI') M. %worlds () (notInMT M N). %%%%%%%%%%%%% %% a class name is NOT defined in a class table nnil : notInCT crnil C. ncons : notInCT CT N -> className_neq N N' -> notInCT (crcons (class N' _ _ _) CT NI') N. %worlds () (notInCT CT C). %%%%%%%%%%%%% % Method lookup lookupMethod : methodTable -> {M :methodName} methodDef M -> type. %name lookupMethod LM lm. %mode lookupMethod +MR +MN -MD. lookupMethod_mrcons1 : % methodName_eq MN1 MN2 -> % ------------------------------------------------------- lookupMethod (mrcons (method C MN1 BE) MT MU) MN1 (method C MN1 BE). lookupMethod_mrcons2 : methodName_neq MN1 MN2 -> lookupMethod MR MN1 MD -> % ----------------------------------------------------------------- lookupMethod (mrcons (method C MN2 BE) MR MU) MN1 MD. %worlds () (lookupMethod MR MN MD). %terminates MR (lookupMethod MR MN MD). %%%%%%%%%%%%% % Find the class definition for a given class. %% returns the rest of the class table, which is where the superclass of lookupClass : {CT:classTable} {C:className} classDef C -> type. %name lookupClass LC lc. %mode lookupClass +CT +CN -CD. lookupClass_crcons1 : % ------------------------------------------------------------ lookupClass (crcons (class CN2 CN3 CNL MR) CT CTU) CN2 (class CN2 CN3 CNL MR). lookupClass_crcons2 : className_neq CN1 CN2 -> lookupClass CT CN1 CD -> % ------------------------------------------------------------------- lookupClass (crcons (class CN2 CN3 CNL MR) CT CTU) CN1 CD. %worlds () (lookupClass CN CT CD). %terminates CN (lookupClass CN CT CD). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Static Semantics of FJ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Subtyping %% Note, I couldn't specify the mode I wanted for subtyping because of the %% transitivity rule---the middle types are not ground inputs. %% therefore, I'm using an 'algorithmic' subtyping judgment instead. %% I should lookup later whether I can use the subtyping judgment that appears %% in TAPL instead. %% In the end, we don't need the mode declaration for subtyping. On the other %% hand, defining subtyping in this way means that our type system is syntax %% directed and proof search capabilities of twelf means that we have also %% implemented a type checker. subtyping: classTable -> className -> className -> type. %name subtyping SB sb. %%mode subtyping +CT +CN1 +CN2. s_refl: subtyping CT C C. % s_trans: subtyping CT C1 C2 -> % subtyping CT C2 C3 -> % % ------------------ % subtyping CT C1 C3. s_super : subtyping CT D E -> lookupClass CT C (class C D _ _) -> className_neq C object -> % ------------------------------------------- subtyping CT C E. %worlds () (subtyping CT C1 C2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Calculate the fields of a given class fields : classTable -> className -> {N:nat} cnlist N -> type. %mode fields +CT +C -N -CS. f_obj : fields _ object z cnnil. f_class : cnappend CS2 CS1 (CS3 : cnlist N) _ -> fields CT D _ CS2 -> lookupClass CT C (class C D CS1 _) -> className_neq C object -> % --------------------------------------------------------------------- fields CT C N CS3. %worlds () (fields CT C M CS). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Method type lookup %% method M in class C1 takes args CS and produces C2. mtype : {CT:classTable} methodName -> className -> cnlist N -> className -> type. %name mtype MTY mty. %mode mtype +CT +M +C1 -CS -C2. %% method is found in this class. mt_class : lookupMethod MT M (method C2 _ (BE : bexp CS)) -> lookupClass CT C1 (class _ _ _ MT) -> className_neq C1 object -> % --------------------------------------------------- mtype CT M C1 CS C2. %% the method is not found in this class, but is found in some %% superclass mt_super : mtype CT M C2 CS C0 -> notInMT MT M -> lookupClass CT C1 (class _ C2 _ MT) -> className_neq C1 object -> % ------------------------------------------------------ mtype CT M C1 CS C0. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Method body lookup mbody : classTable -> methodName -> className -> bexp CS -> type. %mode mbody +CT +M +CNEQ -BE. mb_class : lookupMethod MT M (method _ _ BE) -> lookupClass CT C1 (class _ _ _ MT) -> className_neq C1 object -> % --------------------------------------------------- mbody CT M C1 BE. mb_super : notInMT MT M -> mbody CT M C2 BE -> lookupClass CT C1 (class _ C2 _ MT) -> className_neq C1 object -> % ------------------------------------------------------ mbody CT M C1 BE. %worlds () (mbody C CT M BE). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% method not defined in a class. method_undefined : classTable -> methodName -> className -> type. %mode method_undefined +CT +M +C. %name method_undefined MU mu. mu_object : method_undefined CT M object. mu_super : method_undefined CT M D -> notInMT MT M -> lookupClass CT C (class _ D _ MT) -> className_neq C object -> % -------------------------------------------------- method_undefined CT M C. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Expression/expression list typing %% although expression typing is "tight", expression list typing is not. typing : {CT:classTable} exp -> className -> type. %% %mode typing +CT +E -C. typing_list : {CT:classTable} elist N -> cnlist N -> type. %% %mode typing_list +CT +ES +CS. t_field : cnnth_opt FI CS CI -> fields CT C1 N2 CS -> typing CT E C1 -> % ---------------------------------- typing CT (fieldProj E FI) CI. t_invk : typing_list CT ES DS -> mtype CT M C0 DS C -> typing CT E0 C0 -> % ------------------------------------ typing CT (methodInvk E0 M ES) C. t_new : typing_list CT ES DS -> fields CT C N DS -> % --------------------------- typing CT (new C ES) C. t_cast : typing CT E C1 -> % --------------------------- typing CT (cast C2 E) C2. tl_nil : typing_list CT enil cnnil. tl_cons : subtyping CT C0 C -> typing_list CT ES CS -> typing CT E C0 -> % --------------------------------------------- typing_list CT (econs E ES) (cncons C CS). %% Notes about typing judgment: % casts include both safe and unsafe casts. % field projection uses the "partial" version of nth---if there is % a derivation of nth then the expression will be well-typed. That % seems reasonable to me. %%terminates E (typing CT E C). % Can't prove this b/c don't know fields is total %% typing for method bodies typing_bexp : classTable -> bexp CS -> className -> className -> type. %% %mode typing_bexp +CT +BE +C -E. t_base : ({THIS:exp}{D:typing CT THIS C} typing CT (E THIS) E0) -> % ----------------------------------------------------- typing_bexp CT (base E) C E0. t_bind : ({XI:exp}{D:typing CT XI CI} typing_bexp CT (E XI) C E0) -> % ----------------------------------------------------- typing_bexp CT (bind CI E) C E0. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Check that all definitions of the method above class name have the %% same type. override : classTable -> methodName -> className -> cnlist N -> className -> type. %mode override +CT +M +C +CS +DS. %% mtype is defined for M ov1 : mtype CT M D CS C -> override CT M D CS C. %% mtype is not defined for M ov2 : method_undefined CT M D -> override CT M D CS C. method_typing : classTable -> {M : methodName} methodDef M -> className -> type. %% %mode method_typing +CT +M +MD +C. t_method : subtyping CT E0 C0 -> typing_bexp CT BE C E0 -> override CT M D CS C0 -> lookupClass CT C (class C D FS MT) % ------------------------------------------------ -> method_typing CT M (method C0 M (BE: bexp CS)) C. method_table_typing : classTable -> methodTable -> className -> type. %% %mode method_table_typing +CT +MT +C. mtt_nil : method_table_typing CT mrnil C. mtt_cons : method_table_typing CT MT C -> method_typing CT M MD C -> method_table_typing CT (mrcons (MD : methodDef M) MT MNI) C. class_typing : classTable -> {C:className} classDef C -> type. % %mode class_typing +CT +C +CD. t_class : fields CT D N DS %% side effect of checking that %% D is either object or in CT. -> method_table_typing CT MT C -> subtyping CT D object % -------------------------------------------------------- -> class_typing CT C (class C D FS MT). class_table_typing_help : classTable -> classTable -> type. ctt_nil : class_table_typing_help CT0 crnil. ctt_cons : class_table_typing_help CT0 CT -> class_typing CT0 C CD -> className_neq C object % -------------------------------------- -> class_table_typing_help CT0 (crcons (CD : classDef C) CT CTI). class_table_typing : classTable -> type. % %mode class_table_typing +CT. ctt : class_table_typing_help CT CT -> class_table_typing CT. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % FJ Operational semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Method body invocation helper % Given a method body a list of arguments and a this expression, perform the substitutions invoc : bexp (CS:cnlist N) -> elist N -> exp -> exp -> type. %mode invoc +BT +TL +T1 -T2. invoc_base : invoc (base ([this:exp] E1 this)) enil E2 (E1 E2). invoc_bind : invoc (BE E1) EL E2 E3 -> % -------------------------------------------------- invoc (bind _ ([x:exp] BE x)) (econs E1 EL) E2 E3. %worlds () (invoc BE EL E1 E2). %unique invoc +BE +EL +E1 -1E2. %total BE (invoc BE EL E1 E2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Values and lists of values value_list : elist N -> type. %name value_list VL vl. %mode value_list +EL. value : exp -> type. %name value V v. %mode value +E. v_nil : value_list enil. v_cons : value_list EL -> value E -> % ----------------------- value_list (econs E EL). v_newv : value_list EL -> % ------------------ value (new C EL). %terminates (E EL) (value E) (value_list EL). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Operational semantics reduction_list : {CT:classTable} elist N -> elist N -> type. reduction : {CT:classTable} exp -> exp -> type. r_field : enth_opt N2 EL E -> % -------------------------------------------- reduction CT (fieldProj (new C (EL : elist N1)) N2) E. r_invk : value_list EL2 -> mbody CT M C BE -> invoc BE EL2 (new C EL1) E -> % -------------------------------------------- reduction CT (methodInvk (new C EL1) M EL2) E. r_cast : subtyping CT C1 C2 -> % ----------------------------------------------- reduction CT (cast C2 (new C1 EL)) (new C1 EL). rc_field : reduction CT E1 E2 -> % --------------------------------------------- reduction CT (fieldProj E1 N) (fieldProj E2 N). rc_invk_recv : reduction CT E1 E2 -> % -------------------------------------------------- reduction CT (methodInvk E1 M EL) (methodInvk E2 M EL). rc_invk_arg : value E -> reduction_list CT EL1 EL2 -> % ---------------------------------------------------- reduction CT (methodInvk E M EL1) (methodInvk E M EL2). rc_new_arg : reduction_list CT EL1 EL2 -> % ------------------------------------ reduction CT (new C EL1) (new C EL2). rc_cast : reduction CT E1 E2 -> % ------------------------------------ reduction CT (cast C E1) (cast C E2). rl_hd : reduction CT E1 E2 -> % --------------------------------------------- reduction_list CT (econs E1 EL) (econs E2 EL). rl_tl : value E -> reduction_list CT EL1 EL2 -> % --------------------------------------------- reduction_list CT (econs E EL1) (econs E EL2).