pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Integrated is_monitor flag for monitor class invariants. 

Makes special treatment of monitor class invariants
possible, when changes of trace are indirect...
This commit is contained in:
Burkhart Wolff 2018-12-03 22:36:08 +01:00
parent ac1180b529
commit 17c66f0fea
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
examples/conceptual/Concept_ExampleInvariant.thy
View File

@ -20,14 +20,15 @@ The implementor of an ontology must know what he does ...
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>
fn {is_monitor = b} =>
fn ctxt =>
(writeln ("sample echo : "^oid); true))\<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 =
ML\<open>fun check_A_invariant oid {is_monitor:bool} 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
@ -62,7 +63,7 @@ that instances of class C occur more often as those of class D; note that this i
to take sub-classing into account:
\<close>
ML\<open>fun check_M_invariant oid ctxt =
ML\<open>fun check_M_invariant oid {is_monitor} 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)