theory WWellForm imports"../Common/WellForm" Expr begin
definition wwf_J_mdecl :: "J_prog → cname → J_mb mdecl → bool" where "wwf_J_mdecl P C ≡ λ(M,b,Ts,T,(pns,body)). length Ts = length pns ∧ distinct pns ∧¬sub_RI body ∧ (case b of NonStatic → this ∉ set pns ∧ fv body ⊆ {this} ∪ set pns | Static → fv body ⊆ set pns)"
lemma wwf_J_mdecl_NonStatic[simp]: "wwf_J_mdecl P C (M,NonStatic,Ts,T,pns,body) = (length Ts = length pns ∧ distinct pns ∧¬sub_RI body ∧ this ∉ set pns ∧ fv body⊆ {this} ∪ set pns)" (*<*)by(simp add:wwf_J_mdecl_def)(*>*)
lemma wwf_J_mdecl_Static[simp]: "wwf_J_mdecl P C (M,Static,Ts,T,pns,body) = (length Ts = length pns ∧ distinct pns ∧¬sub_RI body ∧ fv body ⊆ set pns)" (*<*)by(simp add:wwf_J_mdecl_def)(*>*)
lemma sees_wwf_nsub_RI: "[ wwf_J_prog P; P ⊨ C sees M,b : Ts→T = (pns, body) in D ]==>¬sub_RI body" (*<*)by(auto dest!: sees_wf_mdecl simp: wwf_J_mdecl_def wf_mdecl_def)(*>*)
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.8 Sekunden
(vorverarbeitet am 2026-09-27)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
