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

added an Interface Element into cENeLEC
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Burkhart Wolff 2022-04-08 15:56:03 +02:00
parent 7201101a6c
commit 6f4259cc2c
1 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -553,6 +553,7 @@ doc_class SWTS = cenelec_document +
phase :: "phase" <= "SD"
type_synonym software_test_specification = SWTS
doc_class SWAS = cenelec_document +
phase :: "phase" <= "SD"
type_synonym software_architecture_specification = SWAS
@ -561,8 +562,21 @@ doc_class SWDS = cenelec_document +
phase :: "phase" <= "SD"
type_synonym software_design_specification = SWDS
doc_class SWIS_component_element =
\<comment> \<open>channel, input - output of an operation, public global varianles ...\<close>
op_name :: "string"
op_args_ty :: "(string \<times> typ) list"
op_res_ty :: "typ list"
op_exn_ty :: "(string \<times> typ) list"
pre_cond :: "thm list" <= "[]"
post_cond :: "thm list" <= "[]"
boundary_pre_cond :: "thm list" <= "[]"
type_synonym SWIS_CE = SWIS_component_element
doc_class SWIS = cenelec_document +
phase :: "phase" <= "SD"
compionents :: "SWIS_component_element list"
type_synonym software_interface_specification = SWIS
doc_class SWITS = cenelec_document +