Quelle Automata.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/IOA/Automata.thy
    Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
*)

section \<open>The I/O automata of Lynch and Tuttle in HOLCF\<close>

theory Automata
imports Asig
begin

default_sort type

type_synonym ('a, 's) transition = "'s \ 'a \ 's"
type_synonym ('a, 's) ioa =
  "'a signature \ 's set \ ('a, 's)transition set \ 'a set set \ 'a set set"

subsection \<open>IO automata\<close>

definition asig_of :: "('a, 's) ioa \ 'a signature"
  where "asig_of = fst"

definition starts_of :: "('a, 's) ioa \ 's set"
  where "starts_of = fst \ snd"

definition trans_of :: "('a, 's) ioa \ ('a, 's) transition set"
  where "trans_of = fst \ snd \ snd"

abbreviation trans_of_syn  (\<open>_ \<midarrow>_\<midarrow>_\<rightarrow> _\<close> [81, 81, 81, 81] 100)
  where "s \a\A\ t \ (s, a, t) \ trans_of A"

definition wfair_of :: "('a, 's) ioa \ 'a set set"
  where "wfair_of = fst \ snd \ snd \ snd"

definition sfair_of :: "('a, 's) ioa \ 'a set set"
  where "sfair_of = snd \ snd \ snd \ snd"

definition is_asig_of :: "('a, 's) ioa \ bool"
  where "is_asig_of A = is_asig (asig_of A)"

definition is_starts_of :: "('a, 's) ioa \ bool"
  where "is_starts_of A \ starts_of A \ {}"

definition is_trans_of :: "('a, 's) ioa \ bool"
  where "is_trans_of A \
    (\<forall>triple. triple \<in> trans_of A \<longrightarrow> fst (snd triple) \<in> actions (asig_of A))"

definition input_enabled :: "('a, 's) ioa \ bool"
  where "input_enabled A \
    (\<forall>a. a \<in> inputs (asig_of A) \<longrightarrow> (\<forall>s1. \<exists>s2. (s1, a, s2) \<in> trans_of A))"

definition IOA :: "('a, 's) ioa \ bool"
  where "IOA A \
    is_asig_of A \<and>
    is_starts_of A \<and>
    is_trans_of A \<and>
    input_enabled A"

abbreviation "act A \ actions (asig_of A)"
abbreviation "ext A \ externals (asig_of A)"
abbreviation int where "int A \ internals (asig_of A)"
abbreviation "inp A \ inputs (asig_of A)"
abbreviation "out A \ outputs (asig_of A)"
abbreviation "local A \ locals (asig_of A)"

text \<open>invariants\<close>

inductive reachable :: "('a, 's) ioa \ 's \ bool" for C :: "('a, 's) ioa"
where
  reachable_0:  "s \ starts_of C \ reachable C s"
| reachable_n:  "reachable C s \ (s, a, t) \ trans_of C \ reachable C t"

definition invariant :: "[('a, 's) ioa, 's \ bool] \ bool"
  where "invariant A P \ (\s. reachable A s \ P s)"

subsection \<open>Parallel composition\<close>

subsubsection \<open>Binary composition of action signatures and automata\<close>

definition compatible :: "('a, 's) ioa \ ('a, 't) ioa \ bool"
  where "compatible A B \
    out A \<inter> out B = {} \<and>
    int A \<inter> act B = {} \<and>
    int B \<inter> act A = {}"

definition asig_comp :: "'a signature \ 'a signature \ 'a signature"
  where "asig_comp a1 a2 =
     (((inputs a1 \<union> inputs a2) - (outputs a1 \<union> outputs a2),
       (outputs a1 \<union> outputs a2),
       (internals a1 \<union> internals a2)))"

