isabelle: src/HOL/MicroJava/DFA/Typing_Framework.thy@1c2c045decb3 (annotated)

42150 b0c0638c4aad tuned headers; wenzelm parents: 35416 diff changeset	1	(* Title: HOL/MicroJava/DFA/Typing_Framework.thy
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	2	Author: Tobias Nipkow
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	3	Copyright 2000 TUM
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	4	*)
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	5
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	6	section \<open>Typing and Dataflow Analysis Framework\<close>
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	7
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	8	theory Typing_Framework
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	9	imports Listn
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	10	begin
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	11
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	12	text \<open>
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	13	The relationship between dataflow analysis and a welltyped-instruction predicate.
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	14	\<close>
42463 f270e3e18be5 modernized specifications; wenzelm parents: 42150 diff changeset	15	type_synonym 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	16
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	17	definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool" where
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	18	"stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	19
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	20	definition stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	21	"stables r step ss == !p<size ss. stable r step ss p"
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	22
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	23	definition wt_step ::
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	24	"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	25	"wt_step r T step ts ==
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	26	!p<size(ts). ts!p ~= T & stable r step ts p"
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	27
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	28	definition is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	29	\<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool" where
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	30	"is_bcv r T step n A bcv == !ss : list n A.
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	31	(!p<n. (bcv ss)!p ~= T) =
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	32	(? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	33
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	34	end

author	wenzelm
	Fri, 15 Jul 2016 23:47:07 +0200
changeset 63511	1c2c045decb3
parent 61361	8b5f00202e1a
child 67613	ce654b0e6d69
permissions	-rw-r--r--