forked from Isabelle_DOF/Isabelle_DOF
Small corrections
This commit is contained in:
parent
3c6eda2cbb
commit
d2d908534d
|
@ -666,89 +666,90 @@ verification and validation activities to be undertaken effectively.\<close>
|
||||||
section\<open> Design related Categories \<close>
|
section\<open> Design related Categories \<close>
|
||||||
|
|
||||||
doc_class design_item =
|
doc_class design_item =
|
||||||
description :: string
|
description :: string
|
||||||
|
|
||||||
datatype design_kind = unit | module | protocol
|
datatype design_kind = unit | module | protocol
|
||||||
|
|
||||||
doc_class interface = design_item +
|
doc_class interface = design_item +
|
||||||
kind :: design_kind
|
kind :: design_kind
|
||||||
|
|
||||||
|
|
||||||
section\<open> Requirements-Analysis related Categories \<close>
|
section\<open> Requirements-Analysis related Categories \<close>
|
||||||
|
|
||||||
doc_class test_item =
|
doc_class test_item =
|
||||||
nn :: "string option"
|
nn :: "string option"
|
||||||
|
|
||||||
doc_class test_specification = test_item +
|
doc_class test_specification = test_item +
|
||||||
short_goal :: string
|
short_goal :: string
|
||||||
|
|
||||||
doc_class test_case = test_item +
|
doc_class test_case = test_item +
|
||||||
descr :: string
|
descr :: string
|
||||||
|
|
||||||
doc_class test_result = test_item +
|
doc_class test_result = test_item +
|
||||||
verdict :: bool
|
verdict :: bool
|
||||||
remarks :: string
|
remarks :: string
|
||||||
covvrit :: test_coverage_criterion
|
covvrit :: test_coverage_criterion
|
||||||
|
|
||||||
datatype test_environment_kind = hardware_in_the_loop ("hil")
|
datatype test_environment_kind = hardware_in_the_loop ("hil")
|
||||||
| simulated_hardware_in_the_loop ("shil")
|
| simulated_hardware_in_the_loop ("shil")
|
||||||
|
|
||||||
doc_class test_environment = test_item +
|
doc_class test_environment = test_item +
|
||||||
descr :: string
|
descr :: string
|
||||||
kind :: test_environment_kind <= shil
|
kind :: test_environment_kind <= shil
|
||||||
|
|
||||||
doc_class test_tool = test_item +
|
doc_class test_tool = test_item +
|
||||||
descr :: string
|
descr :: string
|
||||||
|
|
||||||
doc_class test_requirement = test_item +
|
doc_class test_requirement = test_item +
|
||||||
descr :: string
|
descr :: string
|
||||||
|
|
||||||
doc_class test_adm_role = test_item +
|
doc_class test_adm_role = test_item +
|
||||||
name :: string
|
name :: string
|
||||||
|
|
||||||
doc_class test_documentation =
|
doc_class test_documentation =
|
||||||
no :: "nat"
|
no :: "nat"
|
||||||
accepts "test_specification ~~ \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
accepts "test_specification ~~
|
||||||
\<lbrakk>test_requirement\<rbrakk> ~~ test_adm_role"
|
\<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~
|
||||||
accepts " test_specification ~~ \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
\<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||||
\<lbrakk>test_requirement \<rbrakk> ~~ test_adm_role"
|
\<lbrakk>test_requirement\<rbrakk> ~~
|
||||||
|
test_adm_role"
|
||||||
|
accepts "test_specification ~~
|
||||||
|
\<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~
|
||||||
|
\<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||||
|
\<lbrakk>test_requirement \<rbrakk> ~~
|
||||||
|
test_adm_role"
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
section\<open> META : Testing and Validation \<close>
|
section\<open> META : Testing and Validation \<close>
|
||||||
|
|
||||||
text\<open>Test : @{semi_formal_content \<open>COTS\<close>}\<close>
|
text\<open>Test : @{semi_formal_content \<open>COTS\<close>}\<close>
|
||||||
|
|
||||||
ML\<open>
|
ML
|
||||||
DOF_core.read_cid_global @{theory} "requirement";
|
\<open> DOF_core.read_cid_global @{theory} "requirement";
|
||||||
DOF_core.read_cid_global @{theory} "SRAC";
|
DOF_core.read_cid_global @{theory} "SRAC";
|
||||||
DOF_core.is_defined_cid_global "SRAC" @{theory};
|
DOF_core.is_defined_cid_global "SRAC" @{theory};
|
||||||
DOF_core.is_defined_cid_global "EC" @{theory};
|
DOF_core.is_defined_cid_global "EC" @{theory}; \<close>
|
||||||
\<close>
|
|
||||||
|
|
||||||
ML\<open>
|
ML
|
||||||
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.EC";
|
\<open> DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.EC";
|
||||||
DOF_core.is_subclass @{context} "CENELEC_50128.SRAC" "CENELEC_50128.EC";
|
DOF_core.is_subclass @{context} "CENELEC_50128.SRAC" "CENELEC_50128.EC";
|
||||||
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.SRAC";
|
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.SRAC";
|
||||||
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.test_requirement";
|
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.test_requirement"; \<close>
|
||||||
\<close>
|
|
||||||
|
|
||||||
ML\<open>val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context};
|
ML
|
||||||
Symtab.dest ref_tab;
|
\<open> val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context};
|
||||||
Symtab.dest class_tab;
|
Symtab.dest ref_tab;
|
||||||
\<close>
|
Symtab.dest class_tab; \<close>
|
||||||
|
|
||||||
ML\<open>
|
ML
|
||||||
val internal_data_of_SRAC_definition = DOF_core.get_attributes_local "SRAC" @{context}
|
\<open> val internal_data_of_SRAC_definition = DOF_core.get_attributes_local "SRAC" @{context} \<close>
|
||||||
\<close>
|
|
||||||
|
|
||||||
ML\<open>
|
ML
|
||||||
DOF_core.read_cid_global @{theory} "requirement";
|
\<open> DOF_core.read_cid_global @{theory} "requirement";
|
||||||
Syntax.parse_typ @{context} "requirement";
|
Syntax.parse_typ @{context} "requirement";
|
||||||
val Type(t,_) = Syntax.parse_typ @{context} "requirement" handle ERROR _ => dummyT;
|
val Type(t,_) = Syntax.parse_typ @{context} "requirement" handle ERROR _ => dummyT;
|
||||||
Syntax.read_typ @{context} "hypothesis" handle _ => dummyT;
|
Syntax.read_typ @{context} "hypothesis" handle _ => dummyT;
|
||||||
Proof_Context.init_global;
|
Proof_Context.init_global; \<close>
|
||||||
\<close>
|
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -365,36 +365,35 @@
|
||||||
}
|
}
|
||||||
|
|
||||||
% An experiment in inheritance of the default behaviour.
|
% An experiment in inheritance of the default behaviour.
|
||||||
%\newisadof{text.scholarly_paper.definition}%
|
% \newisadof{text.scholarly_paper.definition}%
|
||||||
%[label=,type=%
|
% [label=,type=%
|
||||||
% , scholarly_paper.math_content.short_name =%
|
% , scholarly_paper.math_content.short_name =%
|
||||||
% , scholarly_paper.math_content.mcc =%
|
% , scholarly_paper.math_content.mcc =%
|
||||||
% , Isa_COL.text_element.level =%
|
% , Isa_COL.text_element.level =%
|
||||||
% , Isa_COL.text_element.referentiable =%
|
% , Isa_COL.text_element.referentiable =%
|
||||||
% , Isa_COL.text_element.variants =%
|
% , Isa_COL.text_element.variants =%
|
||||||
% , scholarly_paper.text_section.main_author =%
|
% , scholarly_paper.text_section.main_author =%
|
||||||
% , scholarly_paper.text_section.fixme_list =%
|
% , scholarly_paper.text_section.fixme_list =%
|
||||||
% , scholarly_paper.technical.definition_list =%
|
% , scholarly_paper.technical.definition_list =%
|
||||||
% , scholarly_paper.technical.status =%
|
% , scholarly_paper.technical.status =%
|
||||||
% ]
|
% ]
|
||||||
% [1]
|
% [1]
|
||||||
% {%
|
% {%
|
||||||
% \begin{text.scholarly_paper.math_content}%
|
% \cscommand{text.scholarly_paper.math_content}%
|
||||||
% [label=\commandkey{label},type=\commandkey{type}%
|
% [label=\commandkey{label},type=\commandkey{type}%
|
||||||
% , scholarly_paper.math_content.short_name =\commandkey{scholarly_paper.math_content.short_name}%
|
% , scholarly_paper.math_content.short_name =\commandkey{scholarly_paper.math_content.short_name}%
|
||||||
% , scholarly_paper.math_content.mcc =\commandkey{scholarly_paper.math_content.mcc}%
|
% , scholarly_paper.math_content.mcc =\commandkey{scholarly_paper.math_content.mcc}%
|
||||||
% , Isa_COL.text_element.level =\commandkey{Isa_COL.text_element.level}%
|
% , Isa_COL.text_element.level =\commandkey{Isa_COL.text_element.level}%
|
||||||
% , Isa_COL.text_element.referentiable =\commandkey{Isa_COL.text_element.referentiable}%
|
% , Isa_COL.text_element.referentiable =\commandkey{Isa_COL.text_element.referentiable}%
|
||||||
% , Isa_COL.text_element.variants =\commandkey{Isa_COL.text_element.variants}%
|
% , Isa_COL.text_element.variants =\commandkey{Isa_COL.text_element.variants}%
|
||||||
% , scholarly_paper.text_section.main_author =\commandkey{scholarly_paper.text_section.main_author}%
|
% , scholarly_paper.text_section.main_author =\commandkey{scholarly_paper.text_section.main_author}%
|
||||||
% , scholarly_paper.text_section.fixme_list =\commandkey{scholarly_paper.text_section.fixme_list}%
|
% , scholarly_paper.text_section.fixme_list =\commandkey{scholarly_paper.text_section.fixme_list}%
|
||||||
% , scholarly_paper.technical.definition_list =\commandkey{scholarly_paper.technical.definition_list}%
|
% , scholarly_paper.technical.definition_list =\commandkey{scholarly_paper.technical.definition_list}%
|
||||||
% , scholarly_paper.technical.status =\commandkey{scholarly_paper.technical.status}%
|
% , scholarly_paper.technical.status =\commandkey{scholarly_paper.technical.status}%
|
||||||
% ]
|
% ]
|
||||||
% #1%
|
% {#1}%
|
||||||
% \end{text.scholarly_paper.math_content}%
|
% }
|
||||||
% }
|
|
||||||
%
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
%% Besser: Einfach durchreichen wg Vererbung !
|
%% Besser: Einfach durchreichen wg Vererbung !
|
||||||
\newisadof{text.scholarly_paper.lemma}%
|
\newisadof{text.scholarly_paper.lemma}%
|
||||||
|
|
Loading…
Reference in New Issue