chapter ‹ The Owicki-Gries Method› section ‹ Abstract Syntax› theory OG_Com imports Main begin text ‹ Type abbreviations for boolean expressions and assertions:› type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" text ‹ The syntax of commands is defined by two mutually recursive datatypes: ‹ 'a ann_com› for annotated commands and ‹ 'a com › datatype 'a ann_com = AnnBasic "('a assn)" "('a ==> | AnnSeq "('a ann_com)" "('a ann_com)" | AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)" | AnnCond2 "('a assn)" "('a bexp)" "('a ann_com)" | AnnWhile "('a assn)" "('a bexp)" "('a assn)" "('a ann_com)" | AnnAwait "('a assn)" "('a bexp)" "('a com)" and 'a com = Parallel "('a ann_com option × 'a assn) list" | Basic "('a ==> | Seq "('a com)" "('a com)" | Cond "('a bexp)" "('a com)" "('a com)" | While "('a bexp)" "('a assn)" "('a com)" text ‹ The function ‹ pre› extracts the precondition of an annotated command: › primrec pre ::"'a ann_com ==> "pre (AnnBasic r f) = r" | "pre (AnnSeq c1 c2) = pre c1" | "pre (AnnCond1 r b c1 c2) = r" | "pre (AnnCond2 r b c) = r" | "pre (AnnWhile r b i c) = r" | "pre (AnnAwait r b c) = r" text ‹ Well-formedness predicate for atomic programs:› primrec atom_com :: "'a com ==> "atom_com (Parallel Ts) = False" | "atom_com (Basic f) = True" | "atom_com (Seq c1 c2) = (atom_com c1 ∧ atom_com c2)" | "atom_com (Cond b c1 c2) = (atom_com c1 ∧ atom_com c2)" | "atom_com (While b i c) = atom_com c" end
Messung V0.5 in Prozent C=6 H=100 G=70
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-04-29)
¤ *© Formatika GbR, Deutschland