definition par :: "('a, 's) ioa \ ('a, 't) ioa \ ('a, 's * 't) ioa" (infixr \\\ 10)
  where "(A \ B) =
    (asig_comp (asig_of A) (asig_of B),
     {pr. fst pr \<in> starts_of A \<and> snd pr \<in> starts_of B},
     {tr.
        let
          s = fst tr;
          a = fst (snd tr);
          t = snd (snd tr)
        in
          (a \<in> act A \<or> a \<in> act B) \<and>
          (if a \<in> act A then (fst s, a, fst t) \<in> trans_of A
           else fst t = fst s) \<and>
          (if a \<in> act B then (snd s, a, snd t) \<in> trans_of B
           else snd t = snd s)},
      wfair_of A \<union> wfair_of B,
      sfair_of A \<union> sfair_of B)"

subsection \<open>Hiding\<close>

subsubsection \<open>Hiding and restricting\<close>

definition restrict_asig :: "'a signature \ 'a set \ 'a signature"
  where "restrict_asig asig actns =
    (inputs asig \<inter> actns,
     outputs asig \<inter> actns,
     internals asig \<union> (externals asig - actns))"

text \<open>
  Notice that for \<open>wfair_of\<close> and \<open>sfair_of\<close> nothing has to be changed, as
  changes from the outputs to the internals does not touch the locals as a
  whole, which is of importance for fairness only.
\<close>
definition restrict :: "('a, 's) ioa \ 'a set \ ('a, 's) ioa"
  where "restrict A actns =
    (restrict_asig (asig_of A) actns,
     starts_of A,
     trans_of A,
     wfair_of A,
     sfair_of A)"

definition hide_asig :: "'a signature \ 'a set \ 'a signature"
  where "hide_asig asig actns =
    (inputs asig - actns,
     outputs asig - actns,
     internals asig \<union> actns)"

definition hide :: "('a, 's) ioa \ 'a set \ ('a, 's) ioa"
  where "hide A actns =
    (hide_asig (asig_of A) actns,
     starts_of A,
     trans_of A,
     wfair_of A,
     sfair_of A)"

subsection \<open>Renaming\<close>

definition rename_set :: "'a set \ ('c \ 'a option) \ 'c set"
  where "rename_set A ren = {b. \x. Some x = ren b \ x \ A}"

definition rename :: "('a, 'b) ioa \ ('c \ 'a option) \ ('c, 'b) ioa"
  where "rename ioa ren =
    ((rename_set (inp ioa) ren,
      rename_set (out ioa) ren,
      rename_set (int ioa) ren),
     starts_of ioa,
     {tr.
        let
          s = fst tr;
          a = fst (snd tr);
          t = snd (snd tr)
        in \<exists>x. Some x = ren a \<and> s \<midarrow>x\<midarrow>ioa\<rightarrow> t},
     {rename_set s ren | s. s \<in> wfair_of ioa},
     {rename_set s ren | s. s \<in> sfair_of ioa})"

subsection \<open>Fairness\<close>

subsubsection \<open>Enabledness of actions and action sets\<close>

definition enabled :: "('a, 's) ioa \ 'a \ 's \ bool"
  where "enabled A a s \ (\t. s \a\A\ t)"

definition Enabled :: "('a, 's) ioa \ 'a set \ 's \ bool"
  where "Enabled A W s \ (\w \ W. enabled A w s)"

text \<open>Action set keeps enabled until probably disabled by itself.\<close>

definition en_persistent :: "('a, 's) ioa \ 'a set \ bool"
  where "en_persistent A W \
    (\<forall>s a t. Enabled A W s \<and> a \<notin> W \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)"

text \<open>Post conditions for actions and action sets.\<close>

definition was_enabled :: "('a, 's) ioa \ 'a \ 's \ bool"
  where "was_enabled A a t \ (\s. s \a\A\ t)"

definition set_was_enabled :: "('a, 's) ioa \ 'a set \ 's \ bool"
  where "set_was_enabled A W t \ (\w \ W. was_enabled A w t)"

text \<open>Constraints for fair IOA.\<close>

definition fairIOA :: "('a, 's) ioa \ bool"
  where "fairIOA A \ (\S \ wfair_of A. S \ local A) \ (\S \ sfair_of A. S \ local A)"

