parent
9adfeb6425
commit
33602282a0
|
@ -76,10 +76,12 @@ ML\<open>fun check_M_invariant oid {is_monitor} ctxt =
|
||||||
|
|
||||||
setup\<open>DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\<close>
|
setup\<open>DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\<close>
|
||||||
|
|
||||||
open_monitor*[struct::M]
|
|
||||||
|
|
||||||
|
section\<open>Example: Monitor Class Invariant\<close>
|
||||||
|
|
||||||
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
open_monitor*[struct::M]
|
||||||
|
|
||||||
|
subsection*[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*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||||
|
|
||||||
|
@ -87,7 +89,7 @@ text*[d1::E, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede sus
|
||||||
|
|
||||||
text*[c2:: C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer... \<close>
|
text*[c2:: C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer... \<close>
|
||||||
|
|
||||||
section*[f::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
subsection*[f::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||||
|
|
||||||
(* test : close_monitor should fail :
|
(* test : close_monitor should fail :
|
||||||
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||||
|
@ -97,8 +99,6 @@ ML\<open>val term = AttributeAccess.compute_attr_access (Context.Proof @{context
|
||||||
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
|
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 string_pair_list = map conv (HOLogic.dest_list term)
|
||||||
\<close>
|
\<close>
|
||||||
(* trace example *)
|
|
||||||
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
|
|
||||||
|
|
||||||
|
|
||||||
close_monitor*[struct]
|
close_monitor*[struct]
|
||||||
|
|
|
@ -41,9 +41,11 @@ text*[abs::abstract,
|
||||||
|
|
||||||
Sufficiently annotated, large documents are easier to be developed collaboratively
|
Sufficiently annotated, large documents are easier to be developed collaboratively
|
||||||
by continuously validating the \<^emph>\<open>coherence\<close> between formal and informal parts, and
|
by continuously validating the \<^emph>\<open>coherence\<close> between formal and informal parts, and
|
||||||
the impact of changes can be better tracked automatically.
|
the impact of changes can be better tracked automatically.
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
(* Industrial Application ? *)
|
||||||
|
|
||||||
|
|
||||||
(* Support of document ontologies is provided for immediate
|
(* Support of document ontologies is provided for immediate
|
||||||
user-feedback when editing large documents with formal and
|
user-feedback when editing large documents with formal and
|
||||||
|
@ -51,24 +53,55 @@ text*[abs::abstract,
|
||||||
\eg, deliverables in a certified software engineering
|
\eg, deliverables in a certified software engineering
|
||||||
process. *)
|
process. *)
|
||||||
|
|
||||||
|
(*
|
||||||
|
@inproceedings{DBLP:conf/mkm/BlanchetteHMN15,
|
||||||
|
author = {Jasmin Christian Blanchette and
|
||||||
|
Maximilian P. L. Haslbeck and
|
||||||
|
Daniel Matichuk and
|
||||||
|
Tobias Nipkow},
|
||||||
|
title = {Mining the Archive of Formal Proofs},
|
||||||
|
booktitle = {Intelligent Computer Mathematics - International Conference, {CICM}
|
||||||
|
2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
|
||||||
|
pages = {3--17},
|
||||||
|
year = {2015},
|
||||||
|
crossref = {DBLP:conf/mkm/2015},
|
||||||
|
url = {https://doi.org/10.1007/978-3-319-20615-8\_1},
|
||||||
|
doi = {10.1007/978-3-319-20615-8\_1},
|
||||||
|
timestamp = {Fri, 02 Nov 2018 09:40:47 +0100},
|
||||||
|
biburl = {https://dblp.org/rec/bib/conf/mkm/BlanchetteHMN15},
|
||||||
|
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||||||
|
}
|
||||||
|
*)
|
||||||
section*[intro::introduction]\<open> Introduction \<close>
|
section*[intro::introduction]\<open> Introduction \<close>
|
||||||
text*[introtext::introduction]\<open>
|
text*[introtext::introduction]\<open>
|
||||||
|
With the maturation and growing power of interactive proof systems, the body of formalized
|
||||||
|
mathematics and engineering is dramatically increasing. The Isabelle Archive of Formal Proof (AFP),
|
||||||
|
for example, created in 2004, counted in 2015 the number of 215 articles
|
||||||
|
@{footnote \<open>... where "articles" are theory developments underlying a submission process
|
||||||
|
similar to the mizar journal \cite{}\<close>}, whereas the count stood at 413 only three years later.
|
||||||
|
An in-depth empirical analysis shows that both complexity and size increased accordingly
|
||||||
|
@{cite "DBLP:conf/mkm/BlanchetteHMN15"}. Since the entire AFP is part of the Isabelle regression
|
||||||
|
test suite and therefore maintained for the different releases, this body of knowledge is also
|
||||||
|
available in high technical consistency.
|
||||||
|
|
||||||
Given the body of formalized mathematics in
|
This raises a wider interest in the application of advanced "semantic Web" structuring, query
|
||||||
|
and mining techniques. Compared to other scientific disciplines like biology or medicine,
|
||||||
, for example the Isabelle/AFP
|
where large data-bases of genomes or scientific publications have been organized along
|
||||||
|
ontologies @{cite "..." and "..." } enabling queries, for example, there are still a number of
|
||||||
|
technical and social challenges to overcome in order to leverage this techniques in the
|
||||||
|
field of interactive theorem proving. \fixme{avoid ontology here.}
|
||||||
|
|
||||||
One of the main use of ontologies is annotation. Let us consider a set of entities available in
|
One of the main use of ontologies is annotation. Let us consider a set of entities available in
|
||||||
a given corpus. These entities may be sentences or paragraphs in a document, figures, tables,
|
a given corpus. These entities may be sentences or paragraphs in a document, figures, tables,
|
||||||
definitions or lemmas in a document, etc. By annotation, we denote the link that may exist between an ontology concept
|
definitions or lemmas in a document, etc. By annotation, we denote the link that may exist between
|
||||||
and a document element of the considered corpus.
|
an ontology concept and a document element of the considered corpus.
|
||||||
|
|
||||||
The annotation process consists in defining and running a set of rules leading to the production of annotations.
|
The annotation process consists in defining and running a set of rules leading to the production of
|
||||||
This process may be completely automated, semi-automatic with user validation or completely
|
annotations. This process may be completely automated, semi-automatic with user validation or completely
|
||||||
interactive.
|
interactive.
|
||||||
|
\<close>
|
||||||
IDEA: a table with conceptual properties
|
text\<open>
|
||||||
|
IDEA FOR RELATED WORK: a table with conceptual properties of ontology languages
|
||||||
Feature | Ontolingua | DAML+OIL | RDFS | OWL | PLIB | XML | Isa_ODL
|
Feature | Ontolingua | DAML+OIL | RDFS | OWL | PLIB | XML | Isa_ODL
|
||||||
------------------------------------------------------------------------
|
------------------------------------------------------------------------
|
||||||
granularity | Word | | | | | Character | sentence (word)
|
granularity | Word | | | | | Character | sentence (word)
|
||||||
|
@ -79,8 +112,8 @@ algebraic operators | | sets, lists,
|
||||||
Constraints | | ML, executable HOL
|
Constraints | | ML, executable HOL
|
||||||
CWA vs OWA | | OWA
|
CWA vs OWA | | OWA
|
||||||
Context Modeling | | Context import
|
Context Modeling | | Context import
|
||||||
Inheritance |
|
Inheritance | | SINGLE
|
||||||
Instantiation |
|
Instantiation | | MULTIPLE
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text*[intro_old::introduction]\<open>
|
text*[intro_old::introduction]\<open>
|
||||||
|
|
|
@ -35,9 +35,6 @@ text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions fro
|
||||||
\<^item> the Mordell-Lang conjecture holds,
|
\<^item> the Mordell-Lang conjecture holds,
|
||||||
\<^item> euklidian geometry is assumed, or
|
\<^item> euklidian geometry is assumed, or
|
||||||
\<^item> Newtonian (non-relativistic) physics is assumed,
|
\<^item> Newtonian (non-relativistic) physics is assumed,
|
||||||
\<^item> @{term "P \<noteq> NP"},
|
|
||||||
\<^item> or the computational hardness of certain functions
|
|
||||||
relevant for cryptography (like prime-factorization).
|
|
||||||
Their acceptance is inherently outside the scope of the model
|
Their acceptance is inherently outside the scope of the model
|
||||||
and can only established inside certification process by
|
and can only established inside certification process by
|
||||||
authority argument.
|
authority argument.
|
||||||
|
@ -48,10 +45,19 @@ datatype hyp_type = physical | mathematical | computational | other
|
||||||
|
|
||||||
typ "CENELEC_50126.requirement"
|
typ "CENELEC_50126.requirement"
|
||||||
|
|
||||||
|
|
||||||
doc_class hypothesis = requirement +
|
doc_class hypothesis = requirement +
|
||||||
hyp_type :: hyp_type <= physical (* default *)
|
hyp_type :: hyp_type <= physical (* default *)
|
||||||
|
|
||||||
|
text{* 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).
|
||||||
|
*}
|
||||||
|
|
||||||
|
doc_class security_hyp = hypothesis +
|
||||||
|
hyp_type :: hyp_type <= physical (* default *)
|
||||||
|
|
||||||
|
|
||||||
text{*The category @{emph \<open>assumption\<close>} is used for domain-specific assumptions.
|
text{*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
|
It has formal, semi-formal and informal sub-categories. They have to be
|
||||||
tracked and discharged by appropriate validation procedures within a
|
tracked and discharged by appropriate validation procedures within a
|
||||||
|
@ -79,6 +85,16 @@ text{*The category @{emph \<open>safety related application condition\<close>} (
|
||||||
doc_class srac = ec +
|
doc_class srac = ec +
|
||||||
assumption_kind :: ass_kind <= (*default *) formal
|
assumption_kind :: ass_kind <= (*default *) formal
|
||||||
|
|
||||||
|
doc_class timing = ec +
|
||||||
|
assumption_kind :: ass_kind <= (*default *) formal
|
||||||
|
|
||||||
|
doc_class energy = ec +
|
||||||
|
assumption_kind :: ass_kind <= (*default *) formal
|
||||||
|
|
||||||
|
doc_class security = ec +
|
||||||
|
assumption_kind :: ass_kind <= (*default *) formal
|
||||||
|
|
||||||
|
|
||||||
section {* Design related Categories *}
|
section {* Design related Categories *}
|
||||||
|
|
||||||
doc_class design_item =
|
doc_class design_item =
|
||||||
|
|
|
@ -31,10 +31,11 @@ doc_class E = D +
|
||||||
x :: "string" <= "''qed''" (* overriding default *)
|
x :: "string" <= "''qed''" (* overriding default *)
|
||||||
|
|
||||||
doc_class F =
|
doc_class F =
|
||||||
r :: "thm list"
|
property :: "term list"
|
||||||
u :: "file"
|
r :: "thm list"
|
||||||
s :: "typ list"
|
u :: "file"
|
||||||
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
s :: "typ list"
|
||||||
|
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
||||||
to an association class. It can be used to track
|
to an association class. It can be used to track
|
||||||
claims to result - relations, for example.*)
|
claims to result - relations, for example.*)
|
||||||
doc_class G = C +
|
doc_class G = C +
|
||||||
|
|
Loading…
Reference in New Issue