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🪙1 c🪙1 A🪙2; D A🪙2 c🪙2 A🪙3 ]==> D A🪙1 (c🪙1;; c🪙2) A🪙3" | If: "[ vars b ⊆ A; D A c🪙1 A🪙1; D A c🪙2 A🪙2 ]==> D A (IF b THEN c🪙1 ELSE c🪙2) (A🪙1 Int A🪙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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet am 2026-04-28)
¤
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.
