|
theory Def_Init
imports Vars Com
begin
subsection "Definite Initialization Analysis"
inductive D :: "vname set \ com \ vname set \ bool" where
Skip: "D A SKIP A" |
Assign: "vars a \ A \ D A (x ::= a) (insert x A)" |
Seq: "\ D A\<^sub>1 c\<^sub>1 A\<^sub>2; D A\<^sub>2 c\<^sub>2 A\<^sub>3 \ \ D A\<^sub>1 (c\<^sub>1;; c\<^sub>2) A\<^sub>3" |
If: "\ vars b \ A; D A c\<^sub>1 A\<^sub>1; D A c\<^sub>2 A\<^sub>2 \ \
D A (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (A\<^sub>1 Int A\<^sub>2)" |
While: "\ vars b \ A; D A c A' \ \ D A (WHILE b DO c) A"
inductive_cases [elim!]:
"D A SKIP A'"
"D A (x ::= a) A'"
"D A (c1;;c2) A'"
"D A (IF b THEN c1 ELSE c2) A'"
"D A (WHILE b DO c) A'"
lemma D_incr:
"D A c A' \ A \ A'"
by (induct rule: D.induct) auto
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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 ist noch experimentell.
|
