equal
deleted
inserted
replaced
1 theory Def_Ass imports Vars Com |
1 theory Def_Ass imports Vars Com |
2 begin |
2 begin |
3 |
3 |
4 subsection "Definite Assignment Analysis" |
4 subsection "Definite Assignment Analysis" |
5 |
5 |
6 inductive D :: "name set \<Rightarrow> com \<Rightarrow> name set \<Rightarrow> bool" where |
6 inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where |
7 Skip: "D A SKIP A" | |
7 Skip: "D A SKIP A" | |
8 Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" | |
8 Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" | |
9 Semi: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2; D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" | |
9 Semi: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2; D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" | |
10 If: "\<lbrakk> vars b \<subseteq> A; D A c\<^isub>1 A\<^isub>1; D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow> |
10 If: "\<lbrakk> vars b \<subseteq> A; D A c\<^isub>1 A\<^isub>1; D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow> |
11 D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" | |
11 D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" | |