definition input_resistant :: "('a, 's) ioa \ bool"
  where "input_resistant A \
    (\<forall>W \<in> sfair_of A. \<forall>s a t.
      reachable A s \<and> reachable A t \<and> a \<in> inp A \<and>
      Enabled A W s \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)"

declare split_paired_Ex [simp del]

lemmas ioa_projections = asig_of_def starts_of_def trans_of_def wfair_of_def sfair_of_def

subsection "\asig_of\, \starts_of\, \trans_of\"

lemma ioa_triple_proj:
  "asig_of (x, y, z, w, s) = x \
   starts_of (x, y, z, w, s) = y \<and>
   trans_of (x, y, z, w, s) = z \<and>
   wfair_of (x, y, z, w, s) = w \<and>
   sfair_of (x, y, z, w, s) = s"
  by (simp add: ioa_projections)

lemma trans_in_actions: "is_trans_of A \ s1 \a\A\ s2 \ a \ act A"
  by (auto simp add: is_trans_of_def actions_def is_asig_def)

lemma starts_of_par: "starts_of (A \ B) = {p. fst p \ starts_of A \ snd p \ starts_of B}"
  by (simp add: par_def ioa_projections)

lemma trans_of_par:
  "trans_of(A \ B) =
    {tr.
      let
        s = fst tr;
        a = fst (snd tr);
        t = snd (snd tr)
      in
        (a \<in> act A \<or> a \<in> act B) \<and>
        (if a \<in> act A then (fst s, a, fst t) \<in> trans_of A
         else fst t = fst s) \<and>
        (if a \<in> act B then (snd s, a, snd t) \<in> trans_of B
         else snd t = snd s)}"
  by (simp add: par_def ioa_projections)

subsection \<open>\<open>actions\<close> and \<open>par\<close>\<close>

lemma actions_asig_comp: "actions (asig_comp a b) = actions a \ actions b"
  by (auto simp add: actions_def asig_comp_def asig_projections)

lemma asig_of_par: "asig_of(A \ B) = asig_comp (asig_of A) (asig_of B)"
  by (simp add: par_def ioa_projections)

lemma externals_of_par: "ext (A1 \ A2) = ext A1 \ ext A2"
  by (auto simp add: externals_def asig_of_par asig_comp_def
    asig_inputs_def asig_outputs_def Un_def set_diff_eq)

lemma actions_of_par: "act (A1 \ A2) = act A1 \ act A2"
  by (auto simp add: actions_def asig_of_par asig_comp_def
    asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)

lemma inputs_of_par: "inp (A1 \ A2) = (inp A1 \ inp A2) - (out A1 \ out A2)"
  by (simp add: actions_def asig_of_par asig_comp_def
    asig_inputs_def asig_outputs_def Un_def set_diff_eq)

lemma outputs_of_par: "out (A1 \ A2) = out A1 \ out A2"
  by (simp add: actions_def asig_of_par asig_comp_def
    asig_outputs_def Un_def set_diff_eq)

lemma internals_of_par: "int (A1 \ A2) = int A1 \ int A2"
  by (simp add: actions_def asig_of_par asig_comp_def
    asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)

subsection \<open>Actions and compatibility\<close>

lemma compat_commute: "compatible A B = compatible B A"
  by (auto simp add: compatible_def Int_commute)

lemma ext1_is_not_int2: "compatible A1 A2 \ a \ ext A1 \ a \ int A2"
  by (auto simp add: externals_def actions_def compatible_def)

(*just commuting the previous one: better commute compatible*)
lemma ext2_is_not_int1: "compatible A2 A1 \ a \ ext A1 \ a \ int A2"
  by (auto simp add: externals_def actions_def compatible_def)

lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]

lemma intA_is_not_extB: "compatible A B \ x \ int A \ x \ ext B"
  by (auto simp add: externals_def actions_def compatible_def)

lemma intA_is_not_actB: "compatible A B \ a \ int A \ a \ act B"
  by (auto simp add: externals_def actions_def compatible_def is_asig_def asig_of_def)

