| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/IMP/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 961 B |
|
Quelle Def_Init.thySprache: Isabelle |
|||||||||||||||
|
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 A1 c1 A2; D A2 c2 A3 ] ==> D A1 (c1;; c2) A3" | If: "[ vars b ⊆ A; D A c1 A1; D A c2 A2 ] ==> D A (IF b THEN c1 ELSE c2) (A1 Int A2)" | 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.10 Sekunden (vorverarbeitet am 2026-06-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09