equal
deleted
inserted
replaced
7 subsection "True Liveness Analysis" |
7 subsection "True Liveness Analysis" |
8 |
8 |
9 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where |
9 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where |
10 "L SKIP X = X" | |
10 "L SKIP X = X" | |
11 "L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" | |
11 "L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" | |
12 "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" | |
12 "L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" | |
13 "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" | |
13 "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" | |
14 "L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)" |
14 "L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)" |
15 |
15 |
16 lemma L_mono: "mono (L c)" |
16 lemma L_mono: "mono (L c)" |
17 proof- |
17 proof- |