From c181c2851c9fbf30fd5b3abd00620d7a5ad6687b Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 17 Jul 2019 21:10:18 +0200 Subject: [PATCH] Added first somewhat realistic syntax on annotated text elements --- .../IsaDof_Manual/03_GuidedTour.thy | 142 +++++++++--------- .../IsaDof_Manual/04_RefMan.thy | 71 ++++++--- 2 files changed, 125 insertions(+), 88 deletions(-) diff --git a/examples/technical_report/IsaDof_Manual/03_GuidedTour.thy b/examples/technical_report/IsaDof_Manual/03_GuidedTour.thy index 94f2e4d..70e4e9b 100644 --- a/examples/technical_report/IsaDof_Manual/03_GuidedTour.thy +++ b/examples/technical_report/IsaDof_Manual/03_GuidedTour.thy @@ -153,6 +153,78 @@ text\ The document class \inlineisar+figure+ --- supported by the \isadof such as @{docitem_ref \fig_figures\}. \ + +section*[cenelec_onto::example]\ The Certification Scenario following CENELEC \ +text\ 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. +\ +text\ 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>\hypothesis\ and an +\<^emph>\assumption\ 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>\assumption\ 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>\exported constraint\ (or \<^emph>\ec\ 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>\safety related application condition\ (or \<^emph>\srac\ +for short) which is used for \<^emph>\ec\'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} +\ + section*[mathex_onto::example]\ The Math-Exam Scenario \ text\ 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''"] \ A Generated QCM Fragment \ldots \ -section*[cenelec_onto::example]\ The Certification Scenario following CENELEC \ -text\ 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. -\ -text\ 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>\hypothesis\ and an -\<^emph>\assumption\ 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>\assumption\ 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>\exported constraint\ (or \<^emph>\ec\ 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>\safety related application condition\ (or \<^emph>\srac\ -for short) which is used for \<^emph>\ec\'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} -\ - section*[ontopide::technical]\ Ontology-based IDE support \ text\ We present a selection of interaction scenarios @{example \scholar_onto\} and @{example \cenelec_onto\} with Isabelle/PIDE instrumented by \isadof. \ diff --git a/examples/technical_report/IsaDof_Manual/04_RefMan.thy b/examples/technical_report/IsaDof_Manual/04_RefMan.thy index 2504e79..b8a704b 100644 --- a/examples/technical_report/IsaDof_Manual/04_RefMan.thy +++ b/examples/technical_report/IsaDof_Manual/04_RefMan.thy @@ -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. \ -text\ -\<^rail>\ - (@@{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*"}) - \ -\ - section*[install::technical]\Installation\ text\ @@ -91,6 +81,59 @@ article in PDF using the following command: \ + +section*["core-manual"::technical]\Annotatable Text-Elements for Core-Documents\ +text\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 \obj_id\ +\<^enum> belongs to a document class \class_id\ that has been defined earlier +\<^enum> has its class-attributes set with particular values + (which are denotable in Isabelle/HOL mathematical term syntax) +\ + +subsection*["core-manual1"::technical]\Syntax\ + +text\The syntax of toplevel \isadof commands reads as follows: +\<^item> \annotated_text_element\ : +\<^rail>\ + ( ( @@{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 ']' '\' text '\' + ) + | change_status_command + | inspection_command + \ +\<^item> \meta_args\ : + \<^rail>\(obj_id ('::' class_id) ((attribute '=' term)) * ',')\ +\<^item> \rich_meta_args\ : + \<^rail>\ (obj_id ('::' class_id) ((attribute (('=' | '+=') term)) * ','))\ +\<^item> \isadof\change_status_command\ : + \<^rail>\ (@@{command "update_instance*"} '[' rich_meta_args ']') + | (@@{command "declare_reference*"} (obj_id ('::' class_id)))\ +\<^item> \isadof\inspection_command\ : + \<^rail>\ @@{command "print_doc_classes"} + | @@{command "print_doc_items"} + | @@{command "check_doc_global"}\ +\ + +subsection*["commonlib"::technical]\Common Ontology Library (COL)\ + +subsection*["core-manual2"::technical]\Examples\ + +section*["odl-manual"::technical]\The ODL Manual\ + +subsection*["odl-manual1"::technical]\The ODL Command Syntax\ + section*["odl-design"::technical]\The Design of ODL\ subsection*[onto_future::technical]\ Monitor Classes \ @@ -119,18 +162,10 @@ monitor are \<^emph>\independent\ from a monitor; instances of inde may occur freely. \ -section*["odl-manual"::technical]\The ODL Manual\ - -subsection*["odl-manual1"::technical]\The ODL Command Syntax\ - subsection*["odl-manual2"::technical]\Examples\ -section*["core-manual"::technical]\Text-Elements for Core-Documents\ -subsection*["core-manual1"::technical]\Syntax\ - -subsection*["core-manual2"::technical]\Examples\ (*<*) end