(* Title: HOL/MicroJava/DFA/Typing_Framework.thy Author: Tobias Nipkow Copyright 2000 TUM
*)
section \<open>Typing and Dataflow Analysis Framework\<close>
theory Typing_Framework imports Listn begin
text\<open>
The relationship between dataflow analysis and a welltyped-instruction predicate. \<close> type_synonym's step_type = "nat \ 's \ (nat \ 's) list"
definition stable :: "'s ord \ 's step_type \ 's list \ nat \ bool" where "stable r step ss p == \(q,s')\set(step p (ss!p)). s' <=_r ss!q"
definition stables :: "'s ord \ 's step_type \ 's list \ bool" where "stables r step ss == \p
definition wt_step :: "'s ord \ 's \ 's step_type \ 's list \ bool" where "wt_step r T step ts == \<forall>p<size(ts). ts!p ~= T & stable r step ts p"
definition is_bcv :: "'s ord \ 's \ 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool" where "is_bcv r T step n A bcv == \ss \ list n A.
(\<forall>p<n. (bcv ss)!p ~= T) =
(\<exists>ts \<in> list n A. ss <=[r] ts & wt_step r T step ts)"
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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 ist noch experimentell.
