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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-29)
¤
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 und die Messung sind noch experimentell.
