Manual merge.
This commit is contained in:
commit
a2a1f2dc3f
18
Isa_COL.thy
18
Isa_COL.thy
|
|
@ -13,6 +13,9 @@ begin
|
|||
|
||||
section\<open> Library of Standard Text Ontology \<close>
|
||||
|
||||
|
||||
|
||||
|
||||
datatype placement = pl_h | pl_t | pl_b | pl_ht | pl_hb
|
||||
|
||||
|
||||
|
|
@ -45,6 +48,19 @@ doc_class figure_group =
|
|||
(* dito the future monitor: table - block *)
|
||||
|
||||
|
||||
text\<open> The attribute @{term "level"} in the subsequent enables doc-notation support section* etc.
|
||||
we follow LaTeX terminology on levels
|
||||
\<^enum> part = Some -1
|
||||
\<^enum> chapter = Some 0
|
||||
\<^enum> section = Some 1
|
||||
\<^enum> subsection = Some 2
|
||||
\<^enum> subsubsection = Some 3
|
||||
\<^enum> ...
|
||||
|
||||
for scholarly paper: invariant level > 0 \<close>
|
||||
|
||||
doc_class text_element =
|
||||
level :: "int option" <= "None"
|
||||
|
||||
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
|
||||
|
||||
|
|
@ -64,7 +80,7 @@ doc_class formal_content =
|
|||
|
||||
doc_class concept =
|
||||
tag :: "string" <= "''''"
|
||||
properties :: "thm list"
|
||||
properties :: "thm list" <= "[]"
|
||||
|
||||
section\<open>Tests\<close>
|
||||
|
||||
|
|
|
|||
144
Isa_DOF.thy
144
Isa_DOF.thy
|
|
@ -63,6 +63,45 @@ val docclass_markup = docref_markup_gen docclassN
|
|||
|
||||
\<close>
|
||||
|
||||
section\<open>String Utilities\<close>
|
||||
|
||||
ML\<open>
|
||||
fun spy x y = (writeln (x ^ y); y)
|
||||
|
||||
fun markup2string x = XML.content_of (YXML.parse_body x)
|
||||
|
||||
(* a hacky, but save encoding of unicode comming from the interface to the string format
|
||||
that can be parsed by the inner-syntax string parser ''dfdf''. *)
|
||||
fun bstring_to_holstring ctxt x (* (x:bstring) *) : string =
|
||||
let val term = Syntax.parse_term ctxt (markup2string x)
|
||||
fun hpp x = if x = #"\\" then "@" else
|
||||
if x = #"@" then "@@" else String.implode [x]
|
||||
in term |> Sledgehammer_Util.hackish_string_of_term ctxt
|
||||
|> map hpp o String.explode |> String.concat
|
||||
end;
|
||||
|
||||
|
||||
fun chopper p (x:string) =
|
||||
let fun hss buff [] = rev buff
|
||||
|hss buff (S as a::R) = if p a then let val (front,rest) = take_prefix p S
|
||||
in hss (String.implode front :: buff) rest end
|
||||
else let val (front,rest) = take_prefix (not o p) S
|
||||
in hss (String.implode front ::buff) rest end
|
||||
in hss [] (String.explode x) end;
|
||||
|
||||
|
||||
fun holstring_to_bstring ctxt (x:string) : bstring =
|
||||
let fun collapse "" = ""
|
||||
|collapse S = if String.sub(S,0) = #"@"
|
||||
then let val n = String.size S
|
||||
val front = replicate (n div 2) #"@"
|
||||
val back = if (n mod 2)=1 then [#"\\"] else []
|
||||
in String.implode (front @ back) end
|
||||
else S;
|
||||
val t = String.concat (map collapse (chopper (fn x => x = #"@") x));
|
||||
in t |> Syntax.string_of_term ctxt o Syntax.parse_term ctxt end;
|
||||
|
||||
\<close>
|
||||
|
||||
section\<open> A HomeGrown Document Type Management (the ''Model'') \<close>
|
||||
|
||||
|
|
@ -401,17 +440,17 @@ fun declare_anoobject_local ctxt cid =
|
|||
end
|
||||
|
||||
|
||||
fun get_object_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy)
|
||||
in case Symtab.lookup tab oid of
|
||||
NONE => error("undefined reference: "^oid)
|
||||
|SOME(bbb) => bbb
|
||||
end
|
||||
fun get_object_global_opt oid thy = Symtab.lookup (#tab(#docobj_tab(get_data_global thy))) oid
|
||||
|
||||
fun get_object_local oid ctxt = let val {tab,...} = #docobj_tab(get_data ctxt)
|
||||
in case Symtab.lookup tab oid of
|
||||
fun get_object_global oid thy = case get_object_global_opt oid thy of
|
||||
NONE => error("undefined reference: "^oid)
|
||||
|SOME(bbb) => bbb
|
||||
|
||||
fun get_object_local_opt oid ctxt = Symtab.lookup (#tab(#docobj_tab(get_data ctxt))) oid
|
||||
|
||||
fun get_object_local oid ctxt = case get_object_local_opt oid ctxt of
|
||||
NONE => error("undefined reference: "^oid)
|
||||
|SOME(bbb) => bbb
|
||||
end
|
||||
|
||||
fun get_doc_class_global cid thy =
|
||||
if cid = default_cid then error("default doc class acces") (* TODO *)
|
||||
|
|
@ -511,15 +550,15 @@ fun update_isa_global (isa, trans) thy =
|
|||
|
||||
|
||||
fun transduce_term_global (term,pos) thy =
|
||||
(* pre: term should be fully typed in order to allow type-relqted term-transformations *)
|
||||
(* pre: term should be fully typed in order to allow type-related term-transformations *)
|
||||
let val tab = #ISA_transformer_tab(get_data_global thy)
|
||||
fun T(Const(s,ty) $ t) = if String.isPrefix ISA_prefix s
|
||||
then case Symtab.lookup tab s of
|
||||
NONE => error("undefined inner syntax antiquotation: "^s)
|
||||
| SOME(trans) => case trans thy (t,ty,pos) of
|
||||
| SOME(trans) => (case trans thy (t,ty,pos) of
|
||||
NONE => Const(s,ty) $ t
|
||||
(* checking isa, may raise error though. *)
|
||||
| SOME t => Const(s,ty) $ t
|
||||
| SOME t => Const(s,ty) $ t)
|
||||
(* transforming isa *)
|
||||
else (Const(s,ty) $ (T t))
|
||||
|T(t1 $ t2) = T(t1) $ T(t2)
|
||||
|
|
@ -695,6 +734,7 @@ typedecl "thy"
|
|||
|
||||
consts ISA_typ :: "string \<Rightarrow> typ" ("@{typ _}")
|
||||
consts ISA_term :: "string \<Rightarrow> term" ("@{term _}")
|
||||
consts ISA_term_repr :: "string \<Rightarrow> term" ("@{termrepr _}")
|
||||
consts ISA_thm :: "string \<Rightarrow> thm" ("@{thm _}")
|
||||
consts ISA_file :: "string \<Rightarrow> file" ("@{file _}")
|
||||
consts ISA_thy :: "string \<Rightarrow> thy" ("@{thy _}")
|
||||
|
|
@ -796,8 +836,9 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) =
|
|||
|
||||
(* utilities *)
|
||||
|
||||
fun property_list_dest X = map HOLogic.dest_string
|
||||
(map (fn Const ("Isa_DOF.ISA_term", _) $ s => s )
|
||||
fun property_list_dest ctxt X = (map (fn Const ("Isa_DOF.ISA_term", _) $ s => HOLogic.dest_string s
|
||||
|Const ("Isa_DOF.ISA_term_repr",_) $ s
|
||||
=> holstring_to_bstring ctxt (HOLogic.dest_string s))
|
||||
(HOLogic.dest_list X))
|
||||
|
||||
end; (* struct *)
|
||||
|
|
@ -805,11 +846,12 @@ end; (* struct *)
|
|||
\<close>
|
||||
subsection\<open> Isar - Setup\<close>
|
||||
|
||||
setup\<open>DOF_core.update_isa_global("typ" ,ISA_core.ML_isa_check_typ) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("term" ,ISA_core.ML_isa_check_term) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("thm" ,ISA_core.ML_isa_check_thm) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("file" ,ISA_core.ML_isa_check_file) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("docitem",ISA_core.ML_isa_check_docitem)\<close>
|
||||
setup\<open>DOF_core.update_isa_global("typ" ,ISA_core.ML_isa_check_typ) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("term" ,ISA_core.ML_isa_check_term) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("term_repr",fn _ => fn (t,_,_) => SOME t) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("thm" ,ISA_core.ML_isa_check_thm) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("file" ,ISA_core.ML_isa_check_file) \<close>
|
||||
setup\<open>DOF_core.update_isa_global("docitem" ,ISA_core.ML_isa_check_docitem)\<close>
|
||||
|
||||
|
||||
section\<open> Syntax for Annotated Documentation Commands (the '' View'' Part I) \<close>
|
||||
|
|
@ -830,10 +872,6 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) =
|
|||
| SOME(cid,_) => DOF_core.name2doc_class_name thy cid
|
||||
val cid_txt = "type = " ^ (enclose "{" "}" cid_long);
|
||||
|
||||
(* TODO: temp. hack *)
|
||||
fun unquote_string s = if String.isPrefix "''" s then
|
||||
String.substring(s,2,(String.size s)-4)
|
||||
else s
|
||||
fun ltx_of_term _ (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t')
|
||||
= (HOLogic.dest_string (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t'))
|
||||
| ltx_of_term _ (@{term "numeral :: _ \<Rightarrow> _"} $ t) = Int.toString(HOLogic.dest_numeral t)
|
||||
|
|
@ -951,8 +989,7 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list)
|
|||
fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t
|
||||
fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT S) (t)
|
||||
fun read_assn (lhs, pos:Position.T, opr, rhs) term =
|
||||
let val info_opt = DOF_core.get_attribute_info cid_long
|
||||
(Long_Name.base_name lhs) thy
|
||||
let val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy
|
||||
val (ln,lnt,lnu,lnut) = case info_opt of
|
||||
NONE => error ("unknown attribute >"
|
||||
^((Long_Name.base_name lhs))
|
||||
|
|
@ -962,9 +999,9 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list)
|
|||
(typ --> typ)
|
||||
--> cid_ty --> cid_ty)
|
||||
val tyenv = Sign.typ_match thy ((generalize_typ 0)(type_of rhs), lnt) (Vartab.empty)
|
||||
handle Type.TYPE_MATCH => error ("type of attribute: " ^ ln
|
||||
handle Type.TYPE_MATCH => (error ("type of attribute: " ^ ln
|
||||
^ " does not fit to term: "
|
||||
^ toString rhs);
|
||||
^ toString rhs));
|
||||
val tyenv' = (map (fn (s,(t,u)) => ((s,t),u)) (Vartab.dest tyenv))
|
||||
val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then ()
|
||||
else error("illegal notation for attribute of "^cid_long)
|
||||
|
|
@ -1019,7 +1056,6 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
|
|||
end
|
||||
in (moid,map check_for_cid indexed_autoS) end
|
||||
val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab)
|
||||
fun markup2string x = XML.content_of (YXML.parse_body x)
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
||||
Syntax.read_term_global thy rhs)
|
||||
val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
|
||||
|
|
@ -1058,7 +1094,6 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy =
|
|||
fun conv (na, _(*ty*), term) = (Binding.name_of na, Binding.pos_of na, "=", term);
|
||||
val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
|
||||
val (defaults, _(*ty*), _) = calc_update_term thy cid_long S defaults_init;
|
||||
fun markup2string x = XML.content_of (YXML.parse_body x)
|
||||
fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs)
|
||||
val assns' = map conv_attrs doc_attrs
|
||||
val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults
|
||||
|
|
@ -1089,14 +1124,14 @@ fun update_instance_command (((oid:string,pos),cid_pos),
|
|||
val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long
|
||||
then ()
|
||||
else error("incompatible classes:"^cid^":"^cid_long)
|
||||
fun markup2string x = XML.content_of (YXML.parse_body x)
|
||||
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
||||
fun conv_attrs (((lhs, pos), opn), rhs) = ((markup2string lhs),pos,opn,
|
||||
Syntax.read_term_global thy rhs)
|
||||
val assns' = map conv_attrs doc_attrs
|
||||
val def_trans = #1 o (calc_update_term thy cid_long assns')
|
||||
val def_trans = (#1 o (calc_update_term thy cid_long assns'))
|
||||
fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false}
|
||||
o Context.Theory ) thy ; thy)
|
||||
o Context.Theory ) thy ;
|
||||
thy)
|
||||
in
|
||||
thy |> DOF_core.update_value_global oid (def_trans)
|
||||
|> check_inv
|
||||
|
|
@ -1158,7 +1193,8 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
|||
let val {monitor_tab,...} = DOF_core.get_data_global thy
|
||||
fun check_if_final aS = let val i = find_index (not o RegExpInterface.final) aS
|
||||
in if i >= 0
|
||||
then error("monitor number "^Int.toString i^" not in final state.")
|
||||
then msg thy ("monitor number "^Int.toString i^
|
||||
" not in final state.")
|
||||
else ()
|
||||
end
|
||||
val _ = case Symtab.lookup monitor_tab oid of
|
||||
|
|
@ -1283,30 +1319,21 @@ val _ =
|
|||
(attributes_upd >> (Toplevel.theory o update_instance_command));
|
||||
|
||||
|
||||
fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),some_name:string option),modes : string list),
|
||||
fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list),
|
||||
prop) =
|
||||
let fun markup2string x = XML.content_of (YXML.parse_body x)
|
||||
fun parse_convert thy = (let val ctxt = (Proof_Context.init_global thy)
|
||||
val term = Syntax.parse_term ctxt prop
|
||||
val str = Sledgehammer_Util.hackish_string_of_term ctxt term
|
||||
fun hpp x = if x = #"\\" then "\\\\" else String.implode [x]
|
||||
val str' = map hpp (String.explode str)
|
||||
val str'' = String.concatWith " " str'
|
||||
in str''
|
||||
end)
|
||||
val _ = writeln ("XXX" ^ markup2string prop)
|
||||
fun conv_attrs thy = (("property",pos),"[@{term ''"^markup2string prop ^"''}]")::doc_attrs
|
||||
let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy))
|
||||
fun conv_attrs thy = (("property",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]")
|
||||
::doc_attrs
|
||||
(* fun conv_attrs thy = (("property",pos),"[@{term ''"^parse_convert thy ^"''}]")::doc_attrs *)
|
||||
fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy)
|
||||
fun mks thy = case DOF_core.get_object_global oid thy of
|
||||
SOME _ => (writeln "SOME"; update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
|
||||
| NONE => (writeln "NONE"; create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy)
|
||||
val check = (assert_cmd some_name modes prop) o Proof_Context.init_global
|
||||
fun mks thy = case DOF_core.get_object_global_opt oid thy of
|
||||
SOME NONE => (error("update of declared but not created doc_item:" ^ oid))
|
||||
| SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
|
||||
| NONE => (create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy)
|
||||
val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global
|
||||
in
|
||||
(* Toplevel.keep (check o Toplevel.context_of) *)
|
||||
Toplevel.theory (fn thy => (check thy;
|
||||
(* writeln ("YYY" ^ parse_convert thy); *)
|
||||
mks thy))
|
||||
Toplevel.theory (fn thy => (check thy; mks thy))
|
||||
end
|
||||
|
||||
val _ =
|
||||
|
|
@ -1680,6 +1707,17 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []);
|
|||
\<close>
|
||||
*)
|
||||
|
||||
lemma X : "True" oops
|
||||
|
||||
ML\<open>
|
||||
|
||||
\<close>
|
||||
(*
|
||||
ML\<open>
|
||||
val h = bstring_to_holstring @{context} (Syntax.string_of_term @{context} @{term "A \<longrightarrow> A"});
|
||||
holstring_to_bstring @{context} h
|
||||
\<close>
|
||||
*)
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ text\<open>A real example fragment from a larger project, declaring a text-eleme
|
|||
|
||||
text*[new_ass::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close>
|
||||
|
||||
text*[ass122::srac] \<open> The overall sampling frequence of the odometer
|
||||
text*[ass122::SRAC] \<open> The overall sampling frequence of the odometer
|
||||
subsystem is therefore 14 khz, which includes sampling, computing and
|
||||
result communication times... \<close>
|
||||
|
||||
|
|
@ -54,7 +54,7 @@ text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
|||
text \<open> the @{docref \<open>t10\<close>}
|
||||
as well as the @{docref \<open>ass122\<close>}\<close>
|
||||
text \<open> represent a justification of the safety related applicability
|
||||
condition @{srac \<open>ass122\<close>} aka exported constraint @{ec \<open>ass122\<close>}.\<close>
|
||||
condition @{SRAC \<open>ass122\<close>} aka exported constraint @{EC \<open>ass122\<close>}.\<close>
|
||||
|
||||
|
||||
|
||||
|
|
@ -65,11 +65,8 @@ declare_reference* [lalala::requirement, alpha="main", beta=42]
|
|||
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
section*[h::example]\<open> Some global inspection commands for the status of docitem and doc-class tables ... \<close>
|
||||
|
||||
section*[h::example]\<open> Some global inspection commands for the status of docitem and
|
||||
doc-class tables ... \<close>
|
||||
|
||||
|
||||
section*[i::example]\<open> Text Antiquotation Infrastructure ... \<close>
|
||||
|
|
@ -79,7 +76,7 @@ text\<open> @{docitem (unchecked) \<open>lalala\<close>} -- produces no warning.
|
|||
|
||||
text\<open> @{docitem \<open>ass122\<close>} -- global reference to a text-item in another file. \<close>
|
||||
|
||||
text\<open> @{ec \<open>ass122\<close>} -- global reference to a exported constraint in another file.
|
||||
text\<open> @{EC \<open>ass122\<close>} -- global reference to a exported constraint in another file.
|
||||
Note that the link is actually a srac, which, according to
|
||||
the ontology, happens to be an "ec". \<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -16,18 +16,37 @@ section\<open>Definitions, Lemmas, Theorems, Assertions\<close>
|
|||
text*[aa::F, property = "[@{term ''True''}]"]\<open>Our definition of the HOL-Logic has the following properties:\<close>
|
||||
assert*[aa::F] "True"
|
||||
|
||||
ML\<open> ISA_core.property_list_dest @{docitem_attribute property :: aa}\<close>
|
||||
|
||||
assert*[aa::F] "True --> True" (* small pb: unicodes crashes here ... *)
|
||||
(* sample for accessing a property filled with previous assert's of "aa" *)
|
||||
ML\<open> ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};\<close>
|
||||
|
||||
assert*[aa::F] " X \<and> Y \<longrightarrow> True" (*example with uni-code *)
|
||||
ML\<open> ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};
|
||||
app writeln (tl (rev it));\<close>
|
||||
|
||||
assert*[aa::F] "\<forall>x::bool. X \<and> Y \<longrightarrow> True" (*problem with uni-code *)
|
||||
|
||||
ML\<open>
|
||||
Syntax.read_term_global @{theory} "[@{termrepr ''True @<longrightarrow> True''}]";
|
||||
(* this only works because the isa check is not activated in "term" !!! *)
|
||||
@{term "[@{term '' True @<longrightarrow> True ''}]"}; (* with isa-check *)
|
||||
@{term "[@{termrepr '' True @<longrightarrow> True ''}]"}; (* without isa check *)
|
||||
\<close>
|
||||
|
||||
ML\<open>val [_,_,Const _ $ s,_] = (HOLogic.dest_list @{docitem_attribute property :: aa});
|
||||
val t = HOLogic.dest_string s;
|
||||
holstring_to_bstring @{context} t
|
||||
\<close>
|
||||
|
||||
lemma "All (\<lambda>x. X \<and> Y \<longrightarrow> True)" oops
|
||||
|
||||
ML\<open> ISA_core.property_list_dest @{docitem_attribute property :: aa}\<close>
|
||||
|
||||
text\<open>An example for the ontology specification character of the short-cuts such as
|
||||
@{command "assert*"}: in the following, we use the same notation referring to a completely
|
||||
different class. "F" and "assertion" have only in common that they posses the attribute
|
||||
\<^verbatim>\<open>property\<close>: \<close>
|
||||
|
||||
text*[aaa::assertion]\<open>Our definition of the integers has the following properties:\<close>
|
||||
text\<open>Creation just like that: \<close>
|
||||
assert*[aaa::assertion] "3 < (4::int)"
|
||||
assert*[aaa::assertion] "0 < (4::int)"
|
||||
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ 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*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
|
||||
... @{docitem \<open>c1\<close>} @{thm "refl"}\<close>
|
||||
... @{C \<open>c1\<close>} @{thm "refl"}\<close>
|
||||
|
||||
|
||||
update_instance*[d::D, a1 := X2]
|
||||
|
|
|
|||
|
|
@ -1053,8 +1053,77 @@ fun output ctxt prts =
|
|||
*)
|
||||
\<close>
|
||||
|
||||
chapter\<open>Front End \<close>
|
||||
text\<open>Introduction ... TODO\<close>
|
||||
chapter\<open>Front-End \<close>
|
||||
text\<open>In the following chapter, we turn to the right part of the system architecture
|
||||
shown in @{docitem \<open>architecture\<close>}:
|
||||
The PIDE ("Prover-IDE") layer consisting of a part written in SML and another in SCALA.
|
||||
Roughly speaking, PIDE implements "continuous build - continuous check" - functionality
|
||||
over a textual, albeit generic document model. It transforms user modifications
|
||||
of text elements in an instance of this model into increments (edits) and communicates
|
||||
them to the Isabelle system. The latter reacts by the creation of a multitude of light-weight
|
||||
reevaluation threads resulting in an asynchronous stream of markup that is used to annotate text
|
||||
elements. Such markup is used to highlight, e.g., variables
|
||||
or keywords with specific colors, to hyper-linking bound variables to their defining occurrences,
|
||||
or to annotate type-information to terms which becomes displayed by specific
|
||||
user-gestures on demand (hovering), etc.
|
||||
Note that PIDE is not an editor, it is the framework that
|
||||
coordinates these asynchronous information streams and optimizes it to a certain
|
||||
extent (outdated markup referring to modified text is dropped, and
|
||||
corresponding re-calculations are oriented to the user focus, for example).
|
||||
Four concrete editors --- also called PIDE applications --- have been implemented:
|
||||
\<^enum>an Eclipse plugin (developped by an Edinburg-group, based on an very old PIDE version),
|
||||
\<^enum>a Visual-Studio Code plugin (developed by Makarius Wenzel),
|
||||
currently based on a fairly old PIDE version,
|
||||
\<^enum>clide, a web-client supporting javascript and HTML5
|
||||
(developed by a group at University Bremen, based on a very old PIDE version), and
|
||||
\<^enum>the most commonly used: the plugin in JEdit - Editor,
|
||||
(developed by Makarius Wenzel, current PIDE version.)
|
||||
\<close>
|
||||
|
||||
text\<open>The document model forsees a number of text files, which are organized in form of an acyclic graph. Such graphs can be
|
||||
grouped into \<^emph>\<open>sessions\<close> and "frozen" to binaries in order to avoid long compilation
|
||||
times. Text files have an abstract name serving as identity (the mapping to file-paths
|
||||
in an underlying file-system is done in an own build management).
|
||||
The primary format of the text files is \<^verbatim>\<open>.thy\<close> (historically for: theory),
|
||||
secondary formats can be \<^verbatim>\<open>.sty\<close>,\<^verbatim>\<open>.tex\<close>, \<^verbatim>\<open>.png\<close>, \<^verbatim>\<open>.pdf\<close>, or other files processed
|
||||
by Isabelle and listed in a configuration processed by the build system.
|
||||
\<close>
|
||||
figure*[fig3::figure, relative_width="100",src="''figures/document-model''"]
|
||||
\<open>A Theory-Graph in the Document Model\<close>
|
||||
text\<open>A \<^verbatim>\<open>.thy\<close> file consists of a \<^emph>\<open>header\<close>, a \<^emph>\<open>context-definition\<close> and
|
||||
a \<^emph>\<open>body\<close> consisting of a sequence of \<^emph>\<open>commands\<close>. Even the header consists of
|
||||
a sequence of commands used for introductory text elements not depending on any context
|
||||
information (so: practically excluding any form of text antiquotation (see above)).
|
||||
The context-definition contains an \<^emph>\<open>import\<close> and a \<^emph>\<open>keyword\<close> section;
|
||||
for example:
|
||||
\begin{verbatim}
|
||||
theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||
imports Main
|
||||
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
||||
Assert
|
||||
|
||||
keywords "+=" ":=" "accepts" "rejects"
|
||||
\end{verbatim}
|
||||
where \<^verbatim>\<open>Isa_DOF\<close> is the abstract name of the text-file, \<^verbatim>\<open>Main\<close> etc. refer to imported
|
||||
text files (recall that the import relation must be acyclic). \<^emph>\<open>keyword\<close>s are used to separate
|
||||
commands form each other;
|
||||
predefined commands allow for the dynamic creation of new commands similarly
|
||||
to the definition of new functions in an interpreter shell (or: toplevel, see above.).
|
||||
A command starts with a pre-declared keyword and specific syntax of this command;
|
||||
the declaration of a keyword is only allowed in the same \<^verbatim>\<open>.thy\<close>-file where the
|
||||
the corresponding new command is defined. The semantics of the command is expressed
|
||||
in ML and consists of a @{ML_type "Toplevel.transition -> Toplevel.transition"}
|
||||
function. Thus, the Isar-toplevel supports the generic document model
|
||||
and allows for user-programmed extensions.
|
||||
\<close>
|
||||
|
||||
text\<open>Isabelle \<^verbatim>\<open>.thy\<close>-files were processed by two types of parsers:
|
||||
\<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed
|
||||
by a lexer-library and parser combinators built on top, and
|
||||
\<^enum> the "inner-syntax" (i.e. the syntax for @{term \<open>\<Lambda>\<close>} - terms)
|
||||
with an evolved, eight-layer parsing and pretty-printing process.
|
||||
\<close>
|
||||
|
||||
|
||||
section\<open>Basics: string, bstring and xstring\<close>
|
||||
text\<open>@{ML_type "string"} is the basic library type from the SML library
|
||||
|
|
@ -1063,12 +1132,12 @@ or require formats thereof introduced as type synonyms
|
|||
@{ML_type "bstring"} (defined in structure @{ML_structure "Binding"}
|
||||
and @{ML_type "xstring"} (defined in structure @{ML_structure "Name_Space"}.
|
||||
Unfortunately, the abstraction is not tight and combinations with
|
||||
elementary routines might produce quire crappy results.
|
||||
elementary routines might produce quite crappy results.
|
||||
\<close>
|
||||
|
||||
ML\<open>val b = Binding.name_of@{binding "here"}\<close>
|
||||
text\<open>... produces the system output \verb+val it = "here": bstring+,
|
||||
but note that it is trappy to believe it is just a string.
|
||||
but note that it is misleading to believe it is just a string.
|
||||
\<close>
|
||||
|
||||
ML\<open>String.explode b\<close> (* is harmless, but *)
|
||||
|
|
|
|||
|
|
@ -11,4 +11,6 @@ session "TR_mycommentedisabelle" = "Isabelle_DOF" +
|
|||
"figures/isabelle-architecture.pdf"
|
||||
"figures/pure-inferences-I.pdf"
|
||||
"figures/pure-inferences-II.pdf"
|
||||
"figures/document-model.pdf"
|
||||
|
||||
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -28,7 +28,7 @@ Safety assessment is focused on but not limited to the safety properties of a sy
|
|||
Definition*[assessor::concept, tag="''assessor''"]
|
||||
\<open>entity that carries out an assessment\<close>
|
||||
|
||||
Definition*[cots::concept, tag="''commercial off-the-shelf (COTS) software''"]
|
||||
Definition*[COTS::concept, tag="''commercial off-the-shelf software''"]
|
||||
\<open>software defined by market-driven need, commercially available and whose fitness for purpose
|
||||
has been demonstrated by a broad spectrum of commercial users\<close>
|
||||
|
||||
|
|
@ -44,7 +44,7 @@ criteria:
|
|||
(e. g. subsystems) which have an independent version
|
||||
\<close>
|
||||
|
||||
Definition*[cmgr::concept, tag="''configuration manager''"]
|
||||
Definition*[CMGR::concept, tag="''configuration manager''"]
|
||||
\<open>entity that is responsible for implementing and carrying out the processes
|
||||
for the configuration management of documents, software and related tools including
|
||||
\<^emph>\<open>change management\<close>\<close>
|
||||
|
|
@ -71,7 +71,7 @@ from the intended performance or behaviour (cf @{concept \<open>error\<close>})\
|
|||
Definition*[failure::concept]
|
||||
\<open>unacceptable difference between required and observed performance\<close>
|
||||
|
||||
Definition*[ft::concept, tag="''fault tolerance''"]
|
||||
Definition*[FT::concept, tag="''fault tolerance''"]
|
||||
\<open>built-in capability of a system to provide continued correct provision of service as specified,
|
||||
in the presence of a limited number of hardware or software faults\<close>
|
||||
|
||||
|
|
@ -79,7 +79,7 @@ Definition*[firmware::concept]
|
|||
\<open>software stored in read-only memory or in semi-permanent storage such as flash memory, in a
|
||||
way that is functionally independent of applicative software\<close>
|
||||
|
||||
Definition*[gen_soft::concept,tag="''generic software''"]
|
||||
Definition*[GS::concept,tag="''generic software''"]
|
||||
\<open>software which can be used for a variety of installations purely by the provision of
|
||||
application-specific data and/or algorithms\<close>
|
||||
|
||||
|
|
@ -231,27 +231,33 @@ NOTE Verification is mostly based on document reviews (design, implementation, t
|
|||
Definition*[verifier::concept]
|
||||
\<open>entity that is responsible for one or more verification activities\<close>
|
||||
|
||||
section\<open>Organization, Roles and Responsabilities\<close>
|
||||
text\<open>see also section \<^emph>\<open>Software management and organization\<close>.\<close>
|
||||
|
||||
datatype role = PM (* Program Manager *)
|
||||
| RQM (* Requirements Manager *)
|
||||
| DES (* Designer *)
|
||||
| IMP (* Implementer *)
|
||||
| ASR (* Assessor *)
|
||||
| Ne (* Integrator *)
|
||||
| INT (* Integrator *)
|
||||
| TST (* Tester *)
|
||||
| VER (* Verifier *)
|
||||
| VnV (* Verification and Validation *)
|
||||
| VAL (* Validator *)
|
||||
|
||||
|
||||
datatype phase = SR (* Software Requirement *)
|
||||
| SA (* Software Architecture *)
|
||||
| SDES (* Software Design *)
|
||||
| SCDES (* Software Component Design *)
|
||||
| CInT (* Component Implementation and Testing *)
|
||||
| SI (* Software Integration *)
|
||||
| SV (* Software Validation *)
|
||||
| SD (* Software Deployment *)
|
||||
| SM (* Software Maintenance *)
|
||||
|
||||
datatype phase = SYSDEV_ext (* System Development Phase (external) *)
|
||||
| SPl (* Software Planning *)
|
||||
| SR (* Software Requirement *)
|
||||
| SA (* Software Architecture *)
|
||||
| SDES (* Software Design *)
|
||||
| SCDES (* Software Component Design *)
|
||||
| CInT (* Component Implementation and Testing *)
|
||||
| SI (* Software Integration *)
|
||||
| SV (* Software Validation *)
|
||||
| SD (* Software Deployment *)
|
||||
| SM (* Software Maintenance *)
|
||||
|
||||
abbreviation software_requirement :: "phase" where "software_requirement \<equiv> SR"
|
||||
abbreviation software_architecture :: "phase" where "software_architecture \<equiv> SA"
|
||||
|
|
@ -264,24 +270,30 @@ abbreviation software_validation :: "phase" where "software_validation \<equi
|
|||
abbreviation software_deployment :: "phase" where "software_deployment \<equiv> SD"
|
||||
abbreviation software_maintenance :: "phase" where "software_maintenance \<equiv> SM"
|
||||
|
||||
term "SR"
|
||||
term "SR" (* meta-test *)
|
||||
|
||||
|
||||
section\<open>Objectives, Conformance and Software Integrity Levels\<close>
|
||||
|
||||
datatype sil = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
||||
|
||||
type_synonym saftety_integraytion_level = sil
|
||||
|
||||
|
||||
doc_class objectives =
|
||||
long_name :: "string option"
|
||||
is_concerned :: "role set"
|
||||
|
||||
|
||||
section\<open> Requirements-Analysis related Categories \<close>
|
||||
|
||||
doc_class requirement =
|
||||
doc_class requirement = text_element +
|
||||
long_name :: "string option"
|
||||
is_concerned :: "role set"
|
||||
|
||||
|
||||
(*
|
||||
doc_class requirement_analysis =
|
||||
no :: "nat"
|
||||
accepts "\<lbrace>requirement\<rbrace>\<^sup>+"
|
||||
|
||||
*)
|
||||
|
||||
text\<open>The category @{emph \<open>hypothesis\<close>} is used for assumptions from the
|
||||
foundational mathematical or physical domain, so for example:
|
||||
|
|
@ -304,12 +316,21 @@ doc_class hypothesis = requirement +
|
|||
text\<open> The following sub-class of security related hypothesis might comprise, for example:
|
||||
\<^item> @{term "P \<noteq> NP"},
|
||||
\<^item> or the computational hardness of certain functions
|
||||
relevant for cryptography (like prime-factorization).\<close>
|
||||
relevant for cryptography (like prime-factorization).
|
||||
(* speculation bu, not 50128 *)\<close>
|
||||
|
||||
doc_class security_hyp = hypothesis +
|
||||
hyp_type :: hyp_type <= physical (* default *)
|
||||
|
||||
|
||||
doc_class FnI = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
type_synonym functions_and_interfaces = FnI
|
||||
|
||||
doc_class AC = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
type_synonym application_conditions = AC
|
||||
|
||||
text\<open>The category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions. It has formal, semi-formal
|
||||
and informal sub-categories. They have to be tracked and discharged by appropriate
|
||||
validation procedures within a certification process, by it by test or proof. \<close>
|
||||
|
|
@ -319,24 +340,282 @@ datatype ass_kind = informal | semiformal | formal
|
|||
doc_class assumption = requirement +
|
||||
assumption_kind :: ass_kind <= informal
|
||||
|
||||
text\<open> The category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short) is used for formal assumptions, ... \<close>
|
||||
text\<open> The category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>EC\<close> for short) is used for formal application
|
||||
conditions; They represent in particular \<^emph>\<open>derived constraints\<close>, i.e. constraints that arrive
|
||||
as side-conditions during refinement proofs or implementation decisions and must be tracked.\<close>
|
||||
|
||||
doc_class ec = assumption +
|
||||
doc_class EC = AC +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
type_synonym exported_constraint = EC
|
||||
|
||||
text\<open> The category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>srac\<close> for short) is used ... \<close>
|
||||
text\<open> The category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>SRAC\<close> for short) is used
|
||||
for exported constraints assuring in judgements safety requirements of the system. \<close>
|
||||
|
||||
doc_class srac = ec +
|
||||
doc_class SRAC = EC +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
type_synonym safety_related_application_condition = SRAC
|
||||
|
||||
doc_class timing = ec +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
doc_class energy = ec +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
doc_class CoAS = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
type_synonym configuration_or_architecture_of_system = CoAS
|
||||
|
||||
doc_class security = ec +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
doc_class HtbC = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
type_synonym hazard_to_be_controlled = HtbC
|
||||
|
||||
doc_class SIR = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
type_synonym safety_integrity_requirement = SIR
|
||||
|
||||
text\<open>The following class is a bit unclear about usage and seems to be in
|
||||
conceptual mismatch with @{typ objectives}: \<close>
|
||||
doc_class SILA = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
alloc :: "sil" <= "SIL0"
|
||||
type_synonym allocation_of_SIL = SILA
|
||||
|
||||
doc_class TC = requirement +
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
type_synonym timing_constraint = TC
|
||||
|
||||
section\<open>Software Assurance related Entities and Concepts\<close>
|
||||
|
||||
|
||||
text{* subcategories are : *}
|
||||
text\<open>Table A.5: Verification and Testing\<close>
|
||||
datatype vnt_technique =
|
||||
formal_proof
|
||||
| stat_analysis
|
||||
| dyn_analysis (* Refinedin Table A.13:
|
||||
-- Test Case Execution from Boundary Analysis
|
||||
-- Test Case Execution from Error Guessing
|
||||
-- Test Case Execution from Error Seeding
|
||||
-- Performance Modeling
|
||||
-- Equivalence Classes and Input Partition Testing
|
||||
-- Structure-Based Testing
|
||||
*)
|
||||
| metrics
|
||||
| traceability
|
||||
| sw_error_effect_analysis
|
||||
| test_coverage_for_code
|
||||
| functional_testing
|
||||
(* Refined in Table A.14:
|
||||
-- Test Case Execution from Cause Consequence Diagrams
|
||||
-- Prototyping / Animation
|
||||
-- Boundary Value Analysis
|
||||
-- Equivalence Classes and Input Partition Testing
|
||||
-- Process Simulation
|
||||
*)
|
||||
| perf_testing
|
||||
| interface_testing
|
||||
| model_based_testing (* 'modeling' unclear *)
|
||||
|
||||
type_synonym verification_and_testing_technique = vnt_technique
|
||||
|
||||
datatype test_coverage_criterion =
|
||||
allpathk nat nat (* depth, test_coverage_degree *)
|
||||
| mcdc nat (* depth, test_coverage_degree *)
|
||||
| exhaustive
|
||||
| dnf_E_d string nat (* equivalence class testing *)
|
||||
| other string
|
||||
|
||||
text\<open>The objective of software verification is to examine and arrive at a \<^emph>\<open>judgement\<close> based on
|
||||
\<^emph>\<open>evidence\<close> that output items (process, documentation, software or application) of a specific
|
||||
development phase fulfil the requirements and plans with respect to completeness, correctness
|
||||
and consistency. \<close>
|
||||
doc_class judgement =
|
||||
evidence :: "vnt_technique list"
|
||||
is_concerned :: "role set" <= "{VER,ASR,VAL}"
|
||||
|
||||
section\<open> Design and Test Documents \<close>
|
||||
|
||||
doc_class cenelec_text = text_element +
|
||||
phase :: "phase"
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
|
||||
|
||||
|
||||
doc_class SYSREQS = cenelec_text +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
accepts "\<lbrace>objectives||requirement||cenelec_text\<rbrace>\<^sup>+ "
|
||||
type_synonym system_requirements_specification = SYSREQS
|
||||
|
||||
doc_class SYSSREQS = cenelec_text +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
type_synonym system_safety_requirements_specification = SYSSREQS
|
||||
|
||||
doc_class SYSAD = cenelec_text +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
type_synonym system_architecture_description = SYSAD
|
||||
|
||||
doc_class SYSS_pl = cenelec_text +
|
||||
phase :: "phase" <= "SPl"
|
||||
type_synonym system_safety_plan = SYSS_pl
|
||||
|
||||
doc_class SYS_VnV_pl = cenelec_text +
|
||||
phase :: "phase" <= "SPl"
|
||||
type_synonym system_VnV_plan = SYS_VnV_pl
|
||||
|
||||
doc_class SWRS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_requirements_specification = SWRS
|
||||
|
||||
doc_class SWRVR = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_requirements_verification_report = SWRVR
|
||||
|
||||
|
||||
doc_class SWTS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_test_specification = SWTS
|
||||
|
||||
doc_class SWAS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_architecture_specification = SWAS
|
||||
|
||||
doc_class SWDS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_design_specification = SWDS
|
||||
|
||||
doc_class SWIS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_interface_specification = SWIS
|
||||
|
||||
doc_class SWITS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_integration_test_specification = SWITS
|
||||
|
||||
doc_class SWHITS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_hardware_integration_test_specification = SWHITS
|
||||
|
||||
doc_class SWADVR = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_architecture_and_design_verification_report = SWADVR
|
||||
|
||||
doc_class SWCDS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_component_design_specification = SWCDS
|
||||
|
||||
doc_class SWCTS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_component_test_specification = SWCTS
|
||||
|
||||
doc_class SWCDVR = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_component_design_verification_report = SWCDVR
|
||||
|
||||
|
||||
doc_class SWSCD = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_source_code_and_documentation = SWSCD
|
||||
|
||||
doc_class SWCTR = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_component_test_report = SWCTR
|
||||
|
||||
doc_class SWSCVR = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_source_code_verification_report = SWSCVR
|
||||
|
||||
doc_class SWHAITR = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_hardware_integration_test_report = SWHAITR
|
||||
|
||||
doc_class SWIVR = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_integration_verification_report = SWIVR
|
||||
|
||||
doc_class SWTR_global = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym overall_software_test_report = SWTR_global
|
||||
|
||||
doc_class SWVALR = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_validation_report = SWVALR
|
||||
|
||||
doc_class SWDD = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_deployment_documents = SWDD
|
||||
|
||||
doc_class SWMD = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_maintenance_documents = SWMD
|
||||
|
||||
|
||||
section\<open> Software Assurance \<close>
|
||||
|
||||
subsection\<open> Software Testing \<close>
|
||||
text\<open>Objective:
|
||||
The objective of software testing, as performed by the Tester and/or Integrator,
|
||||
is to ascertain the behaviour or performance of software against the corresponding test
|
||||
specification to the extent achievable by the selected test coverage.
|
||||
\<close>
|
||||
|
||||
text\<open>Outputs:
|
||||
\<^enum> @{typ overall_software_test_report}
|
||||
\<^enum> @{typ software_test_specification} Overall Software Test Specification
|
||||
\<^enum> Overall Software Test Report
|
||||
\<^enum> Software Integration Test Specification
|
||||
\<^enum> Software Integration Test Report
|
||||
\<^enum> Software/Hardware Integration Test Specification
|
||||
\<^enum> Software/Hardware Integration Test Report
|
||||
\<^enum> Software Component Test Specification
|
||||
\<^enum> Software Component Test Report
|
||||
\<close>
|
||||
|
||||
subsection\<open> Software Verification \<close>
|
||||
text\<open>Objective:
|
||||
The objective of software verification is to examine and arrive at a judgement based on evidence
|
||||
that output items (process, documentation, software or application) of a specific development
|
||||
phase fulfil the requirements and plans with respect to completeness, correctness and consistency.
|
||||
These activities are managed by the @{concept \<open>verifier\<close>}.
|
||||
\<close>
|
||||
|
||||
text\<open>Outputs:
|
||||
\<^enum> Software Verification Plan
|
||||
\<^enum> Software Verification Report(s)
|
||||
\<^enum> Software Quality Assurance Verification Report
|
||||
\<close>
|
||||
|
||||
subsection\<open> Software Validation \<close>
|
||||
text\<open>Objective:
|
||||
\<^enum>The objective of software validation is to demonstrate that the processes and their outputs are
|
||||
such that the software is of the defined software safety integrity level, fulfils the software
|
||||
requirements and is fit for its intended application. This activity is performed by the Validator.
|
||||
\<^enum>The main validation activities are to demonstrate by analysis and/or testing that all the software
|
||||
requirements are specified, implemented, tested and fulfilled as required by the applicable SIL,
|
||||
and to evaluate the safety criticality of all anomalies and non-conformities based on the results
|
||||
of reviews, analyses and tests.
|
||||
\<close>
|
||||
text\<open>Output documents:
|
||||
\<^enum> Software Validation Plan
|
||||
\<^enum> Software Validation Report
|
||||
\<^enum> Software Validation Verification Report
|
||||
\<close>
|
||||
|
||||
subsection\<open> Software Assessment \<close> (* other word for : formal evaluation. *)
|
||||
text\<open>Objective:
|
||||
\<^enum>To evaluate that the lifecycle processes and their outputs are such that the software is of the
|
||||
defined software safety integrity levels 1-4 andis fit for its intended application.
|
||||
\<^enum> For SIL 0 software, requirements of this standard shall be fulfilled but where a certificate stating
|
||||
compliance with EN ISO 9001 is available, no assessment will be required.
|
||||
\<close>
|
||||
|
||||
subsection\<open> Software Quality Assurance \<close>
|
||||
text\<open>Objectives: To identify, monitor and control all those activities, both technical and
|
||||
managerial, which are necessary to ensure that the software achieves the quality required.
|
||||
This is necessary to provide the required qualitative defence against systematic faults and
|
||||
to ensure that an audit trail can be established to allow
|
||||
verification and validation activities to be undertaken effectively.\<close>
|
||||
(* So : pretty much META *)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* DEATH ZONE FROM HERE ... >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> *)
|
||||
|
||||
|
||||
section\<open> Design related Categories \<close>
|
||||
|
|
@ -354,23 +633,11 @@ section\<open> Requirements-Analysis related Categories \<close>
|
|||
|
||||
doc_class test_item =
|
||||
nn :: "string option"
|
||||
|
||||
text{* subcategories are : *}
|
||||
|
||||
datatype test_kind = blackbox | whitebox | greybox | fuzz | pertubation
|
||||
|
||||
datatype test_coverage_criterion =
|
||||
allpathk nat nat (* depth, test_coverage_degree *)
|
||||
| mcdc nat (* depth, test_coverage_degree *)
|
||||
| exhaustive
|
||||
| dnf_E_d string nat (* equivalence class testing *)
|
||||
| other string
|
||||
|
||||
doc_class test_specification = test_item +
|
||||
short_goal :: string
|
||||
|
||||
doc_class test_case = test_item +
|
||||
kind :: test_kind
|
||||
descr :: string
|
||||
|
||||
doc_class test_result = test_item +
|
||||
|
|
@ -403,21 +670,22 @@ doc_class test_documentation =
|
|||
|
||||
|
||||
|
||||
section\<open> Testing and Validation \<close>
|
||||
section\<open> META : Testing and Validation \<close>
|
||||
|
||||
text\<open>Test : @{concept \<open>cots\<close>}\<close>
|
||||
|
||||
text\<open>Test : @{concept \<open>COTS\<close>}\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
DOF_core.name2doc_class_name @{theory} "requirement";
|
||||
DOF_core.name2doc_class_name @{theory} "srac";
|
||||
DOF_core.is_defined_cid_global "srac" @{theory};
|
||||
DOF_core.is_defined_cid_global "ec" @{theory};
|
||||
DOF_core.name2doc_class_name @{theory} "SRAC";
|
||||
DOF_core.is_defined_cid_global "SRAC" @{theory};
|
||||
DOF_core.is_defined_cid_global "EC" @{theory};
|
||||
"XXXXXXXXXXXXXXXXX";
|
||||
DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.ec";
|
||||
DOF_core.is_subclass @{context} "CENELEC_50128.srac" "CENELEC_50128.ec";
|
||||
DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.srac";
|
||||
DOF_core.is_subclass @{context} "CENELEC_50128.ec" "CENELEC_50128.test_requirement";
|
||||
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.EC";
|
||||
DOF_core.is_subclass @{context} "CENELEC_50128.SRAC" "CENELEC_50128.EC";
|
||||
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.SRAC";
|
||||
DOF_core.is_subclass @{context} "CENELEC_50128.EC" "CENELEC_50128.test_requirement";
|
||||
"XXXXXXXXXXXXXXXXX";
|
||||
val {docobj_tab={maxano, tab=ref_tab},docclass_tab=class_tab,...} = DOF_core.get_data @{context};
|
||||
Symtab.dest ref_tab;
|
||||
|
|
@ -428,7 +696,7 @@ Symtab.dest class_tab;
|
|||
ML\<open>
|
||||
"XXXXXXXXXXXXXXXXX";
|
||||
|
||||
DOF_core.get_attributes_local "srac" @{context};
|
||||
DOF_core.get_attributes_local "SRAC" @{context};
|
||||
|
||||
@{term assumption_kind}
|
||||
\<close>
|
||||
|
|
|
|||
|
|
@ -22,18 +22,18 @@ doc_class abstract =
|
|||
keywordlist :: "string list" <= "[]"
|
||||
principal_theorems :: "thm list"
|
||||
|
||||
doc_class text_section =
|
||||
doc_class text_section = text_element +
|
||||
main_author :: "author option" <= None
|
||||
fixme_list :: "string list" <= "[]"
|
||||
level :: "int option" <= "None"
|
||||
(* this attribute enables doc-notation support section* etc.
|
||||
we follow LaTeX terminology on levels
|
||||
part = Some -1
|
||||
chapter = Some 0
|
||||
section = Some 1
|
||||
subsection = Some 2
|
||||
subsubsection = Some 3
|
||||
... *)
|
||||
(* this attribute enables doc-notation support section* etc.
|
||||
we follow LaTeX terminology on levels
|
||||
part = Some -1
|
||||
chapter = Some 0
|
||||
section = Some 1
|
||||
subsection = Some 2
|
||||
subsubsection = Some 3
|
||||
... *)
|
||||
(* for scholarly paper: invariant level > 0 *)
|
||||
|
||||
doc_class introduction = text_section +
|
||||
|
|
|
|||
|
|
@ -0,0 +1,150 @@
|
|||
section{* An example ontology for a math paper*}
|
||||
|
||||
theory small_math
|
||||
imports "../Isa_COL"
|
||||
begin
|
||||
|
||||
doc_class title =
|
||||
short_title :: "string option" <= "None"
|
||||
|
||||
doc_class author =
|
||||
email :: "string" <= "''''"
|
||||
|
||||
datatype classification = algebra | geometry | graph_theory
|
||||
|
||||
doc_class abstract =
|
||||
keyword_list :: "classification list" <= "[]"
|
||||
|
||||
doc_class text_section =
|
||||
authored_by :: "author set" <= "{}"
|
||||
level :: "int option" <= "None"
|
||||
(* this attribute enables doc-notation support section* etc.
|
||||
we follow LaTeX terminology on levels
|
||||
part = Some -1
|
||||
chapter = Some 0
|
||||
section = Some 1
|
||||
subsection = Some 2
|
||||
subsubsection = Some 3
|
||||
... *)
|
||||
(* for scholarly paper: invariant level > 0 *)
|
||||
|
||||
type_synonym notion = string
|
||||
|
||||
doc_class introduction = text_section +
|
||||
uses :: "notion set"
|
||||
|
||||
doc_class contribution_claim = introduction +
|
||||
based_on :: "notion list"
|
||||
|
||||
doc_class technical = text_section +
|
||||
formal_results :: "thm list"
|
||||
|
||||
doc_class "definition" = technical +
|
||||
is_formal :: "bool"
|
||||
property :: "term list" <= "[]"
|
||||
|
||||
datatype kind = expert_opinion | argument | "proof"
|
||||
|
||||
doc_class result = technical +
|
||||
evidence :: kind
|
||||
property :: "thm list" <= "[]"
|
||||
|
||||
doc_class example = technical +
|
||||
referring_to :: "(notion + definition) set" <= "{}"
|
||||
|
||||
doc_class "conclusion" = text_section +
|
||||
establish :: "(contribution_claim \<times> result) set"
|
||||
|
||||
text\<open> Besides subtyping, there is another relation between
|
||||
doc_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
|
||||
which is expressed by occurrence in the where clause.
|
||||
While sub-classing refers to data-inheritance of attributes,
|
||||
a monitor captures structural constraints -- the order --
|
||||
in which instances of monitored classes may occur.
|
||||
|
||||
The control of monitors is done by the commands:
|
||||
\<^item> \<^verbatim>\<open> monitor <oid::class_type, <attributes-defs> > \<close>
|
||||
\<^item> \<^verbatim>\<open> close_monitor <oid[::class_type],<attributes-updates>> \<close>
|
||||
|
||||
where the automaton of the monitor class is expected
|
||||
to be in a final state.
|
||||
|
||||
Monitors can be nested.
|
||||
|
||||
Classes neither directly or indirectly (via inheritance)
|
||||
mentioned in the monitor clause are \<^emph>\<open>independent\<close> from
|
||||
the monitor and may occur freely, \ie{} in arbitrary order.n \<close>
|
||||
|
||||
|
||||
text \<open>underlying idea: a monitor class automatically receives a
|
||||
\<^verbatim>\<open>trace\<close> attribute in which a list of observed class-ids is maintained.
|
||||
The \<^verbatim>\<open>trace\<close> is a \<^emph>\<open>`predefined id`\<close> like \<^verbatim>\<open>main\<close> in C. It can be accessed
|
||||
like any other attribute of a class instance, \ie{} a document item.\<close>
|
||||
|
||||
doc_class article =
|
||||
style_id :: string <= "''LNCS''"
|
||||
accepts "(title ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ abstract ~~
|
||||
\<lbrace>introduction\<rbrace>\<^sup>+ ~~ \<lbrace>technical || example\<rbrace>\<^sup>+ ~~ \<lbrace>conclusion\<rbrace>\<^sup>+)"
|
||||
|
||||
|
||||
ML\<open>
|
||||
structure Small_Math_trace_invariant =
|
||||
struct
|
||||
local
|
||||
|
||||
fun group f g cidS [] = []
|
||||
|group f g cidS (a::S) = case find_first (f a) cidS of
|
||||
NONE => [a] :: group f g cidS S
|
||||
| SOME cid => let val (pref,suff) = take_prefix (g cid) S
|
||||
in (a::pref)::(group f g cidS suff) end;
|
||||
|
||||
fun partition ctxt cidS trace =
|
||||
let fun find_lead (x,_) = DOF_core.is_subclass ctxt x;
|
||||
fun find_cont cid (cid',_) = DOF_core.is_subclass ctxt cid' cid
|
||||
in group find_lead find_cont cidS trace end;
|
||||
|
||||
fun dest_option _ (Const (@{const_name "None"}, _)) = NONE
|
||||
| dest_option f (Const (@{const_name "Some"}, _) $ t) = SOME (f t)
|
||||
|
||||
in
|
||||
|
||||
fun check ctxt cidS mon_id pos =
|
||||
let val trace = AttributeAccess.compute_trace_ML ctxt mon_id pos @{here}
|
||||
val groups = partition (Context.proof_of ctxt) cidS trace
|
||||
fun get_level_raw oid = AttributeAccess.compute_attr_access ctxt "level" oid @{here} @{here};
|
||||
fun get_level oid = dest_option (snd o HOLogic.dest_number) (get_level_raw (oid));
|
||||
fun check_level_hd a = case (get_level (snd a)) of
|
||||
NONE => error("Invariant violation: leading section" ^ snd a ^
|
||||
" must have lowest level")
|
||||
| SOME X => X
|
||||
fun check_group_elem level_hd a = case (get_level (snd a)) of
|
||||
NONE => true
|
||||
| SOME y => if level_hd <= y then true
|
||||
(* or < ? But this is too strong ... *)
|
||||
else error("Invariant violation: "^
|
||||
"subsequent section " ^ snd a ^
|
||||
" must have higher level.");
|
||||
fun check_group [] = true
|
||||
|check_group [_] = true
|
||||
|check_group (a::S) = forall (check_group_elem (check_level_hd a)) (S)
|
||||
in if forall check_group groups then ()
|
||||
else error"Invariant violation: leading section must have lowest level"
|
||||
end
|
||||
end
|
||||
|
||||
end
|
||||
\<close>
|
||||
|
||||
setup\<open> let val cidS = ["small_math.introduction","small_math.technical", "small_math.conclusion"];
|
||||
fun body moni_oid _ ctxt = (Small_Math_trace_invariant.check ctxt cidS moni_oid @{here};
|
||||
true)
|
||||
in DOF_core.update_class_invariant "small_math.article" body end\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
gen_sty_template
|
||||
|
||||
|
||||
end
|
||||
|
||||
Loading…
Reference in New Issue