(*the only one that needs disjointness of outputs and of internals and _all_ acts*)
lemma outAactB_is_inpB: "compatible A B \ a \ out A \ a \ act B \ a \ inp B"
  by (auto simp add: asig_outputs_def asig_internals_def actions_def asig_inputs_def
      compatible_def is_asig_def asig_of_def)

(*needed for propagation of input_enabledness from A, B to A \<parallel> B*)
lemma inpAAactB_is_inpBoroutB:
  "compatible A B \ a \ inp A \ a \ act B \ a \ inp B \ a \ out B"
  by (auto simp add: asig_outputs_def asig_internals_def actions_def asig_inputs_def
      compatible_def is_asig_def asig_of_def)

subsection \<open>Input enabledness and par\<close>

(*ugly case distinctions. Heart of proof:
    1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
    2. inputs_of_par: outputs are no longer inputs of par. This is important here.*)
lemma input_enabled_par:
  "compatible A B \ input_enabled A \ input_enabled B \ input_enabled (A \ B)"
  apply (unfold input_enabled_def)
  apply (simp add: Let_def inputs_of_par trans_of_par)
  apply (tactic "safe_tac (Context.raw_transfer \<^theory> \<^theory_context>\Fun\)")
  apply (simp add: inp_is_act)
  prefer 2
  apply (simp add: inp_is_act)
  text \<open>\<open>a \<in> inp A\<close>\<close>
  apply (case_tac "a \ act B")
  text \<open>\<open>a \<in> inp B\<close>\<close>
  apply (erule_tac x = "a" in allE)
  apply simp
  apply (drule inpAAactB_is_inpBoroutB)
  apply assumption
  apply assumption
  apply (erule_tac x = "a" in allE)
  apply simp
  apply (erule_tac x = "aa" in allE)
  apply (erule_tac x = "b" in allE)
  apply (erule exE)
  apply (erule exE)
  apply (rule_tac x = "(s2, s2a)" in exI)
  apply (simp add: inp_is_act)
  text \<open>\<open>a \<notin> act B\<close>\<close>
  apply (simp add: inp_is_act)
  apply (erule_tac x = "a" in allE)
  apply simp
  apply (erule_tac x = "aa" in allE)
  apply (erule exE)
  apply (rule_tac x = " (s2,b) " in exI)
  apply simp

  text \<open>\<open>a \<in> inp B\<close>\<close>
  apply (case_tac "a \ act A")
  text \<open>\<open>a \<in> act A\<close>\<close>
  apply (erule_tac x = "a" in allE)
  apply (erule_tac x = "a" in allE)
  apply (simp add: inp_is_act)
  apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
  apply (drule inpAAactB_is_inpBoroutB)
  back
  apply assumption
  apply assumption
  apply simp
  apply (erule_tac x = "aa" in allE)
  apply (erule_tac x = "b" in allE)
  apply (erule exE)
  apply (erule exE)
  apply (rule_tac x = "(s2, s2a)" in exI)
  apply (simp add: inp_is_act)
  text \<open>\<open>a \<notin> act B\<close>\<close>
  apply (simp add: inp_is_act)
  apply (erule_tac x = "a" in allE)
  apply (erule_tac x = "a" in allE)
  apply simp
  apply (erule_tac x = "b" in allE)
  apply (erule exE)
  apply (rule_tac x = "(aa, s2)" in exI)
  apply simp
  done

subsection \<open>Invariants\<close>

lemma invariantI:
  assumes "\s. s \ starts_of A \ P s"
    and "\s t a. reachable A s \ P s \ (s, a, t) \ trans_of A \ P t"
  shows "invariant A P"
  using assms
  apply (unfold invariant_def)
  apply (rule allI)
  apply (rule impI)
  apply (rule_tac x = "s" in reachable.induct)
  apply assumption
  apply blast
  apply blast
  done

lemma invariantI1:
  assumes "\s. s \ starts_of A \ P s"
    and "\s t a. reachable A s \ P s \ (s, a, t) \ trans_of A \ P t"
  shows "invariant A P"
  using assms by (blast intro: invariantI)

