From a803d999c0acccf24d09305ff94ba546e0053e3c Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Thu, 21 Apr 2022 13:37:36 +0200 Subject: [PATCH] Reorganization of the Proving Morphisms on Ontologies section --- .../scholarly_paper/2021-ITP-PMTI/paper.thy | 149 ++++++++---------- 1 file changed, 67 insertions(+), 82 deletions(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 956f04f..9b7115a 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -801,10 +801,6 @@ onto_class Computer_Hardware = Product + composed_of :: "Product list" invariant c2 :: "Product.mass \ = sum(map Product.mass (composed_of \))" -definition Item_to_Resource_morphism :: "Item \ Resource" - ("_ \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m" [1000]999) - where "\ \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m = \ Resource.tag_attribute = 0::int , - Resource.name = name \ \" definition Product_to_Component_morphism :: "Product \ Component" ("_ \Component\\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999) @@ -844,24 +840,48 @@ text\ The \<^dof> framework does not assume that all documents refer to the same ontology. Each document may even build its local ontology without any external reference. It may also be based on several reference ontologies (\<^eg>, from the \<^dof> library). - Since ontological instances possess \<^emph>\representations inside the logic\, the relationship between a local ontology and a reference ontology can be formalised -using a morphism function also inside the logic. -More precisely, the instances of local ontology classes may be described as the image of a +using a morphism function also inside the logic. More precisely, the instances of local ontology +classes may be described as the image of a transformation applied to one or several other instances of class(es) belonging to another -ontology. - -Thanks to the morphism relationship, the obtained class may either import meta-data +ontology. Thanks to the morphism relationship, the obtained class may either import meta-data (definitions are preserved) or map meta-data (the properties are different but are semantically equivalent) that are defined in the referenced class(es). It may also provide additional properties. This means that morphisms may be injective, surjective, bijective, and thus describe abstract relations between ontologies. This raises the question of invariant preservation. \ - text\ -\begin{figure} +To illustrate this process, we have defined a simple ontology to classify Hardware objects. +%This ontology is described in \autoref{fig-Local-Ontology-example + +%\begin{figure}[!h] +@{boxed_theory_text [display] +\onto_class Item = + name :: string +onto_class Product = Item + + serial_number :: int + provider :: string + mass :: int +onto_class Computer_Hardware = Product + + type :: Hardware_Type + composed_of :: "Product list" + invariant c2 :: "Product.mass \ = sum(map Product.mass (composed_of \))"\} +%\caption{An extract of a local (user) ontology.} +%\label{fig-Local-Ontology-example} +%\end{figure} +%} + +This ontology defines the \<^typ>\Item\, \<^typ>\Product\ and \<^typ>\Computer_Hardware\ concepts (or classes). +Each class contains a set of attributes or properties and some local invariants. +In this example, we focus on the \<^typ>\Computer_Hardware\ +class defined as a list of products characterised by their mass value. +This class contains a local \<^theory_text>\invariant c2\ to guarantee that its own mass value +equals the sum of all the masses of the products composing the object. +For the sake of the argument, we use the reference ontology (considered as a standard) +described in this listing : +%\begin{figure} @{boxed_theory_text [display] \definition sum where "sum S = (fold (+) S 0)" @@ -882,68 +902,42 @@ onto_class Hardware = Informatic + mass :: int composed_of :: "Component list" invariant c1 :: "mass \ = sum(map Component.mass (composed_of \))"\} -\caption{An extract of a reference ontology.} -\label{fig-Reference-Ontology-example} -\end{figure} - -To illustrate this process, we use the reference ontology (considered as a standard) described -in the listing \autoref{fig-Reference-Ontology-example}, defining the \<^typ>\Resource\, -\<^typ>\Electronic\, \<^typ>\Component\, \<^typ>\Informatic\ and \<^typ>\Hardware\ concepts (or classes). -Each class contains a set of attributes or properties and some local invariants. +%\caption{An extract of a reference ontology.} +%\label{fig-Reference-Ontology-example} +%\end{figure} +This ontology defines the \<^typ>\Resource\, +\<^typ>\Electronic\, \<^typ>\Component\, \<^typ>\Informatic\ and \<^typ>\Hardware\ concepts. In our example, we focus on the \<^typ>\Hardware\ class containing a \<^const>\mass\ attribute and composed of a list of components with a \<^const>\mass\ attribute formalising the mass value of each component. The \<^typ>\Hardware\ class also contains a local \<^theory_text>\invariant c1\ to define a constraint linking the global mass of a \<^typ>\Hardware\ object with the masses of its own components. + \ text\ -\begin{figure} +To check the coherence of our local ontology, we define a relationship between the local ontology +and the reference ontology using morphism functions (or mapping rules as in ATL framework~@{cite "atl"} +or EXPRESS-X language~@{cite "BGPP95"}). These rules are applied to define the relationship +between one class of the local ontology to one or several other class(es) described in the reference +ontology. In our case, we have define two morphises, \<^const>\Product_to_Component_morphism\ +and \<^const>\Computer_Hardware_to_Hardware_morphism\, detailed in the following listing : + +%\begin{figure} @{boxed_theory_text [display] -\onto_class Item = - name :: string -onto_class Product = Item + - serial_number :: int - provider :: string - mass :: int -onto_class Computer_Hardware = Product + - type :: Hardware_Type - composed_of :: "Product list" - invariant c2 :: "Product.mass \ = sum(map Product.mass (composed_of \))"\} -\caption{An extract of a local (user) ontology.} -\label{fig-Local-Ontology-example} -\end{figure} - -For the sake of the argument, we have defined a simple ontology to classify Hardware objects. -This ontology is described in \autoref{fig-Local-Ontology-example} and -defines the \<^typ>\Item\, \<^typ>\Product\ and \<^typ>\Computer_Hardware\ concepts. -As for the reference ontology, we focus on the \<^typ>\Computer_Hardware\ -class defined as a list of products characterised by their mass value. -This class contains a local \<^theory_text>\invariant c2\ to guarantee that its own mass value -equals the sum of all the masses of the products composing the object. -\ - - -text\ -\begin{figure} -@{boxed_theory_text [display] -\definition Item_to_Resource_morphism :: "Item \ Resource" - ("_ \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m" [1000]999) - where "\ \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m = \ Resource.tag_attribute = 0::int , - Resource.name = name \ \" - -definition Product_to_Component_morphism :: "Product \ Component" - ("_ \Component\\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999) +\definition Product_to_Component_morphism :: + "Product \ Component" ("_ \Component\\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999) where " \ \Component\\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t = \ Resource.tag_attribute = 1::int , Resource.name = name \ , Electronic.provider = provider \ , Electronic.manufacturer = ''no manufacturer'' , Component.mass = mass \ , - Component.dimensions = [] \" + Component.dimensions = [] \"\} -definition Computer_Hardware_to_Hardware_morphism :: +@{boxed_theory_text [display] +\definition Computer_Hardware_to_Hardware_morphism :: "Computer_Hardware \ Hardware" ("_ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e" [1000]999) where "\ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e = @@ -954,30 +948,22 @@ definition Computer_Hardware_to_Hardware_morphism :: Hardware.mass = mass \ , Hardware.composed_of = map Product_to_Component_morphism (composed_of \) \"\} -\caption{An extract of a mapping definition.} - -\label{fig-mapping-example} -\end{figure} +%\caption{An extract of a mapping definition.} +%\label{fig-mapping-example} +%\end{figure} -To check the coherence of our local ontology, we define a relationship between the local ontology -and the reference ontology using morphism functions (or mapping rules as in ATL framework~@{cite "atl"} -or EXPRESS-X language~@{cite "BGPP95"}). These rules are applied to define the relationship -between one class of the local ontology to one or several other class(es) described in the reference -ontology. - -\<^const>\Product_to_Component_morphism\ and \<^const>\Computer_Hardware_to_Hardware_morphism\ -definitions, detailed in \autoref{fig-mapping-example}, -specify how \<^typ>\Product\ or \<^typ>\Computer_Hardware\ objects are mapped to \<^typ>\Component\ +These definitions specify how \<^typ>\Product\ or \<^typ>\Computer_Hardware\ objects are mapped to \<^typ>\Component\ or \<^typ>\Hardware\ objects defined in the reference ontology. This mapping shows that the structure of a (user) ontology may be arbitrarily different from the one of a standard ontology it references. \ - - text\ -\begin{figure} +The following example proof for a simple, but typical example of reformatting +meta-data into another format along an ontological mapping are nearly trivial: + +%\begin{figure} @{boxed_theory_text [display] \lemma inv_c2_preserved : "c2_inv \ \ c1_inv (\ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)" @@ -990,16 +976,16 @@ lemma Computer_Hardware_to_Hardware_total : "Computer_Hardware_to_Hardware_morphism ` ({X. c2_inv X}) \ ({X::Hardware. c1_inv X})" using inv_c2_preserved by auto\} -\caption{Proofs establishing an Invariant Preservation.} -\label{fig-xxx} -\end{figure} -\ -text\The example proof in \autoref{fig-xxx} for a simple, but typical example of reformatting -meta-data into another format along an ontological mapping are nearly trivial: after unfolding +%\caption{Proofs establishing an Invariant Preservation.} +%\label{fig-xxx} +%\end{figure} + +After unfolding the invariant and the morphism definitions, the preservation proof is automatic. The advantage 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.\ +of invariants, as we have demonstrated in the previous example. +\ (*<*) text\Ontology example extracted from @@ -1169,7 +1155,6 @@ Regarding using formal methods to formalise standards, Event-B method was used b 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"} 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. @@ -1183,7 +1168,7 @@ The proposed approach was exemplified on ARINC 661 standard and weather radar sy % exist approaches based on strong type systems \ -section*[concl::conclusion]\Conclusion\ +section*[concl::conclusion]\Conclusion and Future Work\ text\We presented \<^dof>, an ontology framework deeply integrating continuous-check\slash continuous-build functionality into the formal development process in \<^hol>. The novel feature of term-contexts in \<^dof>,