equal
deleted
inserted
replaced
5 subsection "Definite Initialization Analysis" |
5 subsection "Definite Initialization Analysis" |
6 |
6 |
7 inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where |
7 inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where |
8 Skip: "D A SKIP A" | |
8 Skip: "D A SKIP A" | |
9 Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" | |
9 Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" | |
10 Seq: "\<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 Seq: "\<lbrakk> D A\<^sub>1 c\<^sub>1 A\<^sub>2; D A\<^sub>2 c\<^sub>2 A\<^sub>3 \<rbrakk> \<Longrightarrow> D A\<^sub>1 (c\<^sub>1;; c\<^sub>2) A\<^sub>3" | |
11 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 If: "\<lbrakk> vars b \<subseteq> A; D A c\<^sub>1 A\<^sub>1; D A c\<^sub>2 A\<^sub>2 \<rbrakk> \<Longrightarrow> |
12 D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" | |
12 D A (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (A\<^sub>1 Int A\<^sub>2)" | |
13 While: "\<lbrakk> vars b \<subseteq> A; D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A" |
13 While: "\<lbrakk> vars b \<subseteq> A; D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A" |
14 |
14 |
15 inductive_cases [elim!]: |
15 inductive_cases [elim!]: |
16 "D A SKIP A'" |
16 "D A SKIP A'" |
17 "D A (x ::= a) A'" |
17 "D A (x ::= a) A'" |