From ef3eee03c9a94fdadceccd1662ec01bd7188937f Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sat, 4 Mar 2023 13:55:32 +0100 Subject: [PATCH 1/2] extended testkit by declare tester, added consistency proofs for OntoMatching. --- .../Concept_Example_Low_Level_Invariant.thy | 3 +- .../Concept_OntoReferencing.thy | 16 ++--- Isabelle_DOF-Unit-Tests/Latex_Tests.thy | 21 ++++--- .../Ontology_Matching_Example.thy | 63 +++++++++++++++---- Isabelle_DOF-Unit-Tests/TestKit.thy | 26 ++++++-- 5 files changed, 92 insertions(+), 37 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy b/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy index b5eb9515..d3769935 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy @@ -67,6 +67,7 @@ let fun check_A_invariant oid {is_monitor:bool} ctxt = in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (check_A_invariant, cid_long)) thy end \ +(* borderline test *) text*[d0::A, x = "5"] \Lorem ipsum dolor sit amet, ...\ text-assert-error[d1::A, x = "6"]\Lorem ipsum dolor sit amet, ...\\class A invariant violation\ @@ -75,7 +76,7 @@ subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ (* invariant still valid *) update_instance*[d::A, x += "1"] -(* invariant no longer *) +(* invariant no longer holds*) update_instance-assert-error[d::A, x += "1"]\class A invariant violation\ diff --git a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy index 7fb4162e..8fc937f8 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy @@ -13,12 +13,10 @@ chapter\Creating and Referencing Ontological Instances\ -theory - Concept_OntoReferencing - imports - "Isabelle_DOF-Unit-Tests_document" - "Isabelle_DOF-Ontologies.Conceptual" - "TestKit" +theory Concept_OntoReferencing + imports "TestKit" + "Isabelle_DOF-Unit-Tests_document" + "Isabelle_DOF-Ontologies.Conceptual" begin section\Test Purpose.\ @@ -89,9 +87,7 @@ ML*[c4::C]\fun fac x = if x = 0 then 1 else x * (fac(x-1))\ (* TODO lemma*[e5::E] asd: "True" by simp -(* Correct report: "Duplicate instance declaration.. " -declare_reference*[c1::C] \ \forward declaration\ -*) +declare_reference-assert-error[c1::C]\Duplicate instance declaration\ \ \forward declaration\ declare_reference*[e6::E] @@ -101,7 +97,7 @@ definition*[e6::E] facu :: "nat \ nat" where "facu arg = undefined" text\As shown in @{E [display]\e5\} following from @{E [display]\e6\}\ -(* BUG: why is option [display] necessary ? *) +(* BUG ?: why is option [display] necessary ? *) text\As shown in @{C [display]\c4\}\ diff --git a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy index b83db275..84c703f6 100644 --- a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy +++ b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy @@ -11,23 +11,25 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) -theory - Latex_Tests -imports - "Isabelle_DOF-Unit-Tests_document" - "TestKit" -keywords "Figure*" :: document_body (* still experimental feature *) +theory Latex_Tests + imports "TestKit" + "Isabelle_DOF-Unit-Tests_document" + keywords "Figure*" :: document_body (* still experimental feature *) begin -section\Elementary Creation of Doc-items and Access of their Attibutes\ +section\Test Purpose.\ +text\ Testing the generation of LaTeX code. Serves in particular during development. \ text\Output status:\ print_doc_classes print_doc_items +section\Elementary Creation of Doc-items and Access of their Attibutes\ + + text\And here a tex - text macro.\ text\Pythons ReStructuredText (RST). @{url \https://de.wikipedia.org/wiki/ReStructuredText\}. Tool: Sphinx. @@ -109,6 +111,8 @@ setup\DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" text-latex\ \<^blong>\asd\ outer \<^blong>\syntax| ! see {syntax, outer}\ \ (*>*) +section\Experimental Code and Test of advanced LaTeX for free-form text units\ + ML\ fun report_text ctxt text = @@ -237,8 +241,7 @@ text-latex\ -section\Section Experiments of picture-content\ - +section\Experimental Section for Multiple Figure Content\ ML\ diff --git a/Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy b/Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy index 239ff4b0..eb4dcdaa 100644 --- a/Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy +++ b/Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy @@ -1,11 +1,32 @@ -chapter\Ontologys Mathing\ +(************************************************************************* + * Copyright (C) + * 2019-2023 The University of Exeter + * 2018-2023 The University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + +chapter\Ontologys Matching\ theory Ontology_Matching_Example - imports "Isabelle_DOF.Isa_DOF" - "Isabelle_DOF-Unit-Tests_document" + imports TestKit + "Isabelle_DOF.Isa_DOF" + "Isabelle_DOF-Unit-Tests_document" begin +section\Test Purpose.\ +text\ This is merely an example that shows that the generated invariants + fit nicely together; i.e. allow for sensible consistency and invariant + preservation proofs related to ontological matchings. \ + +section\The Scenario.\ + text\Using HOL, we can define a mapping between two ontologies. It is called ontology matching or ontology alignment. Here is an example which show how to map two classes. @@ -14,19 +35,21 @@ text\Using HOL, we can define a mapping between two ontologies. type_synonym UTF8 = string definition utf8_to_string - where "utf8_to_string x = x" + where "utf8_to_string xx = xx" doc_class A = - first_name :: UTF8 - last_name :: UTF8 - age :: nat - married_to :: "string option" + first_name :: UTF8 + last_name :: UTF8 + age :: nat + married_to :: "string option" invariant a :: "age \ < 18 \ married_to \ = None" + + doc_class B = - name :: string - adult :: bool - is_married :: bool + name :: string + adult :: bool + is_married :: bool invariant b :: "is_married \ \ adult \" text\We define the mapping between the two classes, @@ -39,6 +62,15 @@ definition A_to_B_morphism , adult = (age X \ 18) , is_married = (married_to X \ None) \" +text\Sanity check: Invariants are non-contradictory, i.e. there is a witness.\ + +lemma inv_a_satisfyable : " Ex (a_inv::A \ bool)" + unfolding a_inv_def + apply(rule_tac x ="\Ontology_Matching_Example.A.tag_attribute = xxx, + first_name = yyy, last_name = zzz, age = 17, + married_to = None\" in exI) + by auto + text\Now we check that the invariant is preserved through the morphism:\ lemma inv_a_preserved : @@ -46,6 +78,15 @@ lemma inv_a_preserved : unfolding a_inv_def b_inv_def A_to_B_morphism_def by auto +text\This also implies that B invariants are non-contradictory: \ + +lemma inv_b_preserved : "\x. (b_inv::B \ bool) x" + apply(rule_tac x ="A_to_B_morphism \Ontology_Matching_Example.A.tag_attribute = xxx, + first_name = yyy, last_name = zzz, age = 17, + married_to = None\" in exI) + by(rule inv_a_preserved,auto simp: a_inv_def) + + lemma A_morphism_B_total : "A_to_B_morphism ` ({X::A. a_inv X}) \ ({X::B. b_inv X})" using inv_a_preserved diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy index 41b8e86d..7fd0f4d5 100644 --- a/Isabelle_DOF-Unit-Tests/TestKit.thy +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -16,9 +16,10 @@ theory imports "Isabelle_DOF-Unit-Tests_document" "Isabelle_DOF-Ontologies.Conceptual" -keywords "text-" "text-latex" :: document_body - and "text-assert-error" :: document_body - and "update_instance-assert-error" :: document_body +keywords "text-" "text-latex" :: document_body + and "text-assert-error" :: document_body + and "update_instance-assert-error" :: document_body + and "declare_reference-assert-error" :: document_body begin @@ -151,11 +152,26 @@ val _ = (ODL_Meta_Args_Parser.attributes_upd -- Parse.document_source >> (Toplevel.theory o update_instance_command)); +val _ = + let fun create_and_check_docitem ((((oid, pos),cid_pos),doc_attrs),src) thy= + (Value_Command.Docitem_Parser.create_and_check_docitem + {is_monitor = false} {is_inline=true} + {define = false} oid pos (cid_pos) (doc_attrs) thy) + handle ERROR msg => (if error_match src msg + then (writeln ("Correct error:"^msg^":reported.");thy) + else error"Wrong error reported") + in Outer_Syntax.command \<^command_keyword>\declare_reference-assert-error\ + "declare document reference" + (ODL_Meta_Args_Parser.attributes -- Parse.document_source + >> (Toplevel.theory o create_and_check_docitem)) + end; + + + val _ = Outer_Syntax.command ("text-latex", \<^here>) "formal comment (primary style)" (Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true}); - \ (* auto-tests *) @@ -163,7 +179,5 @@ text-latex\dfg\ text-assert-error[aaaa::A]\ @{A \sdf\}\\reference ontologically inconsistent\ -ML\String.isPrefix "ab" "abc"\ - end (*>*) From 48c6457f63fb392dc6050729eb8bc3f81ec5477f Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Sat, 4 Mar 2023 13:58:51 +0100 Subject: [PATCH 2/2] Code Cleanup. --- Isabelle_DOF-Unit-Tests/TestKit.thy | 21 +-------------------- 1 file changed, 1 insertion(+), 20 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy index 7fd0f4d5..5bfe8a38 100644 --- a/Isabelle_DOF-Unit-Tests/TestKit.thy +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -23,30 +23,11 @@ keywords "text-" "text-latex" :: document_body begin -section\Elementary Creation of Doc-items and Access of their Attibutes\ - - -text\Current status:\ -print_doc_classes -print_doc_items - -(* this corresponds to low-level accesses : *) -ML\ -val docitem_tab = DOF_core.get_instances \<^context>; -val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>; -val docclass_tab = DOF_core.get_onto_classes \<^context>; - -Name_Space.dest_table docitem_tab; -Name_Space.dest_table isa_transformer_tab; -Name_Space.dest_table docclass_tab; -app; -\ +section\Testing Commands (exec-catch-verify - versions of std commands)\ ML\ -val _ = Document_Output.document_output - fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, xstring_opt:(xstring * Position.T) option),