| products/Sources/formale Sprachen/Isabelle/HOL/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 13 kB |
|
Quellcode-Bibliothek OG_Com.thySprache: Isabelle |
|||||||||||||||
|
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 ==> '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 ==> '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 ==> 'a assn" where "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 ==> bool" where "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
¤ 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.0.15Bemerkung: (vorverarbeitet am 2026-04-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26