lemma invariantE: "invariant A P \ reachable A s \ P s"
  unfolding invariant_def by blast

subsection \<open>\<open>restrict\<close>\<close>

lemmas reachable_0 = reachable.reachable_0
  and reachable_n = reachable.reachable_n

lemma cancel_restrict_a:
  "starts_of (restrict ioa acts) = starts_of ioa \
   trans_of (restrict ioa acts) = trans_of ioa"
  by (simp add: restrict_def ioa_projections)

lemma cancel_restrict_b: "reachable (restrict ioa acts) s = reachable ioa s"
  apply (rule iffI)
  apply (erule reachable.induct)
  apply (simp add: cancel_restrict_a reachable_0)
  apply (erule reachable_n)
  apply (simp add: cancel_restrict_a)
  text \<open>\<open>\<longleftarrow>\<close>\<close>
  apply (erule reachable.induct)
  apply (rule reachable_0)
  apply (simp add: cancel_restrict_a)
  apply (erule reachable_n)
  apply (simp add: cancel_restrict_a)
  done

lemma acts_restrict: "act (restrict A acts) = act A"
  by (auto simp add: actions_def asig_internals_def
    asig_outputs_def asig_inputs_def externals_def asig_of_def restrict_def restrict_asig_def)

lemma cancel_restrict:
  "starts_of (restrict ioa acts) = starts_of ioa \
   trans_of (restrict ioa acts) = trans_of ioa \<and>
   reachable (restrict ioa acts) s = reachable ioa s \<and>
   act (restrict A acts) = act A"
  by (simp add: cancel_restrict_a cancel_restrict_b acts_restrict)

subsection \<open>\<open>rename\<close>\<close>

lemma trans_rename: "s \a\(rename C f)\ t \ (\x. Some x = f a \ s \x\C\ t)"
  by (simp add: Let_def rename_def trans_of_def)

lemma reachable_rename: "reachable (rename C g) s \ reachable C s"
  apply (erule reachable.induct)
  apply (rule reachable_0)
  apply (simp add: rename_def ioa_projections)
  apply (drule trans_rename)
  apply (erule exE)
  apply (erule conjE)
  apply (erule reachable_n)
  apply assumption
  done

subsection \<open>\<open>trans_of (A \<parallel> B)\<close>\<close>

lemma trans_A_proj:
  "(s, a, t) \ trans_of (A \ B) \ a \ act A \ (fst s, a, fst t) \ trans_of A"
  by (simp add: Let_def par_def trans_of_def)

lemma trans_B_proj:
  "(s, a, t) \ trans_of (A \ B) \ a \ act B \ (snd s, a, snd t) \ trans_of B"
  by (simp add: Let_def par_def trans_of_def)

lemma trans_A_proj2: "(s, a, t) \ trans_of (A \ B) \ a \ act A \ fst s = fst t"
  by (simp add: Let_def par_def trans_of_def)

lemma trans_B_proj2: "(s, a, t) \ trans_of (A \ B) \ a \ act B \ snd s = snd t"
  by (simp add: Let_def par_def trans_of_def)

lemma trans_AB_proj: "(s, a, t) \ trans_of (A \ B) \ a \ act A \ a \ act B"
  by (simp add: Let_def par_def trans_of_def)

lemma trans_AB:
  "a \ act A \ a \ act B \
  (fst s, a, fst t) \<in> trans_of A \<Longrightarrow>
  (snd s, a, snd t) \<in> trans_of B \<Longrightarrow>
  (s, a, t) \<in> trans_of (A \<parallel> B)"
  by (simp add: Let_def par_def trans_of_def)

lemma trans_A_notB:
  "a \ act A \ a \ act B \
  (fst s, a, fst t) \<in> trans_of A \<Longrightarrow>
  snd s = snd t \<Longrightarrow>
  (s, a, t) \<in> trans_of (A \<parallel> B)"
  by (simp add: Let_def par_def trans_of_def)

