(************************************************************************* * 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\Testing hand-programmed (low-level) Invariants\ theory Concept_Example_Low_Level_Invariant imports "Isabelle_DOF_Unit_Tests_document" "Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *) TestKit begin section\Test Purpose.\ text\ Via @{ML "DOF_core.add_ml_invariant"} it is possible to attach user-defined ML-code to classes which is executed at each creation or modification of class instances. We test exection of creation and updates. \ text\Consult the status of the DOF engine:\ print_doc_classes print_doc_items section\Example: Standard Class Invariant\ text\Watch out: The current programming interface to document class invariants is pretty low-level: \<^item> No inheritance principle \<^item> No high-level notation in HOL \<^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\ fn thy => let val ctxt = Proof_Context.init_global thy val cid_long = DOF_core.get_onto_class_name_global "A" thy val bind = Binding.name "Sample_Echo" val exec = (fn oid => fn {is_monitor = b} => fn ctxt => (writeln ("sample echo : "^oid); true)) in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (exec, cid_long)) thy end \ text\The checker \exec\ above is set. Just used to provoke output: "sample echo : b"\ text*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ text\Setting a sample invariant, referring to attribute value "x":\ setup\ fn thy => let fun check_A_invariant oid {is_monitor:bool} ctxt = let val term = ISA_core.compute_attr_access ctxt "x" oid NONE @{here} val (@{typ "int"},x_value) = HOLogic.dest_number term in if x_value > 5 then error("class A invariant violation") else true end val cid_long = DOF_core.get_onto_class_name_global "A" thy val bind = Binding.name "Check_A_Invariant" 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\ subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ (* invariant still valid *) update_instance*[d::A, x += "1"] (* invariant no longer holds*) update_instance-assert-error[d::A, x += "1"]\class A invariant violation\ 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: \ setup\ fn thy => let fun check_M_invariant oid {is_monitor} ctxt = let val term = ISA_core.compute_attr_access ctxt "trace" oid NONE @{here} fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = let val s' = DOF_core.get_onto_class_name_global' (HOLogic.dest_string s) thy in (s', HOLogic.dest_string S) end 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 val cid_long = DOF_core.get_onto_class_name_global "M" thy val binding = Binding.name "Check_M_Invariant" in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (check_M_invariant, cid_long)) thy end \ section\Example: Monitor Class Invariant\ open_monitor*[struct::M] subsection*[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... \ subsection*[f::E] \ Lectus accumsan velit ultrices, ... \ text-assert-error[f2::E] \ Lectus accumsan velit ultrices, ... \\class M invariant violation\ ML\val ctxt = @{context} val term = ISA_core.compute_attr_access (Context.Proof ctxt) "trace" "struct" NONE @{here} ; fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) fun conv' (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = let val s' = DOF_core.get_onto_class_name_global' (HOLogic.dest_string s) (Proof_Context.theory_of ctxt) in (s', HOLogic.dest_string S) end val string_pair_list = map conv' (HOLogic.dest_list term); @{assert} (string_pair_list = [("Conceptual.A", "a"), ("Conceptual.C", "c1"), ("Conceptual.E", "d1"), ("Conceptual.C", "c2"), ("Conceptual.E", "f")]) \ close_monitor*[struct] end