- checking class invariants

- checking monitor class invariants

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)
+    let val term = calc_attr_access ctxt "trace" oid pos
-        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

examples/conceptual/Concept_ExampleInvariant.thy

@@ -4,14 +4,12 @@ theory Concept_ExampleInvariant
   imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
 begin
 
+section\<open>Example: Standard Class Invariant\<close>
+
+text\<open>Status:\<close>
 print_doc_classes
 print_doc_items
 
-ML\<open>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
-\<close>
 
 text\<open>Watch out: The current programming interface to document class invariants is pretty low-level:
 \<^item> No inheritance principle
@@ -19,21 +17,92 @@ text\<open>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 ...
 \<close>
+
+text\<open>Setting a sample invariant, which simply produces some side-effect:\<close>
 setup\<open>DOF_core.update_class_invariant "Conceptual.A" (fn oid => 
                                                        fn ctxt => 
                                                         (writeln ("sample echo : "^oid); true))\<close>
 
-section*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
+subsection*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
+
+
+text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
+ML\<open>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
+\<close>
 
 setup\<open>DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\<close>
 
-(* test : should fail :
+(* test : should fail : *)
-section*[c::A, x = "6"] \<open> Lorem ipsum dolor sit amet, ... \<close>
+subsection*[c::A, x = "6"] \<open> Lorem ipsum dolor sit amet, ... \<close>
+
+
+subsection*[d::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
+
+(* test : update should fail : *)
+update_instance*[d::A, x += "1"]
+
+
+section\<open>Example: Monitor Class Invariant\<close>
+
+text\<open>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.
+\<close>
+
+text\<open>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:
+\<close>
+
+ML\<open>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
+\<close>
+
+setup\<open>DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\<close>
+
+open_monitor*[struct::M]  
+
+
+section*[a::A, x = "3"]       \<open> Lorem ipsum dolor sit amet, ... \<close>
+
+text*[c1::C, x = "''beta''"]  \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
+
+text*[d1::E, a1 = "X3"]       \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
+    
+text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer...  \<close>
+
+section*[f::E]                \<open> Lectus accumsan velit ultrices, ... }\<close>
+
+(* test : close_monitor should fail : *
+section*[f2::E]               \<open> Lectus accumsan velit ultrices, ... }\<close>
 *)
+ML\<open>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)
+  \<close>
+(*  trace example *)
+text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
 
-(* to test : updates *)
 
-(* to do: trace example *)
+close_monitor*[struct]
+
 
 end 
   

ontologies/Conceptual.thy

@@ -44,7 +44,7 @@ doc_class M =
 
 
 section*[test::A]\<open> Test and Validation\<close>
-text\<open>Defining some document elements to be referenced in another theory: \<close>
+text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
 text*[sdf] {* f @{thm refl}*}  
 text*[sdfg] {* fg @{thm refl}*}