From d422e78849d3da388efbbfeae069846f0b861ee1 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 13 Apr 2022 19:40:10 +0200 Subject: [PATCH] completed sec 5 --- .../scholarly_paper/2021-ITP-PMTI/paper.thy | 73 +++++++++++-------- 1 file changed, 43 insertions(+), 30 deletions(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 9cbaa4d..e405dfb 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -1176,24 +1176,27 @@ onto_class assoc_Method_Problem = section*[appl_certif::technical]\Application: CENELEC Ontology\ text\From its beginning, \<^dof> had been used for documents containing formal models targeting certifications. A major case-study from the railways domain based on the CENELEC 50128 standard -had been published earlier (cf. @{cite "DBLP:conf-ifm-BruckerW19"}) \<^footnote>\ Our CENELEC ontology in -\<^dof> can be found at \<^url>\https://github.com/logicalhacking/Isabelle_DOF/blob/main/src/ontologies/CENELEC_50128/CENELEC_50128.thy\.\. +had been published earlier (cf. @{cite "DBLP:conf-ifm-BruckerW19"}) +\<^footnote>\ Our CENELEC ontology in +\<^dof> can be found at +\<^url>\https://github.com/logicalhacking/Isabelle_DOF/blob/main/src/ontologies/CENELEC_50128/CENELEC_50128.thy\.\. The CENELEC Standard comprises 18 different ``Design and Test Documents''; a fully fledged description of our ontology covering these is therefore out of reach of this paper. -Rather, we present how the novel concepts like invariants and term-antiquotations are used in +Rather, we present how the novel concepts such as invariants and term-antiquotations are used in selected elements in this ontology. According to CENELEC Table C.1, for example, we specify the category of ``Design and Test Documents'' as follows: -@{theory_text [display] \ +@{boxed_theory_text [display] \ doc_class cenelec_document = text_element + phase :: phase written_by :: role \ \Annex C Table C.1 \ - fst_check :: role \ \Annex C Table C.1\ - snd_check :: role \ \Annex C Table C.1\ + fst_check :: role \ \Annex C Table C.1 \ + snd_check :: role \ \Annex C Table C.1 \ ... invariant must_be_chapter :: "text_element.level \ = Some(0)" - invariant two_eyes_prcple :: "written_by \ \ fst_check \ \ written_by \ \ snd_check \" + invariant two_eyes_prcple :: "written_by \ \ fst_check \ + \ written_by \ \ snd_check \" \} This class refers to the ``software phases'' the standard postulates (like \SPL\ for ``Software Planning'' or \SCDES\ for ``Software Component Design'') @@ -1205,35 +1208,45 @@ the textual structure of a chapter (the \level\-attribute is inheri ontology library specifying text-elements) as well as the two-eyes-principle between authors and checkers of this document. \ -(* -text\The concrete instance of the \cenelec_document\-class is the -\software_interface_specification\ (\SWIS\ for short) as shown below, -where the role attribution as done for this document type accordingly: -@{theory_text [display] \ -doc_class SWIS = cenelec_document + \ \software_interface_specification\ - phase :: "phase" <= "SCDES" - written_by :: "role" <= "DES" - fst_check :: "role" <= "VER" - snd_check :: "role" <= "VAL" +text\ The concrete instance of the \cenelec_document\ - class is the +\software_interface_specification\ (\SWIS\ for short) as shown below, +where the role assignment is done for this document type as follows: +@{boxed_theory_text [display] \ +doc_class SWIS = cenelec_document + \ \software interface specification\ + phase :: "phase" <= "SCDES" written_by :: "role" <= "DES" + fst_check :: "role" <= "VER" snd_check :: "role" <= "VAL" components :: "SWIS_E list" -\}\ -text\ -While the structural constraints presented so far can in principle be covered by any -conventional validation process and the editing be supported by, \<^eg>, the Protégé editor -@{cite "protege"}, a closer look at the class \SWIS_E\ (``software interface specification element'') -referenced in the \components\-attribute reveals the unique power of \<^dof>: -@{theory_text [display] \ +\} +The structural constraints expressed so far can in principle be covered by any +conventional validation process and suitable editing support (\<^eg>, Protégé @{cite "protege"}). +However, a closer look at the class \SWIS_E\ (``software interface specification +element'') referenced in the \components\-attribute reveals the unique power of \<^dof>: +@{boxed_theory_text [display] \ doc_class SWIS_E = - \ \input - output of an operation; alternatives could be channels or public global variables ...\ op_name :: "string" - op_args_res :: "(string \ typ) list \ typ" - pre_cond :: "(string \ thm) list" \ \labels and predicates\ - post_cond :: "(string \ thm) list" \ \labels and predicates\ + op_args_res :: "(string \ typ) list \ typ" \ \args and result type\ + pre_cond :: "(string \ thm) list" \ \labels and predicates\ + post_cond :: "(string \ thm) list" \ \labels and predicates\ + invariant well_formed_pre :: "\cond \ set(map snd (pre_cond \)). + iswff\<^sub>p\<^sub>r\<^sub>e (op_args_res \) (cond)" + invariant well_formed_post:: ... \} +where the constants \iswff\<^sub>p\<^sub>r\<^sub>e\ is bound to a functions at the SML-level, that +is executed during the evaluation phase of these invariants and that checks: +\<^item> Any \cond\ is indeed a valid definition in the global logical context of Isabelle/HOL + (taking HOL-libraries but also the concrete safety specification into account). +\<^item> Any such definition has the syntactic form: \pre_ (a\<^sub>1::\\<^sub>1) ... (a\<^sub>n::\\<^sub>n) \ \, + where the \(a\<^sub>1::\\<^sub>1) ... (a\<^sub>n::\\<^sub>n)\ correspond to the argument list of the operation. +\<^item> The case for the post-condition is treated analogously. \ - +text\Note that this technique can also be applied to impose specific constraints on types in +Isabelle/HOL. For example, via the SI-package available in the Isabelle AFP +\<^footnote>\\<^url>\https://www.isa-afp.org/entries/Physical_Quantities.html\\, it is possible to express +that the result of some calculation is of type +\32 unsigned [m\<^sup>os\<^sup>-\<^sup>2]\, so a 32-bit unsigned integer representing an acceleration in the SI-system. +Therefore it is possible to impose that some values refer to physical dimensions +measured in a concrete metrological system. \ -*) section*[concl::conclusion]\Conclusion\ text\We presented \<^dof>, an ontology framework