Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Added first somewhat realistic syntax on annotated text elements
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-07-17 21:10:18 +02:00
parent 1704c17776
commit c181c2851c
2 changed files with 125 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

142
examples/technical_report/IsaDof_Manual/03_GuidedTour.thy
View File

@ -153,6 +153,78 @@ text\<open> The document class \inlineisar+figure+ --- supported by the \isadof
such as @{docitem_ref \<open>fig_figures\<close>}.
\<close>
section*[cenelec_onto::example]\<open> The Certification Scenario following CENELEC \<close>
text\<open> Documents to be provided in formal certifications (such as CENELEC
50126/50128, the DO-178B/C, or Common Criteria) can much profit from the control of ontological consistency:
a lot of an evaluators work consists in tracing down the links from requirements over
assumptions down to elements of evidence, be it in the models, the code, or the tests.
In a certification process, traceability becomes a major concern; and providing
mechanisms to ensure complete traceability already at the development of the
global document will clearly increase speed and reduce risk and cost of a
certification process. Making the link-structure machine-checkable, be it between requirements,
assumptions, their implementation and their discharge by evidence (be it tests, proofs, or
authoritative arguments), is therefore natural and has the potential to decrease the cost
of developments targeting certifications. Continuously checking the links between the formal
and the semi-formal parts of such documents is particularly valuable during the (usually
collaborative) development effort.
As in many other cases, formal certification documents come with an own terminology and
pragmatics of what has to be demonstrated and where, and how the trace-ability of requirements through
design-models over code to system environment assumptions has to be assured.
\<close>
text\<open> In the sequel, we present a simplified version of an ontological model used in a
case-study~ @{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of requirement
(see \autoref{fig:conceptual}).
\begin{figure}
\begin{isar}
doc_class requirement = long_name :: "string option"
doc_class requirement_analysis = no :: "nat"
where "requirement_item +"
doc_class hypothesis = requirement +
hyp_type :: hyp_type <= physical (* default *)
datatype ass_kind = informal | semiformal | formal
doc_class assumption = requirement +
assumption_kind :: ass_kind <= informal
\end{isar}
\caption{Modeling requirements.}
\label{fig:conceptual}
\end{figure}
Such ontologies can be enriched by larger explanations and examples, which may help
the team of engineers substantially when developing the central document for a certification,
like an explication what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an
\<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each
document class its definition available by a simple mouse-click, this kind on meta-knowledge
can be made far more accessible during the document evolution.
For example, the term of 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. It is different from a hypothesis, which is
globally assumed and accepted.
In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short)
is used for formal assumptions, that arise during the analysis,
design or implementation and have to be tracked till the final
evaluation target, and discharged by appropriate validation procedures
within the certification process, by it by test or proof. A particular class of interest
is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>srac\<close>
for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
of the evaluation target. Their track-ability throughout the certification
is therefore particularly critical. This is naturally modeled as follows:
\begin{isar}
doc_class ec = assumption +
assumption_kind :: ass_kind <= (*default *) formal
doc_class srac = ec +
assumption_kind :: ass_kind <= (*default *) formal
\end{isar}
\<close>
section*[mathex_onto::example]\<open> The Math-Exam Scenario \<close>
text\<open> The Math-Exam Scenario is an application with mixed formal and
semi-formal content. It addresses applications where the author of the exam is not present
@ -277,77 +349,7 @@ figure*[fig_qcm::figure,spawn_columns=False,
relative_width="90",src="''figures/InteractiveMathSheet''"]
\<open> A Generated QCM Fragment \ldots \<close>
section*[cenelec_onto::example]\<open> The Certification Scenario following CENELEC \<close>
text\<open> Documents to be provided in formal certifications (such as CENELEC
50126/50128, the DO-178B/C, or Common Criteria) can much profit from the control of ontological consistency:
a lot of an evaluators work consists in tracing down the links from requirements over
assumptions down to elements of evidence, be it in the models, the code, or the tests.
In a certification process, traceability becomes a major concern; and providing
mechanisms to ensure complete traceability already at the development of the
global document will clearly increase speed and reduce risk and cost of a
certification process. Making the link-structure machine-checkable, be it between requirements,
assumptions, their implementation and their discharge by evidence (be it tests, proofs, or
authoritative arguments), is therefore natural and has the potential to decrease the cost
of developments targeting certifications. Continuously checking the links between the formal
and the semi-formal parts of such documents is particularly valuable during the (usually
collaborative) development effort.
As in many other cases, formal certification documents come with an own terminology and
pragmatics of what has to be demonstrated and where, and how the trace-ability of requirements through
design-models over code to system environment assumptions has to be assured.
\<close>
text\<open> In the sequel, we present a simplified version of an ontological model used in a
case-study~ @{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of requirement
(see \autoref{fig:conceptual}).
\begin{figure}
\begin{isar}
doc_class requirement = long_name :: "string option"
doc_class requirement_analysis = no :: "nat"
where "requirement_item +"
doc_class hypothesis = requirement +
hyp_type :: hyp_type <= physical (* default *)
datatype ass_kind = informal | semiformal | formal
doc_class assumption = requirement +
assumption_kind :: ass_kind <= informal
\end{isar}
\caption{Modeling requirements.}
\label{fig:conceptual}
\end{figure}
Such ontologies can be enriched by larger explanations and examples, which may help
the team of engineers substantially when developing the central document for a certification,
like an explication what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an
\<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each
document class its definition available by a simple mouse-click, this kind on meta-knowledge
can be made far more accessible during the document evolution.
For example, the term of 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. It is different from a hypothesis, which is
globally assumed and accepted.
In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short)
is used for formal assumptions, that arise during the analysis,
design or implementation and have to be tracked till the final
evaluation target, and discharged by appropriate validation procedures
within the certification process, by it by test or proof. A particular class of interest
is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>srac\<close>
for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
of the evaluation target. Their track-ability throughout the certification
is therefore particularly critical. This is naturally modeled as follows:
\begin{isar}
doc_class ec = assumption +
assumption_kind :: ass_kind <= (*default *) formal
doc_class srac = ec +
assumption_kind :: ass_kind <= (*default *) formal
\end{isar}
\<close>
section*[ontopide::technical]\<open> Ontology-based IDE support \<close>
text\<open> We present a selection of interaction scenarios @{example \<open>scholar_onto\<close>}
and @{example \<open>cenelec_onto\<close>} with Isabelle/PIDE instrumented by \isadof. \<close>

