- added support for formal text statements Definition*, Lemma*, Theorem*, Conjecture*
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
HOL-OCL/Isabelle_DOF/master There was a failure building this commit
Details
- added lemma* theorem* corrolary* refering to Isar std commands, but ignoring the meta-args. - Text-exercise: Improved the "Terms and Definitions" section Darstellung in der Ontologie durch verwendung von Definition*.
This commit is contained in:
parent
65346b3f0a
commit
cd6e82949f
|
@ -62,8 +62,9 @@ doc_class formal_content =
|
|||
accepts "\<lbrace>formal_item\<rbrace>\<^sup>+"
|
||||
|
||||
|
||||
|
||||
|
||||
doc_class concept =
|
||||
tag :: "string" <= "''''"
|
||||
properties :: "thm list"
|
||||
|
||||
section\<open>Tests\<close>
|
||||
|
||||
|
|
102
Isa_DOF.thy
102
Isa_DOF.thy
|
@ -28,12 +28,15 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
|||
"text*"
|
||||
"figure*"
|
||||
"side_by_side_figure*"
|
||||
"Definition*" "Lemma*" "Theorem*" "Conjecture*"
|
||||
:: document_body
|
||||
|
||||
and "open_monitor*" "close_monitor*" "declare_reference*"
|
||||
"update_instance*" "doc_class" ::thy_decl
|
||||
|
||||
and "lemma*" "theorem*" "assert*" ::thy_decl
|
||||
and (* "definition*" *) "corrollary*" "proposition*" "schematic_goal*"
|
||||
"lemma*" "theorem*" (* -- intended replacement of Isar std commands.*)
|
||||
"assert*" ::thy_decl
|
||||
|
||||
and "print_doc_classes" "print_doc_items" "gen_sty_template" "check_doc_global" :: diag
|
||||
|
||||
|
@ -1081,7 +1084,9 @@ fun update_instance_command (((oid:string,pos),cid_pos),
|
|||
end
|
||||
|
||||
|
||||
fun enriched_document_command markdown level (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
|
||||
fun gen_enriched_document_command transform
|
||||
markdown
|
||||
(((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
|
||||
xstring_opt:(xstring * Position.T) option),
|
||||
toks:Input.source)
|
||||
: theory -> theory =
|
||||
|
@ -1089,14 +1094,22 @@ fun enriched_document_command markdown level (((((oid,pos),cid_pos), doc_attrs)
|
|||
(* as side-effect, generates markup *)
|
||||
fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy)
|
||||
(* generating the level-attribute syntax *)
|
||||
val doc_attrs' = case level of
|
||||
in
|
||||
(create_and_check_docitem false oid pos cid_pos (transform doc_attrs) #> check_text)
|
||||
(* Thanks Frederic Tuong! ! ! *)
|
||||
end;
|
||||
|
||||
fun enriched_document_command level =
|
||||
let fun transform doc_attrs = case level of
|
||||
NONE => doc_attrs
|
||||
| SOME(NONE) => (("level",@{here}),"None")::doc_attrs
|
||||
| SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs
|
||||
in
|
||||
(create_and_check_docitem false oid pos cid_pos doc_attrs' #> check_text)
|
||||
(* Thanks Frederic Tuong! ! ! *)
|
||||
end;
|
||||
in gen_enriched_document_command transform end;
|
||||
|
||||
fun enriched_formal_statement_command (tag:string) =
|
||||
let fun transform doc_attrs = (("tag",@{here}),"''"^tag^"''") ::
|
||||
(("properties",@{here}),"([]::thm list)")::doc_attrs
|
||||
in gen_enriched_document_command transform end;
|
||||
|
||||
|
||||
|
||||
|
@ -1143,63 +1156,90 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
|||
|> delete_monitor_entry
|
||||
end
|
||||
|
||||
(* *********************************************************************** *)
|
||||
(* Textual Command Support *)
|
||||
(* *********************************************************************** *)
|
||||
|
||||
(* {markdown = true} sets the parsing process such that in the text-core markdown elements are
|
||||
accepted. *)
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_formal_statement_command "definition" {markdown = true} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_formal_statement_command "lemma" {markdown = true} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_formal_statement_command "theorem" {markdown = true} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("Conjecture*", @{here}) "Textual Theorem Outline"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_formal_statement_command "conjecture" {markdown = true} )));
|
||||
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("title*", @{here}) "section heading"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} NONE))) ;
|
||||
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} ))) ;
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("subtitle*", @{here}) "section heading"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} NONE)));
|
||||
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("chapter*", @{here}) "section heading"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 0)))));
|
||||
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 0)) {markdown = false} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("section*", @{here}) "section heading"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 1)))));
|
||||
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 1)) {markdown = false} )));
|
||||
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 2)))));
|
||||
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 2)) {markdown = false} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 3)))));
|
||||
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 3)) {markdown = false} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 4)))));
|
||||
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 4)) {markdown = false} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 5)))));
|
||||
>> (Toplevel.theory o (enriched_document_command (SOME(SOME 5)) {markdown = false} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("figure*", @{here}) "figure"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} NONE)));
|
||||
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = false} NONE)));
|
||||
>> (Toplevel.theory o (enriched_document_command NONE {markdown = false} )));
|
||||
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source
|
||||
>> (Toplevel.theory o (enriched_document_command {markdown = true} (NONE))));
|
||||
>> (Toplevel.theory o (enriched_document_command NONE {markdown = true} )));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "declare_reference*"}
|
||||
|
@ -1223,12 +1263,6 @@ val _ =
|
|||
"update meta-attributes of an instance of a document class"
|
||||
(attributes_upd >> (Toplevel.theory o update_instance_command));
|
||||
|
||||
(* dummy/fake so far: *)
|
||||
val update_lemma_cmd = (fn (((oid,pos),cid),doc_attrs) => (Toplevel.theory (I)))
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "lemma*"}
|
||||
"lemma" (attributes >> update_lemma_cmd);
|
||||
|
||||
fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),some_name:string option),modes : string list),
|
||||
prop) =
|
||||
|
@ -1294,18 +1328,22 @@ val short_statement =
|
|||
|
||||
fun theorem spec schematic descr =
|
||||
Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
|
||||
((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) =>
|
||||
((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd )
|
||||
((ODL_Command_Parser.attributes -- (long_statement || short_statement))
|
||||
>> (fn (_ (* skip *) ,(long, binding, includes, elems, concl)) =>
|
||||
((if schematic then Specification.schematic_theorem_cmd
|
||||
else Specification.theorem_cmd )
|
||||
long Thm.theoremK NONE (K I) binding includes elems concl)));
|
||||
|
||||
in
|
||||
|
||||
(* Half - fake. activates original Isar commands, but skips meta-arguments for the moment. *)
|
||||
val _ = theorem @{command_keyword "theorem*"} false "theorem";
|
||||
(* val _ = theorem @{command_keyword "lemma*"} false "lemma";
|
||||
val _ = theorem @{command_keyword corollary} false "corollary";
|
||||
val _ = theorem @{command_keyword proposition} false "proposition";
|
||||
val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; *)
|
||||
val _ = theorem @{command_keyword "lemma*"} false "lemma";
|
||||
val _ = theorem @{command_keyword "corrollary*"} false "corollary";
|
||||
val _ = theorem @{command_keyword "proposition*"} false "proposition";
|
||||
val _ = theorem @{command_keyword "schematic_goal*"} true "schematic goal";
|
||||
|
||||
in end\<close>
|
||||
end\<close>
|
||||
|
||||
|
||||
section\<open> Syntax for Ontological Antiquotations (the '' View'' Part II) \<close>
|
||||
|
@ -1623,4 +1661,6 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []);
|
|||
\<close>
|
||||
*)
|
||||
|
||||
lemma X : "True" sorry
|
||||
|
||||
end
|
||||
|
|
|
@ -20,22 +20,21 @@ text\<open> Excerpt of the BE EN 50128:2011, page 22. \<close>
|
|||
|
||||
section\<open>Terms and Definitions\<close>
|
||||
|
||||
subsection\<open>assessment\<close>
|
||||
text\<open>process of analysis to determine whether software, which may include process, documentation,
|
||||
system, subsystem hardware and/or software components, meets the specified requirements and to form
|
||||
a judgement as to whether the software is fit for its intended purpose. Safety assessment is
|
||||
focused on but not limited to the safety properties of a system.\<close>
|
||||
Definition*[assessment::concept]\<open>process of analysis to determine whether software, which may include
|
||||
process, documentation, system, subsystem hardware and/or software components, meets the specified
|
||||
requirements and to form a judgement as to whether the software is fit for its intended purpose.
|
||||
Safety assessment is focused on but not limited to the safety properties of a system.\<close>
|
||||
|
||||
subsection\<open>assessor\<close>
|
||||
text\<open>entity that carries out an assessment\<close>
|
||||
Definition*[assessor::concept, tag="''assessor''"]
|
||||
\<open>entity that carries out an assessment\<close>
|
||||
|
||||
subsection\<open>commercial off-the-shelf (COTS) software\<close>
|
||||
text\<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>
|
||||
Definition*[cots::concept, tag="''commercial off-the-shelf (COTS) 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>
|
||||
|
||||
subsection\<open>component\<close>
|
||||
text\<open>a constituent part of software which has well-defined interfaces and behaviour
|
||||
|
||||
Definition*[component::concept]
|
||||
\<open>a constituent part of software which has well-defined interfaces and behaviour
|
||||
with respect to the software architecture and design and fulfils the following
|
||||
criteria:
|
||||
\<^enum> it is designed according to “Components” (see Table A.20);
|
||||
|
@ -45,112 +44,109 @@ criteria:
|
|||
(e. g. subsystems) which have an independent version
|
||||
\<close>
|
||||
|
||||
subsection\<open>configuration manager\<close>
|
||||
text\<open>entity that is responsible for implementing and carrying out the processes
|
||||
Definition*[cmgr::concept, tag="''configuration manager''"]
|
||||
\<open>entity that is responsible for implementing and carrying out the processes
|
||||
for the configuration management of documents, software and related tools including
|
||||
\<^emph>\<open>change management\<close>\<close>
|
||||
|
||||
subsection\<open>customer\<close>
|
||||
text\<open>entity which purchases a railway control and protection system including
|
||||
the software\<close>
|
||||
Definition*[customer::concept]
|
||||
\<open>entity which purchases a railway control and protection system including the software\<close>
|
||||
|
||||
subsection\<open>designer\<close>
|
||||
text\<open>entity that analyses and transforms specified requirements into acceptable design solutions
|
||||
Definition*[designer::concept]
|
||||
\<open>entity that analyses and transforms specified requirements into acceptable design solutions
|
||||
which have the required safety integrity level\<close>
|
||||
|
||||
subsection\<open>entity\<close>
|
||||
text\<open>person, group or organisation who fulfils a role as defined in this European
|
||||
Standard\<close>
|
||||
Definition*[entity::concept]
|
||||
\<open>person, group or organisation who fulfils a role as defined in this European Standard\<close>
|
||||
|
||||
subsection\<open>error, fault\<close>
|
||||
text\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
|
||||
from the intended performance or behaviour\<close>
|
||||
declare_reference*[fault::concept]
|
||||
Definition*[error::concept]
|
||||
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
|
||||
from the intended performance or behaviour (cf @{concept (unchecked) \<open>fault\<close>}))\<close>
|
||||
|
||||
subsection\<open>failure\<close>
|
||||
text\<open>unacceptable difference between required and observed performance\<close>
|
||||
Definition*[fault::concept]
|
||||
\<open>defect, mistake or inaccuracy which could result in failure or in a deviation
|
||||
from the intended performance or behaviour (cf @{concept \<open>error\<close>})\<close>
|
||||
|
||||
subsection\<open>fault tolerance\<close>
|
||||
text\<open>built-in capability of a system to provide continued correct provision of service as specified,
|
||||
Definition*[failure::concept]
|
||||
\<open>unacceptable difference between required and observed performance\<close>
|
||||
|
||||
Definition*[ft::concept, tag="''fault tolerance''"]
|
||||
\<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>
|
||||
|
||||
subsection\<open>firmware\<close>
|
||||
text\<open>software stored in read-only memory or in semi-permanent storage such as flash memory, in a
|
||||
Definition*[firmware::concept]
|
||||
\<open>software stored in read-only memory or in semi-permanent storage such as flash memory, in a
|
||||
way that is functionally independent of applicative software\<close>
|
||||
|
||||
subsection\<open>generic software\<close>
|
||||
text\<open>software which can be usedfor a variety of installations purely by the provision of
|
||||
Definition*[gen_soft::concept,tag="''generic software''"]
|
||||
\<open>software which can be used for a variety of installations purely by the provision of
|
||||
application-specific data and/or algorithms\<close>
|
||||
|
||||
subsection\<open>implementer\<close>
|
||||
text\<open>entity that transforms specified designs into their physical realisation\<close>
|
||||
Definition*[implementer::concept]
|
||||
\<open>entity that transforms specified designs into their physical realisation\<close>
|
||||
|
||||
subsection\<open>integration\<close>
|
||||
text\<open>process of assembling software and/or hardware items, according to the architectural and
|
||||
design specification, and testing the integrated unit
|
||||
\<close>
|
||||
Definition*[integration::concept]
|
||||
\<open>process of assembling software and/or hardware items, according to the architectural and
|
||||
design specification, and testing the integrated unit\<close>
|
||||
|
||||
subsection\<open>integrator\<close>
|
||||
text\<open>entity that carries out software integration\<close>
|
||||
Definition*[integrator::concept]
|
||||
\<open>entity that carries out software integration\<close>
|
||||
|
||||
subsection\<open>pre-existing software\<close>
|
||||
text\<open>software developed prior to the application currently in question, including COTS (commercial
|
||||
Definition*[PES :: concept, tag="''pre-existing software''"]
|
||||
\<open>software developed prior to the application currently in question, including COTS (commercial
|
||||
off-the shelf) and open source software\<close>
|
||||
|
||||
subsection\<open>open source software\<close>
|
||||
text\<open>source code available to the general public with relaxed or non-existent copyright restrictions
|
||||
\<close>
|
||||
Definition*[OSS :: concept, tag="''open source software''"]
|
||||
\<open>source code available to the general public with relaxed or non-existent copyright restrictions\<close>
|
||||
|
||||
subsection\<open>programmable logic controller\<close>
|
||||
text\<open>solid-state control system which has a user programmable memory for storage of instructions to
|
||||
implement specific functions
|
||||
\<close>
|
||||
Definition*[PLC::concept, tag="''programmable logic controller''"]
|
||||
\<open>solid-state control system which has a user programmable memory for storage of instructions to
|
||||
implement specific functions\<close>
|
||||
|
||||
subsection\<open>project management\<close>
|
||||
text\<open>administrative and/or technical conduct of a project, including safety aspects\<close>
|
||||
Definition*[PM::concept, tag="''project management''"]
|
||||
\<open>administrative and/or technical conduct of a project, including safety aspects\<close>
|
||||
|
||||
subsection\<open>project manager\<close>
|
||||
text\<open>entity that carries out project management\<close>
|
||||
Definition*[PGMGR::concept, tag="''project manager''"]
|
||||
\<open>entity that carries out project management\<close>
|
||||
|
||||
subsection\<open>reliability\<close>
|
||||
text\<open>ability of an item to perform a required function under given conditions for a given period of
|
||||
time\<close>
|
||||
Definition*[reliability::concept]
|
||||
\<open>ability of an item to perform a required function under given conditions for a given period of time\<close>
|
||||
|
||||
subsection\<open>robustness\<close>
|
||||
text\<open>ability of an item to detect and handle abnormal situations\<close>
|
||||
Definition*[robustness::concept]
|
||||
\<open>ability of an item to detect and handle abnormal situations\<close>
|
||||
|
||||
subsection\<open>requirements manager\<close>
|
||||
text\<open>entity that carries out requirements management\<close>
|
||||
Definition*[RMGR::concept, tag="''requirements manager''"]
|
||||
\<open>entity that carries out requirements management\<close>
|
||||
|
||||
subsection\<open>requirements management\<close>
|
||||
text\<open>the process of eliciting, documenting, analysing, prioritising and agreeing on requirements and
|
||||
Definition*[RMGMT::concept, tag="''requirements management''"]
|
||||
\<open>the process of eliciting, documenting, analysing, prioritising and agreeing on requirements and
|
||||
then controlling change and communicating to relevant stakeholders. It is a continuous process
|
||||
throughout a project
|
||||
\<close>
|
||||
throughout a project\<close>
|
||||
|
||||
subsection\<open>risk\<close>
|
||||
text\<open>combination of the rate of occurrence of accidents and incidents resulting in harm (caused by
|
||||
a hazard) and the degree of severity of that harm
|
||||
\<close>
|
||||
Definition*[risk::concept]
|
||||
\<open>combination of the rate of occurrence of accidents and incidents resulting in harm (caused by
|
||||
a hazard) and the degree of severity of that harm\<close>
|
||||
|
||||
subsection\<open>safety\<close>
|
||||
text\<open>freedom from unacceptable levels of risk of harm to people\<close>
|
||||
Definition*[safety::concept]
|
||||
\<open>freedom from unacceptable levels of risk of harm to people\<close>
|
||||
|
||||
subsection\<open>safety authority\<close>
|
||||
text\<open>body responsible for certifying that safety related software or services comply with relevant
|
||||
Definition*[SA::concept, tag="''safety authority''"]
|
||||
\<open>body responsible for certifying that safety related software or services comply with relevant
|
||||
statutory safety requirements\<close>
|
||||
|
||||
subsection\<open>safety function\<close>
|
||||
text\<open>a function that implements a part or whole of a safety requirement\<close>
|
||||
Definition*[SF::concept, tag="''safety function''"]
|
||||
\<open>a function that implements a part or whole of a safety requirement\<close>
|
||||
|
||||
subsection\<open>safety-related software\<close>
|
||||
text\<open>software which performs safety functions\<close>
|
||||
Definition*[SFRS::concept, tag= "''safety-related software''"]
|
||||
\<open>software which performs safety functions\<close>
|
||||
|
||||
subsection\<open>software\<close>
|
||||
text\<open>intellectual creation comprising the programs, procedures, rules, data and any associated
|
||||
Definition*[software::concept]
|
||||
\<open>intellectual creation comprising the programs, procedures, rules, data and any associated
|
||||
documentation pertaining to the operation of a system\<close>
|
||||
|
||||
subsection\<open>software baseline\<close>
|
||||
text\<open>complete and consistent set of source code, executable files, configuration files,
|
||||
Definition*[SB::concept, tag="''software baseline''"]
|
||||
\<open>complete and consistent set of source code, executable files, configuration files,
|
||||
installation scripts and documentation that are needed for a software release. Information about
|
||||
compilers, operating systems, preexisting software and dependent tools is stored as part of the
|
||||
baseline. This will enable the organisation to software deployment
|
||||
|
@ -160,91 +156,80 @@ released and assessed
|
|||
|
||||
|
||||
|
||||
subsection\<open>software life-cycle\<close>
|
||||
text\<open>those activities occurring during a period of time that starts when
|
||||
Definition*[SWLC::concept, tag="''software life-cycle''"]
|
||||
\<open>those activities occurring during a period of time that starts when
|
||||
software is conceived and ends when the software is no longer available for use. The software life
|
||||
cycle typically includes a requirements phase, design phase,test phase, integration phase,
|
||||
deployment phase and a maintenance phase 3.1.35 software maintainability
|
||||
capability of the software to be modified; to correct faults, improve to a different environment
|
||||
\<close>
|
||||
|
||||
subsection\<open>software maintenance\<close>
|
||||
text\<open> action, or set of actions, carried out on software after deployment functionality
|
||||
performance or other attributes, or adapt it with the aim of enhancing or correcting its
|
||||
\<close>
|
||||
Definition*[SM::concept, tag="''software maintenance''"]
|
||||
\<open> action, or set of actions, carried out on software after deployment functionality
|
||||
performance or other attributes, or adapt it with the aim of enhancing or correcting its\<close>
|
||||
|
||||
subsection\<open>software safety integrity level\<close>
|
||||
text\<open>classification number which determines the techniques and measures that have to be applied to
|
||||
Definition*[SOSIL::concept, tag="''software safety integrity level''"]
|
||||
\<open>classification number which determines the techniques and measures that have to be applied to
|
||||
software NOTE Safety-related software has been classified into five safety integrity levels, where
|
||||
0 is the lowest and 4 the highest.
|
||||
\<close>
|
||||
0 is the lowest and 4 the highest.\<close>
|
||||
|
||||
subsection\<open>supplier\<close>
|
||||
text\<open>entity that designs and builds a railway control and protection system including the software
|
||||
Definition*[supplier::concept]
|
||||
\<open>entity that designs and builds a railway control and protection system including the software
|
||||
or parts thereof\<close>
|
||||
|
||||
subsection\<open>system safety integrity level\<close>
|
||||
text\<open> classification number which indicates the required degree of confidence that an integrated
|
||||
system comprising hardware and software will meet its specified safety requirements
|
||||
\<close>
|
||||
Definition*[SYSIL::concept, tag="''system safety integrity level''"]
|
||||
\<open>classification number which indicates the required degree of confidence that an integrated
|
||||
system comprising hardware and software will meet its specified safety requirements\<close>
|
||||
|
||||
subsection\<open>tester\<close>
|
||||
text\<open>an entity that carries out testing
|
||||
\<close>
|
||||
Definition*[tester::concept]\<open>an entity that carries out testing\<close>
|
||||
|
||||
subsection\<open>testing\<close>
|
||||
text\<open>process of executing software under controlled conditions as to ascertain its behaviour and
|
||||
performance comparedto the corresponding requirements specification
|
||||
\<close>
|
||||
Definition*[testing::concept]
|
||||
\<open>process of executing software under controlled conditions as to ascertain its behaviour and
|
||||
performance compared to the corresponding requirements specification\<close>
|
||||
|
||||
subsection\<open>tool class T1\<close>
|
||||
text\<open>generates no outputs which candirectly or indirectly contribute to the executable code
|
||||
Definition*[TCT1::concept, tag="''tool class T1''"]
|
||||
\<open>generates no outputs which can directly or indirectly contribute to the executable code
|
||||
(including data) of the software NOTE 11 examples include: a text editor or a requirement or
|
||||
design support tool with no automatic code generation capabilities; configuration control tools.
|
||||
\<close>
|
||||
design support tool with no automatic code generation capabilities; configuration control tools.\<close>
|
||||
|
||||
subsection\<open>tool class T2\<close>
|
||||
text\<open>supports the test or verification of the design or executable code, where errors in the tool
|
||||
Definition*[TCT2::concept,tag="''tool class T2''"]
|
||||
\<open>supports the test or verification of the design or executable code, where errors in the tool
|
||||
can fail to reveal defects but cannot directly create errors in the executable software
|
||||
NOTE T2 examples include: a test harness generator; a test coverage measurement tool; a static
|
||||
analysis tool. reproduce defined versions and be the input for future releases at enhancements or
|
||||
at upgrade in the maintenance phase
|
||||
\<close>
|
||||
|
||||
subsection\<open>tool class T3\<close>
|
||||
text\<open>generates outputs which can directly or indirectly contribute to the executable code
|
||||
Definition*[TCT3::concept, tag="''tool class T3''"]
|
||||
\<open>generates outputs which can directly or indirectly contribute to the executable code
|
||||
(including data) of the safety related system NOTE T3 examples include: a source code compiler,
|
||||
a data/algorithms compiler, a tool to change set-points during system operation; an optimising
|
||||
compiler where the relationship between the source code program and the generated object code is
|
||||
not obvious; a compiler that incorporates an executable run-time package into the executable code.
|
||||
\<close>
|
||||
subsection\<open>traceability\<close>
|
||||
text\<open>degree to which relationship can be established between two or more products of a development
|
||||
Definition*[traceability::concept]
|
||||
\<open>degree to which relationship can be established between two or more products of a development
|
||||
process, especially those having a predecessor/successor or master/subordinate relationship to one
|
||||
another
|
||||
\<close>
|
||||
another\<close>
|
||||
|
||||
subsection\<open>validation\<close>
|
||||
text\<open>process of analysis followed by a judgment based on evidence to
|
||||
Definition*[validation::concept]
|
||||
\<open>process of analysis followed by a judgment based on evidence to
|
||||
documentation, software or application) fits the user needs,in particular with respect to safety
|
||||
and quality and determine whether an item (e.g. process, with emphasis on the suitability of its
|
||||
operation in accordance to its purpose in its intended environment
|
||||
\<close>
|
||||
operation in accordance to its purpose in its intended environment\<close>
|
||||
|
||||
subsection\<open>validator\<close>
|
||||
text\<open>entity that is responsible for the validation
|
||||
\<close>
|
||||
Definition*[validator::concept]
|
||||
\<open>entity that is responsible for the validation\<close>
|
||||
|
||||
subsection\<open>verification\<close>
|
||||
text\<open>process of examination followed by a judgment based on evidence that output items (process,
|
||||
Definition*[verification::concept]
|
||||
\<open>process of examination followed by a judgment based on evidence that output items (process,
|
||||
documentation, software or application) of a specific development phase fulfils the requirements of
|
||||
that phase with respect to completeness, correctness and consistency.
|
||||
NOTE Verification is mostly based on document reviews (design, implementation, test documents etc.).
|
||||
\<close>
|
||||
|
||||
subsection\<open>verifier\<close>
|
||||
text\<open>entity that is responsible for one or more verification activities
|
||||
\<close>
|
||||
Definition*[verifier::concept]
|
||||
\<open>entity that is responsible for one or more verification activities\<close>
|
||||
|
||||
|
||||
datatype role = PM (* Program Manager *)
|
||||
|
@ -420,6 +405,9 @@ doc_class test_documentation =
|
|||
|
||||
section\<open> Testing and Validation \<close>
|
||||
|
||||
text\<open>Test : @{concept \<open>cots\<close>}\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
DOF_core.name2doc_class_name @{theory} "requirement";
|
||||
DOF_core.name2doc_class_name @{theory} "srac";
|
||||
|
|
Loading…
Reference in New Issue