intermediate session with Macro-Bug.
This commit is contained in:
parent
efeee1e863
commit
698da3dd24
|
@ -443,13 +443,13 @@ integrated source, we will, in the following, point out three scenarios.\<close>
|
||||||
|
|
||||||
subsection\<open>Internal Verification of Claims in the Requirements Specification.\<close>
|
subsection\<open>Internal Verification of Claims in the Requirements Specification.\<close>
|
||||||
text\<open>In our case, the SR-team early on detected a property necessary
|
text\<open>In our case, the SR-team early on detected a property necessary
|
||||||
for error-detection of the device (c.f. @{docitem verific}):
|
for error-detection of the device (c.f. @{technical verific}):
|
||||||
\enlargethispage{2\baselineskip}\begin{isar}
|
\enlargethispage{2\baselineskip}\begin{isar}
|
||||||
text*[encoder_props::requirement]<open> The requirement specification team ...
|
text*[encoder_props::requirement]<open> The requirement specification team ...
|
||||||
C1 & C2 & C3 = 0 (bitwise logical AND operation)
|
C1 & C2 & C3 = 0 (bitwise logical AND operation)
|
||||||
C1 | C2 | C3 = 1 (bitwise logical OR operation) <close>
|
C1 | C2 | C3 = 1 (bitwise logical OR operation) <close>
|
||||||
\end{isar}
|
\end{isar}
|
||||||
After the Isabelle proofs shown in @{docitem verific}, we can either register the theorems
|
After the Isabelle proofs shown in @{technical verific}, we can either register the theorems
|
||||||
directly in an evidence statement:
|
directly in an evidence statement:
|
||||||
|
|
||||||
\begin{isar}
|
\begin{isar}
|
||||||
|
@ -562,13 +562,19 @@ to a test-environment or test-engine. \<close>
|
||||||
|
|
||||||
text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared
|
text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared
|
||||||
meta-information and status. \<close>
|
meta-information and status. \<close>
|
||||||
text \<open> As established by @{docitem (unchecked) \<open>t10\<close>},
|
text \<open> As established by @{test_result (unchecked) \<open>t10\<close>},
|
||||||
@{docitem (define) \<open>t10\<close>} \<close>
|
@{test_result (define) \<open>t10\<close>} \<close>
|
||||||
text \<open> the @{docitem \<open>t10\<close>}
|
text \<open> the @{test_result \<open>t10\<close>}
|
||||||
as well as the @{docitem \<open>ass122\<close>}\<close>
|
as well as the @{SRAC \<open>ass122\<close>}\<close>
|
||||||
text \<open> represent a justification of the safety related applicability
|
text \<open> represent a justification of the safety related applicability
|
||||||
condition @{SRAC \<open>ass122\<close>} aka exported constraint @{EC \<open>ass122\<close>}.\<close>
|
condition @{SRAC \<open>ass122\<close>} aka exported constraint @{EC \<open>ass122\<close>}.\<close>
|
||||||
|
|
||||||
|
(* due to notational conventions for antiquotations, one may even write: *)
|
||||||
|
(* CRASHES WITH LaTeX backend error. *)
|
||||||
|
text \<open> represent a justification of the safety related applicability
|
||||||
|
condition \<^SRAC>\<open>ass122\<close> aka exported constraint \<^EC>\<open>ass122\<close>.\<close>
|
||||||
|
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
end
|
end
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
|
@ -527,16 +527,16 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
|
||||||
%Note that we do not redefine \<open>RUN\<close> with \<open>SKIP\<close> because this process is supposed to never terminate,
|
%Note that we do not redefine \<open>RUN\<close> with \<open>SKIP\<close> because this process is supposed to never terminate,
|
||||||
%thus must be without it.
|
%thus must be without it.
|
||||||
\<close>
|
\<close>
|
||||||
(*
|
|
||||||
Definition*[X22]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
text*[X22::"definition"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
||||||
Definition*[X32]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
text*[X32::"definition"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||||
Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<^vs>\<open>-0.7cm\<close>\<close>
|
Definition*[X42::"definition"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<close>
|
||||||
|
|
||||||
text\<open> The \<open>RUN\<close>-process defined @{definition X22} represents the process that accepts all
|
text\<open> The \<open>RUN\<close>-process defined @{definition X22} represents the process that accepts all
|
||||||
events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in
|
events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in
|
||||||
@{definition X32} and @{definition X42}: the process that non-deterministically stops or
|
@{definition X32} and @{definition X42}: the process that non-deterministically stops or
|
||||||
accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close>
|
accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close>
|
||||||
*)
|
|
||||||
|
|
||||||
Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||||
Definition*[X3]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
Definition*[X3]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||||
|
|
Loading…
Reference in New Issue