%{ 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 . }% % Failed cast is an inductive predicate over expressions and expression lists % that contain a cast that cannot be reduced. failed_cast : classTable -> exp -> type. failed_cast_list : classTable -> elist N -> type. fc_field : failed_cast CT E -> % -------------------------------- failed_cast CT (fieldProj E N). fc_invk_recv : failed_cast CT E -> % ---------------------------------- failed_cast CT (methodInvk E MN ES). fc_invk_arg : failed_cast_list CT ES -> % ---------------------------------- failed_cast CT (methodInvk E MN ES). fc_new : failed_cast_list CT ES -> % --------------------------- failed_cast CT (new CN ES). fc_cast : notSubtype CT CN2 CN1 -> value_list ES -> % -------------------------------------- failed_cast CT (cast CN1 (new CN2 ES)). fc_cast_arg : failed_cast CT E -> % --------------------------- failed_cast CT (cast CN E). fc_hd : failed_cast CT E -> % --------------------------------- failed_cast_list CT (econs E ES). fc_tl : failed_cast_list CT ES -> % --------------------------------- failed_cast_list CT (econs E ES). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Disjoint sums for progress % With respect to a classTable an expression is either: a value, can take % a step or contains a failed cast. progsum : classTable -> exp -> type. ps_value : value E -> progsum CT E. ps_step : reduction CT E1 E2 -> progsum CT E1. ps_failed : failed_cast CT E -> progsum CT E. % Analogous cases for expression lists progsum_list : classTable -> elist N -> type. psl_value : value_list ES -> progsum_list CT ES. psl_step : reduction_list CT ES1 ES2 -> progsum_list CT ES1. psl_failed : failed_cast_list CT ES -> progsum_list CT ES. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Proof of progress for expressions and expression lists. % Every case of the proof requires a helper lemma because of output coverage % constraints. progress : {CT:classTable} class_table_typing CT -> typing CT E C -> progsum CT E -> type. %mode progress +CT +CTT +TP -PS. progress_list : {CT:classTable} class_table_typing CT -> typing_list CT ES C -> progsum_list CT ES -> type. %mode progress_list +CT +CTT +TPS -PSL. %%%% Cases for well-typed casts progress_cast_helper2 : value (new C ES) -> xm_subtype CT C D -> progsum CT (cast D (new C ES)) -> type. %mode progress_cast_helper2 +VL +XMSB -PS. - : progress_cast_helper2 VL (xms_sub SB) (ps_step (r_cast SB)). - : progress_cast_helper2 (v_newv VLS) (xms_notsub NSB) (ps_failed (fc_cast NSB VLS)). %worlds () (progress_cast_helper2 VL XMSB PS). %total XMSB (progress_cast_helper2 VL XMSB PS). progress_cast_helper1 : {CT:classTable} {D:className} class_table_typing CT -> progsum CT E -> progsum CT (cast D E) -> type. %mode progress_cast_helper1 +CT +D +CTT +PS1 -PS2. - : progress_cast_helper2 VL XMSB PS -> sb_total CT _ D CTT XMSB -> % ---------------------------------------------- progress_cast_helper1 CT D CTT (ps_value VL) PS. - : progress_cast_helper1 CT D CTT (ps_step RD) (ps_step (rc_cast RD)). - : progress_cast_helper1 CT D CTT (ps_failed FC) (ps_failed (fc_cast_arg FC)). %worlds () (progress_cast_helper1 CT D CTT PS1 PS2). %total PS1 (progress_cast_helper1 CT D CTT PS1 PS2). - : progress_cast_helper1 CT _ CTT PS1 PS2 -> progress CT CTT TP PS1 -> % ----------------------------------- progress CT CTT (t_cast TP) PS2. %%%% Cases for well-typed field projections progress_field_helper : {CT:classTable} class_table_typing CT -> cnnth_opt FI CS CI -> fields CT C1 N2 CS -> typing CT E C1 -> progsum CT E -> progsum CT (fieldProj E FI) -> type. %mode progress_field_helper +CT +CTT +CNOPT +FS +TP +PS1 -PS2. - : proj_lemma TP FS CNOPT ENTH -> % --------------------------------------------------------------------------- progress_field_helper CT CTT CNOPT FS TP (ps_value VL) (ps_step (r_field ENTH)). - : progress_field_helper CT CTT CNOPT FS TP (ps_step RD) (ps_step (rc_field RD)). - : progress_field_helper CT CTT CNOPT FS TP (ps_failed FC) (ps_failed (fc_field FC)). %worlds () (progress_field_helper CT CTT CNOPT FS TP PS1 PS2). %total PS1 (progress_field_helper CT CTT CNOPT FS TP PS1 PS2). - : progress_field_helper CT CTT CNOPT FS TP PS1 PS2 -> progress CT CTT TP PS1 -> % ---------------------------------------- progress CT CTT (t_field CNOPT FS TP) PS2. %%%% Cases for well-typed method invocations progress_invk_helper : {ES:elist N} {CS:cnlist N} mtype CT M C1 CS C0 -> typing CT E C1 -> typing_list CT ES CS -> progsum CT E -> progsum_list CT ES -> progsum CT (methodInvk E M ES) -> type. %mode progress_invk_helper +ES +CS +MTY +TP +TPS +PS1 +PSL -PS2. - : invoc_total ES TPS BE _ INV -> mbody_inv TP MTY BE MBY -> % --------------------------------------------------------------------------------- progress_invk_helper ES CS MTY TP TPS (ps_value VL) (psl_value VLS) (ps_step (r_invk VLS MBY INV)). - : progress_invk_helper ES CS MTY TP TPS (ps_value VL) (psl_step RDS) (ps_step (rc_invk_arg VL RDS)). - : progress_invk_helper ES CS MTY TP TPS (ps_value VL) (psl_failed FC) (ps_failed (fc_invk_arg FC)). - : progress_invk_helper ES CS MTY TP TPS (ps_step RD) PSL (ps_step (rc_invk_recv RD)). - : progress_invk_helper ES CS MTY TP TPS (ps_failed FC) PSL (ps_failed (fc_invk_recv FC)). %worlds () (progress_invk_helper ES CS MTY TP TPS PS1 PSL PS2). %total {PS1 PSL} (progress_invk_helper ES CS MTY TP TPS PS1 PSL PS2). - : progress_invk_helper _ _ MTY TP TPS PS1 PSL PS2 -> progress CT CTT TP PS1 -> progress_list CT CTT TPS PSL -> % ---------------------------------------- progress CT CTT (t_invk TPS MTY TP) PS2. %%%% Cases for well-typed object creation progress_new_helper : {C:className} progsum_list CT ES -> progsum CT (new C ES) -> type. %mode progress_new_helper +C +PSL -PS. - : progress_new_helper C (psl_value VLS) (ps_value (v_newv VLS)). - : progress_new_helper C (psl_step RDS) (ps_step (rc_new_arg RDS)). - : progress_new_helper C (psl_failed FC) (ps_failed (fc_new FC)). %worlds () (progress_new_helper C PSL PS). %total PSL (progress_new_helper C PSL PS). - : progress_new_helper _ PSL PS -> progress_list CT CTT TPS PSL -> % ----------------------------------- progress CT CTT (t_new TPS FS) PS. %%%% Cases for well-typed expression lists progress_list_helper : progsum CT E -> progsum_list CT ES -> progsum_list CT (econs E ES) -> type. %mode progress_list_helper +PS +PSL1 -PSL2. - : progress_list_helper (ps_value VL) (psl_value VLS) (psl_value (v_cons VLS VL)). - : progress_list_helper (ps_value VL) (psl_step RDS) (psl_step (rl_tl VL RDS)). - : progress_list_helper (ps_value VL) (psl_failed FC) (psl_failed (fc_tl FC)). - : progress_list_helper (ps_step RD) _ (psl_step (rl_hd RD)). - : progress_list_helper (ps_failed FC) _ (psl_failed (fc_hd FC)). %worlds () (progress_list_helper PS PSL1 PSL2). %total PS (progress_list_helper PS PSL1 PSL2). - : % ---------------------------------------------- progress_list CT CTT (tl_nil) (psl_value v_nil). - : progress_list_helper PS1 PSL1 PSL2 -> progress CT CTT TP PS1 -> progress_list CT CTT TPS PSL1 -> % -------------------------------------------- progress_list CT CTT (tl_cons SB TPS TP) PSL2. %worlds () (progress CT CTT TP PS) (progress_list CT CTT TPS PSL). %total (TP TPS) (progress CT1 CTT1 TP PS) (progress_list CT2 CTT2 TPS PSL).