From ac1180b5291b6b7a89b7c7dc282f67344406a94f Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 22:18:47 +0100 Subject: [PATCH] - checking class invariants - checking monitor class invariants --- Isa_DOF.thy | 11 ++- .../conceptual/Concept_ExampleInvariant.thy | 89 ++++++++++++++++--- ontologies/Conceptual.thy | 2 +- 3 files changed, 87 insertions(+), 15 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index dfe346f3..3c27e190 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1090,7 +1090,10 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos), SOME X => check_if_final X | NONE => error ("Not belonging to a monitor class: "^oid) val delete_monitor_entry = DOF_core.map_data_global (DOF_core.upd_monitor_tabs (Symtab.delete oid)) - in thy |> update_instance_command args + val {cid=cid_long, ...} = the(DOF_core.get_object_global oid thy) + val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory + in thy |> update_instance_command args + |> (fn thy => (check_inv thy; thy)) |> delete_monitor_entry end @@ -1364,7 +1367,7 @@ fun calc_attr_access ctxt attr oid pos = (* template *) {long_name, typ=ty,...} = case DOF_core.get_attribute_info_local cid attr ctxt of SOME f => f - | NONE => error ("attribute undefined for ref"^ oid) + | NONE => error ("attribute undefined for reference: "^ oid) val proj_term = Const(long_name,dummyT --> ty) in calculate_attr_access0 ctxt proj_term term end | NONE => error "identifier not a docitem reference" @@ -1386,8 +1389,8 @@ val _ = Theory.setup fun calculate_trace ctxt oid pos = (* grabs attribute, and converts its HOL-term into (textual) ML representation *) - let fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) - val term = calc_attr_access ctxt "trace" oid pos + let val term = calc_attr_access ctxt "trace" oid pos + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) val string_pair_list = map conv (HOLogic.dest_list term) val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string in ML_Syntax.print_list print_string_pair string_pair_list end diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy index 850ac484..67b6297a 100644 --- a/examples/conceptual/Concept_ExampleInvariant.thy +++ b/examples/conceptual/Concept_ExampleInvariant.thy @@ -4,14 +4,12 @@ theory Concept_ExampleInvariant imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *) begin +section\Example: Standard Class Invariant\ + +text\Status:\ print_doc_classes print_doc_items -ML\fun check_A_invariant oid ctxt = - let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} - val (@{typ "int"},x_value) = HOLogic.dest_number term - in if x_value > 5 then error("class A invariant violation") else true end -\ text\Watch out: The current programming interface to document class invariants is pretty low-level: \<^item> No inheritance principle @@ -19,21 +17,92 @@ text\Watch out: The current programming interface to document class invari \<^item> Typing on ML level is assumed to be correct. The implementor of an ontology must know what he does ... \ + +text\Setting a sample invariant, which simply produces some side-effect:\ setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => fn ctxt => (writeln ("sample echo : "^oid); true))\ -section*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ +subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + + +text\Setting a sample invariant, referring to attribute value "x":\ +ML\fun check_A_invariant oid ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} + val (@{typ "int"},x_value) = HOLogic.dest_number term + in if x_value > 5 then error("class A invariant violation") else true end +\ setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ -(* test : should fail : -section*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ +(* test : should fail : *) +subsection*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ + + +subsection*[d::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + +(* test : update should fail : *) +update_instance*[d::A, x += "1"] + + +section\Example: Monitor Class Invariant\ + +text\Of particular interest are class invariants attached to monitor classes: since the +latter manage a trace-attribute, a class invariant on them can assure a global form of consistency. +It is possible to express: +\<^item> that attributes of a document element must satisfy particular conditions depending on the + prior document elements --- as long they have been observed in a monitor. +\<^item> non-regular properties on a trace not expressible in a regular expression + (like balanced ness of opening and closing text elements) +\<^item> etc. +\ + +text\A simple global trace-invariant is expressed in the following: it requires +that instances of class C occur more often as those of class D; note that this is meant +to take sub-classing into account: +\ + +ML\fun check_M_invariant oid ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val string_pair_list = map conv (HOLogic.dest_list term) + val cid_list = map fst string_pair_list + val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) + fun is_C x = DOF_core.is_subclass ctxt' x "Conceptual.C" + fun is_D x = DOF_core.is_subclass ctxt' x "Conceptual.D" + val n = length (filter is_C cid_list) + val m = length (filter is_D cid_list) + in if m > n then error("class M invariant violation") else true end +\ + +setup\DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\ + +open_monitor*[struct::M] + + +section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ + +text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ + +text*[d1::E, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, ... \ + +text*[c2::C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium consectetuer... \ + +section*[f::E] \ Lectus accumsan velit ultrices, ... }\ + +(* test : close_monitor should fail : * +section*[f2::E] \ Lectus accumsan velit ultrices, ... }\ *) +ML\val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here}; + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val string_pair_list = map conv (HOLogic.dest_list term) + \ +(* trace example *) +text\Setting a sample invariant, referring to attribute value "x":\ -(* to test : updates *) -(* to do: trace example *) +close_monitor*[struct] + end \ No newline at end of file diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy index 32c3a163..0cbcc649 100644 --- a/ontologies/Conceptual.thy +++ b/ontologies/Conceptual.thy @@ -44,7 +44,7 @@ doc_class M = section*[test::A]\ Test and Validation\ -text\Defining some document elements to be referenced in another theory: \ +text\Defining some document elements to be referenced in later on in another theory: \ text*[sdf] {* f @{thm refl}*} text*[sdfg] {* fg @{thm refl}*}