71
examples/technical_report/IsaDof_Manual/04_RefMan.thy
View File

@ -63,16 +63,6 @@ of documents via the language specified by the regular expression
enforcing a sequence of text-elements that must belong to the corresponding classes.
\<close>
text\<open>
\<^rail>\<open>
(@@{command "chapter*"} | @@{command "section*"} | @@{command "subsection*"} |
@@{command "subsubsection*"} | @@{command "paragraph*"} | @@{command "subparagraph*"})
(@@{command "text*"} | @@{command "figure*"} | @@{command "side_by_side_figure*"} |
@@{command "open_monitor*"} | @@{command "close_monitor*"} |
@@{command "update_instance*"} | @@{command "declare_reference*"})
\<close>
\<close>
section*[install::technical]\<open>Installation\<close>
text\<open>
@ -91,6 +81,59 @@ article in PDF using the following command:
\<close>
section*["core-manual"::technical]\<open>Annotatable Text-Elements for Core-Documents\<close>
text\<open>In general, all standard text-elements from the Isabelle document model such
as @{command "chapter"}, @{command "section"}, @{command "text"}, have in the \isadof
implementation their counterparts in the family of text-elements that are "ontology-aware",
\ie they dispose on a meta-argument list that allows to define that a test-element
\<^enum> has an identity as a text-object labelled as \<open>obj_id\<close>
\<^enum> belongs to a document class \<open>class_id\<close> that has been defined earlier
\<^enum> has its class-attributes set with particular values
(which are denotable in Isabelle/HOL mathematical term syntax)
\<close>
subsection*["core-manual1"::technical]\<open>Syntax\<close>
text\<open>The syntax of toplevel \isadof commands reads as follows:
\<^item> \<open>annotated_text_element\<close> :
\<^rail>\<open>
( ( @@{command "title*"}
| @@{command "subtitle*"}
| @@{command "chapter*"}
| @@{command "section*"} | @@{command "subsection*"}
| @@{command "subsubsection*"} | @@{command "paragraph*"} | @@{command "subparagraph*"}
| @@{command "text*"} | @@{command "figure*"} | @@{command "side_by_side_figure*"}
| @@{command "open_monitor*"} | @@{command "close_monitor*"}
| @@{command "Definition*"} | @@{command "Lemma*"}
| @@{command "Theorem*"} | @@{command "Conjecture*"}
)
'[' meta_args ']' '\<open>' text '\<close>'
)
| change_status_command
| inspection_command
\<close>
\<^item> \<open>meta_args\<close> :
\<^rail>\<open>(obj_id ('::' class_id) ((attribute '=' term)) * ',')\<close>
\<^item> \<open>rich_meta_args\<close> :
\<^rail>\<open> (obj_id ('::' class_id) ((attribute (('=' | '+=') term)) * ','))\<close>
\<^item> \isadof\<open>change_status_command\<close> :
\<^rail>\<open> (@@{command "update_instance*"} '[' rich_meta_args ']')
| (@@{command "declare_reference*"} (obj_id ('::' class_id)))\<close>
\<^item> \isadof\<open>inspection_command\<close> :
\<^rail>\<open> @@{command "print_doc_classes"}
| @@{command "print_doc_items"}
| @@{command "check_doc_global"}\<close>
\<close>
subsection*["commonlib"::technical]\<open>Common Ontology Library (COL)\<close>
subsection*["core-manual2"::technical]\<open>Examples\<close>
section*["odl-manual"::technical]\<open>The ODL Manual\<close>
subsection*["odl-manual1"::technical]\<open>The ODL Command Syntax\<close>
section*["odl-design"::technical]\<open>The Design of ODL\<close>
subsection*[onto_future::technical]\<open> Monitor Classes \<close>
@ -119,18 +162,10 @@ monitor are \<^emph>\<open>independent\<close> from a monitor; instances of inde
may occur freely. \<close>
section*["odl-manual"::technical]\<open>The ODL Manual\<close>
subsection*["odl-manual1"::technical]\<open>The ODL Command Syntax\<close>
subsection*["odl-manual2"::technical]\<open>Examples\<close>
section*["core-manual"::technical]\<open>Text-Elements for Core-Documents\<close>
subsection*["core-manual1"::technical]\<open>Syntax\<close>
subsection*["core-manual2"::technical]\<open>Examples\<close>
(*<*)
end