lemma trans_notA_B:
  "a \ act A \ a \ act B \
  (snd s, a, snd t) \<in> trans_of B \<Longrightarrow>
  fst s = fst t \<Longrightarrow>
  (s, a, t) \<in> trans_of (A \<parallel> B)"
  by (simp add: Let_def par_def trans_of_def)

lemmas trans_of_defs1 = trans_AB trans_A_notB trans_notA_B
  and trans_of_defs2 = trans_A_proj trans_B_proj trans_A_proj2 trans_B_proj2 trans_AB_proj

lemma trans_of_par4:
  "(s, a, t) \ trans_of (A \ B \ C \ D) \
    ((a \<in> actions (asig_of A) \<or> a \<in> actions (asig_of B) \<or> a \<in> actions (asig_of C) \<or>
      a \<in> actions (asig_of D)) \<and>
     (if a \<in> actions (asig_of A)
      then (fst s, a, fst t) \<in> trans_of A
      else fst t = fst s) \<and>
     (if a \<in> actions (asig_of B)
      then (fst (snd s), a, fst (snd t)) \<in> trans_of B
      else fst (snd t) = fst (snd s)) \<and>
     (if a \<in> actions (asig_of C)
      then (fst (snd (snd s)), a, fst (snd (snd t))) \<in> trans_of C
      else fst (snd (snd t)) = fst (snd (snd s))) \<and>
     (if a \<in> actions (asig_of D)
      then (snd (snd (snd s)), a, snd (snd (snd t))) \<in> trans_of D
      else snd (snd (snd t)) = snd (snd (snd s))))"
  by (simp add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)

subsection \<open>Proof obligation generator for IOA requirements\<close>

(*without assumptions on A and B because is_trans_of is also incorporated in par_def*)
lemma is_trans_of_par: "is_trans_of (A \ B)"
  by (simp add: is_trans_of_def Let_def actions_of_par trans_of_par)

lemma is_trans_of_restrict: "is_trans_of A \ is_trans_of (restrict A acts)"
  by (simp add: is_trans_of_def cancel_restrict acts_restrict)

lemma is_trans_of_rename: "is_trans_of A \ is_trans_of (rename A f)"
  apply (unfold is_trans_of_def restrict_def restrict_asig_def)
  apply (simp add: Let_def actions_def trans_of_def asig_internals_def
    asig_outputs_def asig_inputs_def externals_def asig_of_def rename_def rename_set_def)
  apply blast
  done

lemma is_asig_of_par: "is_asig_of A \ is_asig_of B \ compatible A B \ is_asig_of (A \ B)"
  apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def
    asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def)
  apply (simp add: asig_of_def)
  apply auto
  done

lemma is_asig_of_restrict: "is_asig_of A \ is_asig_of (restrict A f)"
  apply (unfold is_asig_of_def is_asig_def asig_of_def restrict_def restrict_asig_def
    asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def)
  apply simp
  apply auto
  done

lemma is_asig_of_rename: "is_asig_of A \ is_asig_of (rename A f)"
  apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def
    asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def)
  apply auto
  apply (drule_tac [!] s = "Some _" in sym)
  apply auto
  done

lemmas [simp] = is_asig_of_par is_asig_of_restrict
  is_asig_of_rename is_trans_of_par is_trans_of_restrict is_trans_of_rename

lemma compatible_par: "compatible A B \ compatible A C \ compatible A (B \ C)"
  by (auto simp add: compatible_def internals_of_par outputs_of_par actions_of_par)

(*better derive by previous one and compat_commute*)
lemma compatible_par2: "compatible A C \ compatible B C \ compatible (A \ B) C"
  by (auto simp add: compatible_def internals_of_par outputs_of_par actions_of_par)

lemma compatible_restrict:
  "compatible A B \ (ext B - S) \ ext A = {} \ compatible A (restrict B S)"
  by (auto simp add: compatible_def ioa_triple_proj asig_triple_proj externals_def
    restrict_def restrict_asig_def actions_def)

declare split_paired_Ex [simp]

end

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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 ist noch experimentell.