no message
This commit is contained in:
parent
436d41d232
commit
c752a25dd6
16
Isa_DOF.thy
16
Isa_DOF.thy
|
@ -1511,7 +1511,9 @@ end\<close>
|
|||
|
||||
|
||||
section\<open> Syntax for Ontological Antiquotations (the '' View'' Part II) \<close>
|
||||
|
||||
|
||||
text\<open> @{theory Main}\<close>
|
||||
|
||||
ML\<open>
|
||||
structure OntoLinkParser =
|
||||
struct
|
||||
|
@ -1555,6 +1557,16 @@ fun docitem_antiquotation_generic cid_decl
|
|||
{context = ctxt, source = src:Token.src, state}
|
||||
({unchecked = x, define= y}, source:Input.source) =
|
||||
let fun label_latex flag = enclose (if flag then "\\label{" else "\\autoref{") "}"
|
||||
val X1 = Thy_Output.output_text state {markdown=false}
|
||||
: Input.source -> string
|
||||
val X2 = check_and_mark ctxt
|
||||
cid_decl
|
||||
({strict_checking = not x})
|
||||
(Input.pos_of source)
|
||||
: string -> string
|
||||
val X3 = label_latex y
|
||||
: string -> string
|
||||
|
||||
in
|
||||
(Thy_Output.output_text state {markdown=false} #>
|
||||
check_and_mark ctxt
|
||||
|
@ -1811,4 +1823,6 @@ val _ =
|
|||
end (* struct *)
|
||||
\<close>
|
||||
|
||||
ML\<open>Thy_Output.document_command; Thy_Output.output_text\<close>
|
||||
|
||||
end
|
||||
|
|
|
@ -28,6 +28,8 @@ Safety assessment is focused on but not limited to the safety properties of a sy
|
|||
Definition*[assessor::concept, tag="''assessor''"]
|
||||
\<open>entity that carries out an assessment\<close>
|
||||
|
||||
text\<open>@{docitem \<open>assessment\<close>}\<close>
|
||||
|
||||
Definition*[COTS::concept, tag="''commercial off-the-shelf software''"]
|
||||
\<open>software defined by market-driven need, commercially available and whose fitness for purpose
|
||||
has been demonstrated by a broad spectrum of commercial users\<close>
|
||||
|
@ -71,7 +73,7 @@ from the intended performance or behaviour (cf @{concept \<open>error\<close>})\
|
|||
Definition*[failure::concept]
|
||||
\<open>unacceptable difference between required and observed performance\<close>
|
||||
|
||||
Definition*[FT::concept, tag="''fault tolerance''"]
|
||||
Definition*[FT::concept, tag="\<open>fault tolerance\<close>"]
|
||||
\<open>built-in capability of a system to provide continued correct provision of service as specified,
|
||||
in the presence of a limited number of hardware or software faults\<close>
|
||||
|
||||
|
@ -260,6 +262,16 @@ datatype phase = SYSDEV_ext (* System Development Phase (external) *)
|
|||
| SD (* Software Deployment *)
|
||||
| SM (* Software Maintenance *)
|
||||
|
||||
datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
||||
|
||||
type_synonym saftety_integraytion_level = sil
|
||||
|
||||
doc_class cenelec_text = text_element +
|
||||
phase :: "phase"
|
||||
sil :: sil
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
|
||||
|
||||
abbreviation software_requirement :: "phase" where "software_requirement \<equiv> SR"
|
||||
abbreviation software_architecture :: "phase" where "software_architecture \<equiv> SA"
|
||||
abbreviation software_design :: "phase" where "software_design \<equiv> SD"
|
||||
|
@ -276,9 +288,6 @@ term "SR" (* meta-test *)
|
|||
|
||||
section\<open>Objectives, Conformance and Software Integrity Levels\<close>
|
||||
|
||||
datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
||||
|
||||
type_synonym saftety_integraytion_level = sil
|
||||
|
||||
|
||||
doc_class objectives =
|
||||
|
@ -286,7 +295,7 @@ doc_class objectives =
|
|||
is_concerned :: "role set"
|
||||
|
||||
|
||||
doc_class requirement = text_element +
|
||||
doc_class requirement = cenelec_text +
|
||||
long_name :: "string option"
|
||||
is_concerned :: "role set"
|
||||
|
||||
|
@ -450,11 +459,6 @@ doc_class judgement =
|
|||
|
||||
section\<open> Design and Test Documents \<close>
|
||||
|
||||
doc_class cenelec_text = text_element +
|
||||
phase :: "phase"
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
|
||||
|
||||
|
||||
doc_class SYSREQS = cenelec_text +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
|
|
Loading…
Reference in New Issue