From 35b50e419f87f2c95b9cc72ca21b21c21698a4a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Wed, 20 Apr 2022 14:51:39 +0200 Subject: [PATCH] Update related work and enable checking for section 5 Also fix typos --- .../scholarly_paper/2021-ITP-PMTI/paper.thy | 279 +++++------------- src/document-templates/root-lncs.tex | 2 +- 2 files changed, 80 insertions(+), 201 deletions(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index cffc9e3..d311d55 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -457,7 +457,7 @@ doc_class myintro = mytext_section + and force_level :: "the (level \) > 1" doc_class myclaim = myintro + based_on :: "string list" -doc_class mytechnical = text_section + +doc_class mytechnical = mytext_section + formal_results :: "thm list" datatype kind = expert_opinion | argument | "proof" @@ -1002,174 +1002,64 @@ of using the \<^dof> framework compared to approaches like ATL or EXPRESS-X is the possibility of formally verifying the \<^emph>\mapping rules\. \<^ie> proving the preservation of invariants, as we have demonstrated in the previous example.\ -(* -section*[ontoexample::text_section,main_author="Some(@{docitem ''idir''}::author)"] -\Mathematics Example : An Extract from OntoMath\textsuperscript{PRO}\ - (*<*) -(* OntoMathPro_Ontology example *) +text\Ontology example extracted from +\<^file>\$ISABELLE_DOF_HOME/src/ontologies/CENELEC_50128/CENELEC_50128.thy\ and adapted\ -datatype dc = creator string | title string +datatype role = PM \ \Program Manager\ + | RQM \ \Requirements Manager\ + | DES \ \Designer\ + | IMP \ \Implementer\ + | ASR \ \Assessor\ + | INT \ \Integrator\ + | TST \ \Tester\ + | VER \ \Verifier\ + | VnV \ \Verification and Validation\ + | VAL \ \Validator\ -datatype owl = - backwardCompatibleWith string - | deprecated string - | incompatibleWith string - | priorVersion string - | versionInfo string - -datatype rdfs = - comment string - | isDefinedBy string - | label string - | seeAlso string +datatype phase = SYSDEV_ext \ \ System Development Phase (external)\ + | SPl \ \Software Planning\ + | SR \ \Software Requirement\ + | SA \ \Software Architecture\ + | SDES \ \Software Design\ + | SCDES \ \Software Component Design\ + | CInT \ \Component Implementation and Testing\ + | SI \ \Software Integration\ + | SV \ \Software Validation\ + | SD \ \Software Deployment\ + | SM \ \Software Maintenance\ -datatype annotation = DC dc | OWL owl | RDFS rdfs +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 \ + invariant must_be_chapter :: "text_element.level \ = Some(0)" + invariant two_eyes_prcple :: "written_by \ \ fst_check \ + \ written_by \ \ snd_check \" -onto_class Top = - Annotations :: "annotation list" +definition "iswff\<^sub>p\<^sub>r\<^sub>e" :: "bool" + where "iswff\<^sub>p\<^sub>r\<^sub>e \ True" -onto_class Field_of_mathematics = - Annotations :: "annotation list" <= "[RDFS (label ''Field of mathematics'')]" - invariant restrict_annotation_F ::"set (Annotations \) \ - range (RDFS o label) \ range (RDFS o comment)" +doc_class SWIS_E = + op_name :: "string" + 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:: ...*) -onto_class Mathematical_knowledge_object = - Annotations :: "annotation list" - invariant restrict_annotation_M ::"set (Annotations \) \ - range (RDFS o label) \ range (RDFS o comment)" - -onto_class assoc_F_M = - contains:: "(Field_of_mathematics \ Mathematical_knowledge_object) set" - invariant contains_defined :: "\ x. x \ Domain (contains \) - \ (\ y \ Range (contains \). (x, y) \ contains \)" - -onto_class assoc_M_F = - belongs_to :: "(Mathematical_knowledge_object \ Field_of_mathematics) set" - invariant belong_to_defined :: "\ x. x \ Domain (belongs_to \) - \ (\ y \ Range (belongs_to \). (x, y) \ belongs_to \)" - -onto_class assoc_M_M = - is_defined_by :: "(Mathematical_knowledge_object \ Mathematical_knowledge_object) set" - invariant is_defined_by_defined :: "\ x. x \ Domain (is_defined_by \) - \ (\ y \ Range (is_defined_by \). (x, y) \ is_defined_by \)" -(*typedef 'a A'_scheme = - "{x :: 'a A_scheme. " -*) - -onto_class assoc_M_M' = - "defines" :: "(Mathematical_knowledge_object \ Mathematical_knowledge_object) set" - invariant defines_defined :: "\ x. x \ Domain (defines \) - \ (\ y \ Range (defines \). (x, y) \ defines \)" - -onto_class assoc_M_M_see_also = - see_also :: "(Mathematical_knowledge_object rel) set" - invariant see_also_trans :: "\ r \ (see_also \). trans r" - invariant see_also_sym :: "\ r \ (see_also \). sym r" - -onto_class Problem = Mathematical_knowledge_object + - Annotations :: "annotation list" - -onto_class Method = Mathematical_knowledge_object + - Annotations :: "annotation list" - -onto_class assoc_Problem_Method = - is_solved_by :: "(Problem \ Method) set" - invariant is_solved_by_defined :: "\ x. x \ Domain (is_solved_by \) - \ (\ y \ Range (is_solved_by \). (x, y) \ is_solved_by \)" - -onto_class assoc_Method_Problem = - solves :: "(Method \ Problem) set" - invariant solves_defined :: "\ x. x \ Domain (solves \) - \ (\ y \ Range (solves \). (x, y) \ solves \)" +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" + type_synonym software_interface_specification = SWIS (*>*) -text\ - The \<^emph>\OntoMath\textsuperscript{PRO}\ ontology~@{cite "Nevzorova2014OntoMathPO"} - is an OWL ontology of mathematical knowledge concepts. - It possesses the \<^emph>\is-a\ semantics for hierarchies of mathematical knowledge elements, - and defines these elements as two hierarchies of classes: - a taxonomy of the fields of mathematics and a taxonomy of mathematical knowledge objects. - It defines two main type of relations for these two taxonomies: - directed relations between elements of the two hierarchies - like \<^const>\belongs_to\, \<^const>\contains\, \<^const>\defines\, \<^const>\is_defined_by\, \<^const>\solves\, - \<^const>\is_solved_by\, and a symmetric transitive associative relation \<^const>\see_also\ - between two mathematical knowledge objects. - It also represents links with external resources - such as DBpedia~@{cite "10.1007/978-3-540-76298-0_52"} - with annotations properties~@{cite "Parsia:12:OWO"}. - \<^dof> covers a wide range of the OWL concepts used by the OntoMath\textsuperscript{PRO} ontology. - We can represent the annotations properties as datatypes and - then attach them as an attributes list to a class. - For example the declaration: -@{theory_text [display,indent=5, margin=70] \ -datatype dc = creator string | title string -datatype owl = backwardCompatibleWith string - | deprecated string - | incompatibleWith string - | priorVersion string - | versionInfo string -datatype rdfs = comment string - | isDefinedBy string - | label string - | seeAlso string -datatype annotation = DC dc | OWL owl | RDFS rdfs +section*[appl_certif::technical]\Application: CENELEC Ontology\ -onto_class Field_of_mathematics = - Annotations :: "annotation list" <= "[RDFS (label ''Field of mathematics'')]" - invariant restrict_annotation_F ::"set (Annotations \) \ - range (RDFS o label) - \ range (RDFS o comment)" -\} - defines the class \<^typ>\Field_of_mathematics\ with an attribute \<^theory_text>\Annotations\ - which is a \<^type>\list\ of \<^typ>\annotation\s. - We can even constrain the type of allowed \<^typ>\annotation\s with an invariant. - Here the \<^theory_text>\invariant restrict_annotation_F\ forces the \<^typ>\annotation\s to be - a \<^const>\label\ or a \<^const>\comment\. - Subsumption relation is straightforward. - The OntoMath\textsuperscript{PRO} ontology defines - a \<^typ>\Problem\ and a \<^typ>\Method\ - as subclasses of the class \<^typ>\Mathematical_knowledge_object\. - It gives in \<^dof>: -@{theory_text [display,indent=5, margin=70] \ -onto_class Problem = Mathematical_knowledge_object + - Annotations :: "annotation list" - -onto_class Method = Mathematical_knowledge_object + - Annotations :: "annotation list" -\} - We can express the relations between the two taxonomies - with association \<^theory_text>\onto_class\es which specify - the relation as an attribute and enforces the relation with an \<^theory_text>\invariant\. - The two directed relations \<^const>\is_solved_by\ and \<^const>\solves\ - between \<^typ>\Problem\ and a \<^typ>\Method\ can be represented in \<^dof> like this: -@{theory_text [display,indent=5, margin=70] \ -onto_class assoc_Problem_Method = - is_solved_by :: "(Problem \ Method) set" - invariant is_solved_by_defined :: "\ x. x \ Domain (is_solved_by \) - \ (\ y \ Range (is_solved_by \). (x, y) \ is_solved_by \)" - -onto_class assoc_Method_Problem = - solves :: "(Method \ Problem) set" - invariant solves_defined :: "\ x. x \ Domain (solves \) - \ (\ y \ Range (solves \). (x, y) \ solves \)" -\} - where the attributes \<^const>\is_solved_by\ and \<^const>\solves\ define the relations - of the classes and the invariants \<^theory_text>\is_solved_by_defined\ and \<^theory_text>\solves_defined\ enforce - the existence of the relations when one define instances of the classes. - - \<^dof> allows to define ontologies and specify constraints - on their concepts. - Additionally it dynamically checks at run-time the concepts when defining instances. - It offers an environment to define and test ontologies in an integrated document, - where all the knowledge and the proof-checking can be specified, - and thus can help to find the right trade-off between plain vocabularies and - highly formalized models. -\ -*) - -section*[appl_certif::technical]\Selected Applications to the 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"}) @@ -1183,8 +1073,8 @@ selected elements in this ontology. According to CENELEC Table C.1, for example, we specify the category of ``Design and Test Documents'' as follows: -@{boxed_theory_text [display] \ -doc_class cenelec_document = text_element + +@{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 \ @@ -1192,45 +1082,44 @@ doc_class cenelec_document = text_element + ... invariant must_be_chapter :: "text_element.level \ = Some(0)" 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'') + \ written_by \ \ snd_check \"\} + +This class refers to the ``software phases'' the standard postulates (like \<^const>\SPl\ for +``Software Planning'' or \<^const>\SCDES\ for ``Software Component Design'') which we model by a corresponding enumeration types (not shown here). -Similarly, the standard postulates ``roles'' that certain specified teams posses in the overall process -(like \VER\ for verification and \VAL\ for validation). We added invariants that specify -certain constraints implicit in the standard: for example, a \cenelec_document\ must have -the textual structure of a chapter (the \level\-attribute is inherited from an underlying +Similarly, the standard postulates ``roles'' that certain specified teams possess in the overall process +(like \<^const>\VER\ for verification and \<^const>\VAL\ for validation). We added invariants that specify +certain constraints implicit in the standard: for example, a \<^typ>\cenelec_document\ must have +the textual structure of a chapter (the \<^emph>\level\-attribute is inherited from an underlying ontology library specifying basic text-elements) as well as the two-eyes-principle between authors and checkers of these chapters. \ -text\ The concrete sub-class of \cenelec_document\ is the -\software_interface_specification\-class (\SWIS\ for short) as shown below, +text\ The concrete sub-class of \<^typ>\cenelec_document\ is the +\<^typ>\software_interface_specification\-class (\<^typ>\SWIS\ for short) as shown below, which provides the role assignment required for this document type: @{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" -\} + components:: "SWIS_E list"\} The structural constraints expressed so far can in principle be covered by any hand-coded 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>; +However, a closer look at the class \<^typ>\SWIS_E\ (``software interface specification +element'') referenced in the \<^const>\components\-attribute reveals the unique power of \<^dof>; rather than saying ``there must be a pre-condition'', \<^dof> can be far more precise: -@{boxed_theory_text [display] \ -doc_class SWIS_E = +@{boxed_theory_text [display] +\doc_class SWIS_E = op_name :: "string" 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 + invariant well_formed_post:: ...\} +where the constant \<^const>\iswff\<^sub>p\<^sub>r\<^sub>e\ is bound to a function 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 +\<^item> Any \<^emph>\cond\ is indeed a valid definition in the global logical context (taking HOL-libraries but also the concrete certification target model into account). \<^item> Any such HOL definition has the syntactic form: \<^vs>\-0.3cm\ @@ -1253,45 +1142,35 @@ section*[rw::related_work]\Related Work\ text\There are a number of approaches to use ontologies for structuring the link between information and knowledge, and to make it amenable to ``semantic'' search in or consistency checking of documents. -Some are targeting mathematical libraries: - -\<^item> The search engine \<^url>\http://shinh.org/wfs\ uses clever text-based search methods in - a large number of formulas, agnostic of their logical context, and of formal proof. - -\<^item> The OAF project @{cite "KohlhaseR21"} +Some are targeting mathematical libraries, +like the search engine \<^url>\http://shinh.org/wfs\ which uses clever text-based search methods in + a large number of formulas, agnostic of their logical context and of formal proof, +or the OAF project @{cite "KohlhaseR21"} which developed a common ontological format, called OMDoc/MMT, and - developed six \<^emph>\export\ functions from major ITP systems into it. + six \<^emph>\export\ functions from major ITP systems into it. The emphasis was put on building a server infrastructure based on conventional, rather heavy-weight database and OWL technology. -\<^item> There are meanwhile a number of proposals of ontologies targeting mathematics: - \<^item> OntoMath\textsuperscript{PRO} @{cite "Nevzorova2014OntoMathPO"} proposes a +There are also a number of proposals of ontologies targeting mathematics: +the OntoMath\textsuperscript{PRO} @{cite "Nevzorova2014OntoMathPO"} proposes a ``taxonomy of the fields of mathematics'' (pp 110). In total, OntoMath\textsuperscript{PRO} contains the daunting number of 3,449 classes, which is in part due to the need to compensate the lack of general datatype definition methods for meta-data. - \<^item> Other ontologies worth mentioning are DBpedia @{cite "10.1007/978-3-540-76298-0_52"}, +Other ontologies worth mentioning are DBpedia @{cite "10.1007/978-3-540-76298-0_52"}, which provides with the \<^emph>\SPARQL endpoint\ \<^url>\http://dbpedia.org/sparql\ a search engine, and the more general ScienceWISE \<^footnote>\\<^url>\http://sciencewise.info/ontology/\.\ - that allows users to introduce their own category concepts. + that allows users to introduce their own category concepts. Regarding using formal methods to formalise standards, Event-B method was used by Fotso et al. @{cite "FotsoFLM18"} to propose a specification of the hybrid ERTMS/ETCS level 3 standard, in which requirements are specified using SysML/KAOS goal diagrams that are translated into Event-B, and domain-specific properties are specified by ontologies. -In another case, Mendil et al. @{cite "MendilASMP21"} proposes an Event-B framework for formalising standard +In another case, Mendil et al. @{cite "MendilASMP21"} propose an Event-B framework for formalising standard conformance through formal modelling of standards as ontologies. The proposed approach was exemplified on ARINC 661 standard and weather radar system application. - Our approach emphasizes type-safeness, expressive power and ``depth'' of meta-data, - which is adapted to the specific needs of ITP systems and theory developments. - It is a concrete proposal for the ITP community allowing - a deeper structuring of mathematical libraries - such as the Isabelle Archive of Formal Proofs (AFP)~@{cite "AFP-ref22"} - which passed the impressive numbers of 650 articles, - written by 420 authors at the beginning of 2022. - % \<^url>\https://github.com/CLLKazan/OntoMathPro\ % % ITEM The "Ontology for Engineering Mathematics" diff --git a/src/document-templates/root-lncs.tex b/src/document-templates/root-lncs.tex index 83258d5..aaeb1c7 100644 --- a/src/document-templates/root-lncs.tex +++ b/src/document-templates/root-lncs.tex @@ -98,7 +98,7 @@ \input{session} % optional bibliography \IfFileExists{root.bib}{% -{\small \renewcommand{\doi}[1]{} +{\small \newcommand{\urlprefix}{} \bibliographystyle{splncs04}