diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 31c810d8..61ee082e 100755 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -513,8 +513,10 @@ section\ Design and Test Documents \ doc_class cenelec_document = text_element + phase :: "phase" - level :: "int option" <= "Some(-1)" \ \Must be a "chapter" in the - overall document\ + level :: "int option" <= "Some(-1)" \ \Must be a "chapter" in the overall document\ + written_by :: role \ \Annex C Table C.1 \ + fst_check :: role \ \Annex C Table C.1\ + snd_check :: role \ \Annex C Table C.1\ is_concerned :: "role set" <= "UNIV" text\see Fig.3.\ @@ -562,20 +564,23 @@ doc_class SWDS = cenelec_document + phase :: "phase" <= "SD" type_synonym software_design_specification = SWDS -doc_class SWIS_CE = - \ \channel, input - output of an operation, public global variables ...\ +doc_class SWIS_E = + \ \input - output of an operation; alternatives could be channels or public global variables ...\ op_name :: "string" op_args_ty :: "(string \ typ) list \ typ" - op_exn_ty :: "(string \ typ) list" - pre_cond :: "thm list" <= "[]" - post_cond :: "thm list" <= "[]" + raises_exn :: "(string \ typ) list" \ \exn name and value\ + pre_cond :: "(string \ thm) list" <= "[]" \ \labels and predicates\ + post_cond :: "(string \ thm) list" <= "[]" \ \labels and predicates\ boundary_pre_cond :: "thm list" <= "[]" - type_synonym software_interface_specification_component = SWIS_CE + type_synonym software_interface_specification_element = SWIS_E doc_class SWIS = cenelec_document + phase :: "phase" <= "SCDES" - components :: "SWIS_CE list" + written_by :: "role" <= "DES" + fst_check :: "role" <= "VER" + snd_check :: "role" <= "VAL" + components :: "SWIS_E list" type_synonym software_interface_specification = SWIS doc_class SWITS = cenelec_document + @@ -758,7 +763,7 @@ doc_class test_requirement = test_item + doc_class test_adm_role = test_item + name :: string -doc_class test_documentation = +doc_class test_documentation = (* OUTDATED ? *) no :: "nat" accepts "test_specification ~~ \test_case~~test_result\\<^sup>+ ~~