Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

added stubs for CC project

This commit is contained in:
Burkhart Wolff 2020-08-20 12:53:39 +02:00
parent 1470776428
commit f35d498ad8
3 changed files with 11 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

0
examples/CC_ISO15408/README Normal file
View File

0
src/ontologies/CC_ISO15408/README Normal file
View File

21
src/ontologies/CENELEC_50128/CENELEC_50128.thy
View File

@ -285,16 +285,16 @@ datatype phase = SYSDEV_ext (* System Development Phase (external) *)
| SD (* Software Deployment *)
| SM (* Software Maintenance *)
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"
abbreviation software_component_design:: "phase" where "software_component_design \<equiv> SCDES"
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"
abbreviation software_component_design :: "phase" where "software_component_design \<equiv> SCDES"
abbreviation component_implementation_and_testing :: "phase"
where "component_implementation_and_testing \<equiv> CInT"
abbreviation software_integration :: "phase" where "software_integration \<equiv> SI"
abbreviation software_validation :: "phase" where "software_validation \<equiv> SV"
abbreviation software_deployment :: "phase" where "software_deployment \<equiv> SD"
abbreviation software_maintenance :: "phase" where "software_maintenance \<equiv> SM"
where "component_implementation_and_testing \<equiv> CInT"
abbreviation software_integration :: "phase" where "software_integration \<equiv> SI"
abbreviation software_validation :: "phase" where "software_validation \<equiv> SV"
abbreviation software_deployment :: "phase" where "software_deployment \<equiv> SD"
abbreviation software_maintenance :: "phase" where "software_maintenance \<equiv> SM"
term "SR" (* meta-test *)
@ -359,7 +359,8 @@ doc_class FnI = requirement +
doc_class AC = requirement +
is_concerned :: "role set" <= "UNIV"
type_synonym application_conditions = AC
type_synonym application_conditions = AC
text\<open>The category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions. It has formal, semi-formal
and informal sub-categories. They have to be tracked and discharged by appropriate