(* Title: HOL/MicroJava/DFA/Typing_Framework.thy Author: Tobias Nipkow Copyright 2000 TUM *)
section‹Typing and Dataflow Analysis Framework›
theory Typing_Framework imports Listn begin
text‹ The relationship between dataflow analysis and a welltyped-instruction predicate. › 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 == ∀p
definition is_bcv :: "'s ord ==> 's ==> 's step_type ==> nat ==> 's set ==> ('s list ==> 's list) ==> bool"where "is_bcv r T step n A bcv == ∀ss ∈ list n A. (∀p (∃ts ∈ list n A. ss <=[r] ts & wt_step r T step ts)"
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-05-03)
¤
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.
