new config of the document
|
@ -1537,10 +1537,9 @@ ML\<open> (* Setting in thy_output.ML a parser for the syntactic handling of the
|
||||||
text elements - so text*[m<meta-info>]\<open> ... dfgdfg .... \<close> *)
|
text elements - so text*[m<meta-info>]\<open> ... dfgdfg .... \<close> *)
|
||||||
|
|
||||||
val _ = Thy_Output.set_meta_args_parser
|
val _ = Thy_Output.set_meta_args_parser
|
||||||
(fn thy => let val _ = writeln "META_ARGS_PARSING"
|
(fn thy => (Scan.optional (Document_Source.improper
|
||||||
in (Scan.optional (Document_Source.improper |-- ODL_Command_Parser.attributes
|
|-- ODL_Command_Parser.attributes
|
||||||
>> ODL_LTX_Converter.meta_args_2_string thy) "")
|
>> ODL_LTX_Converter.meta_args_2_string thy) "")); \<close>
|
||||||
end); \<close>
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -85,7 +85,7 @@ Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
|
||||||
section*["sec:background"::introduction]\<open>The Document Model\<close>
|
section*["sec:background"::introduction]\<open>The Required Document Model\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
In this section, we explain the assumed document model underlying
|
In this section, we explain the assumed document model underlying
|
||||||
\dof in general; in particular the concepts \<^emph>\<open>integrated document\<close>,
|
\dof in general; in particular the concepts \<^emph>\<open>integrated document\<close>,
|
||||||
|
@ -166,9 +166,8 @@ typeset. They represent the device for linking the formal with the informal. \<c
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
subsection*[bgrnd21::introduction]\<open>Implementability of the Assumed Document Model.\<close>
|
section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model.\<close>
|
||||||
text\<open>
|
text\<open> Batch-mode checkers for \dof can be implemented in all systems of the
|
||||||
Batch-mode checkers for \dof can be implemented in all systems of the
|
|
||||||
LCF-style prover family, \ie, systems with a type-checked
|
LCF-style prover family, \ie, systems with a type-checked
|
||||||
\inlinesml{term}, and abstract \inlinesml{thm}-type for
|
\inlinesml{term}, and abstract \inlinesml{thm}-type for
|
||||||
theorems (protected by a kernel). This includes, \eg, ProofPower,
|
theorems (protected by a kernel). This includes, \eg, ProofPower,
|
||||||
|
|
|
@ -61,6 +61,10 @@ in an object-oriented manner, monitor classes enforce structural organization
|
||||||
of documents via the language specified by the regular expression
|
of documents via the language specified by the regular expression
|
||||||
enforcing a sequence of text-elements that must belong to the corresponding classes.
|
enforcing a sequence of text-elements that must belong to the corresponding classes.
|
||||||
|
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
section*[install::technical]\<open>Installation\<close>
|
||||||
|
text\<open>
|
||||||
To start using \isadof, one creates an Isabelle project (with the name
|
To start using \isadof, one creates an Isabelle project (with the name
|
||||||
\inlinebash{IsaDofApplications}):
|
\inlinebash{IsaDofApplications}):
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
|
@ -75,433 +79,21 @@ article in PDF using the following command:
|
||||||
\end{bash}
|
\end{bash}
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
chapter*[ontomod::text_section]\<open> Modeling Ontologies in \isadof \<close>
|
|
||||||
text\<open> In this section, we will use the \isadof document ontology language
|
|
||||||
for three different application scenarios: for scholarly papers, for mathematical
|
|
||||||
exam sheets as well as standardization documents where the concepts of the
|
|
||||||
standard are captured in the ontology. For space reasons, we will concentrate in all three
|
|
||||||
cases on aspects of the modeling due to space limitations.\<close>
|
|
||||||
|
|
||||||
section*[scholar_onto::example]\<open> The Scholar Paper Scenario: Eating One's Own Dog Food. \<close>
|
section*["odl-design"::technical]\<open>The Design of ODL\<close>
|
||||||
text\<open> The following ontology is a simple ontology modeling scientific papers. In this
|
|
||||||
\isadof application scenario, we deliberately refrain from integrating references to
|
|
||||||
(Isabelle) formal content in order demonstrate that \isadof is not a framework from
|
|
||||||
Isabelle users to Isabelle users only.
|
|
||||||
Of course, such references can be added easily and represent a particular strength
|
|
||||||
of \isadof.
|
|
||||||
|
|
||||||
|
declare_reference*[scholar_onto::example]
|
||||||
\begin{figure}
|
subsection*[onto_future::technical]\<open> Monitor Classes \<close>
|
||||||
\begin{isar}
|
(*
|
||||||
doc_class title =
|
|
||||||
short_title :: "string option" <= None
|
|
||||||
|
|
||||||
doc_class subtitle =
|
|
||||||
abbrev :: "string option" <= None
|
|
||||||
|
|
||||||
doc_class author =
|
|
||||||
affiliation :: "string"
|
|
||||||
|
|
||||||
doc_class abstract =
|
|
||||||
keyword_list :: "string list" <= None
|
|
||||||
|
|
||||||
doc_class text_section =
|
|
||||||
main_author :: "author option" <= None
|
|
||||||
todo_list :: "string list" <= "[]"
|
|
||||||
\end{isar}
|
|
||||||
\caption{The core of the ontology definition for writing scholarly papers.}
|
|
||||||
\label{fig:paper-onto-core}
|
|
||||||
\end{figure}
|
|
||||||
The first part of the ontology \inlineisar+scholarly_paper+ (see \autoref{fig:paper-onto-core})
|
|
||||||
contains the document class definitions
|
|
||||||
with the usual text-elements of a scientific paper. The attributes \inlineisar+short_title+,
|
|
||||||
\inlineisar+abbrev+ etc are introduced with their types as well as their default values.
|
|
||||||
Our model prescribes an optional \inlineisar+main_author+ and a todo-list attached to an arbitrary
|
|
||||||
text section; since instances of this class are mutable (meta)-objects of text-elements, they
|
|
||||||
can be modified arbitrarily through subsequent text and of course globally during text evolution.
|
|
||||||
Since \inlineisar+author+ is a HOL-type internally generated by \isadof framework and can therefore
|
|
||||||
appear in the \inlineisar+main_author+ attribute of the \inlineisar+text_section+ class;
|
|
||||||
semantic links between concepts can be modeled this way.
|
|
||||||
|
|
||||||
The translation of its content to, \eg, Springer's \LaTeX{} setup for the Lecture Notes in Computer
|
|
||||||
Science Series, as required by many scientific conferences, is mostly straight-forward. \<close>
|
|
||||||
|
|
||||||
figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
|
|
||||||
\<open> Ouroboros I: This paper from inside \ldots \<close>
|
|
||||||
|
|
||||||
text\<open> @{docitem \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of thqqe present paper.
|
|
||||||
Note that the text uses \isadof's own text-commands containing the meta-information provided by
|
|
||||||
the underlying ontology.
|
|
||||||
We proceed by a definition of \inlineisar+introduction+'s, which we define as the extension of
|
|
||||||
\inlineisar+text_section+ which is intended to capture common infrastructure:
|
|
||||||
\begin{isar}
|
|
||||||
doc_class introduction = text_section +
|
|
||||||
comment :: string
|
|
||||||
\end{isar}
|
|
||||||
As a consequence of the definition as extension, the \inlineisar+introduction+ class
|
|
||||||
inherits the attributes \inlineisar+main_author+ and \inlineisar+todo_list+ together with
|
|
||||||
the corresponding default values.
|
|
||||||
|
|
||||||
As a variant of the introduction, we could add here an attribute that contains the formal
|
|
||||||
claims of the article --- either here, or, for example, in the keyword list of the abstract.
|
|
||||||
As type, one could use either the built-in type \inlineisar+term+ (for syntactically correct,
|
|
||||||
but not necessarily proven entity) or \inlineisar+thm+ (for formally proven entities). It suffices
|
|
||||||
to add the line:
|
|
||||||
\begin{isar}
|
|
||||||
claims :: "thm list"
|
|
||||||
\end{isar}
|
|
||||||
and to extent the \LaTeX-style accordingly to handle the additional field.
|
|
||||||
Note that \inlineisar+term+ and \inlineisar+thm+ are types reflecting the core-types of the
|
|
||||||
Isabelle kernel. In a corresponding conclusion section, one could model analogously an
|
|
||||||
achievement section; by programming a specific compliance check in SML, the implementation
|
|
||||||
of automated forms of validation check for specific categories of papers is envisageable.
|
|
||||||
Since this requires deeper knowledge in Isabelle programming, however, we consider this out
|
|
||||||
of the scope of this paper.
|
|
||||||
|
|
||||||
|
|
||||||
We proceed more or less conventionally by the subsequent sections (\autoref{fig:paper-onto-sections})
|
|
||||||
\begin{figure}
|
|
||||||
\begin{isar}
|
|
||||||
doc_class technical = text_section +
|
|
||||||
definition_list :: "string list" <= "[]"
|
|
||||||
|
|
||||||
doc_class example = text_section +
|
|
||||||
comment :: string
|
|
||||||
|
|
||||||
doc_class conclusion = text_section +
|
|
||||||
main_author :: "author option" <= None
|
|
||||||
|
|
||||||
doc_class related_work = conclusion +
|
|
||||||
main_author :: "author option" <= None
|
|
||||||
|
|
||||||
doc_class bibliography =
|
|
||||||
style :: "string option" <= "''LNCS''"
|
|
||||||
\end{isar}
|
|
||||||
\caption{Various types of sections of a scholarly papers.}
|
|
||||||
\label{fig:paper-onto-sections}
|
|
||||||
\end{figure}
|
|
||||||
and finish with a monitor class definition that enforces a textual ordering
|
|
||||||
in the document core by a regular expression (\autoref{fig:paper-onto-monitor}).
|
|
||||||
\begin{figure}
|
|
||||||
\begin{isar}
|
|
||||||
doc_class article =
|
|
||||||
trace :: "(title + subtitle + author+ abstract +
|
|
||||||
introduction + technical + example +
|
|
||||||
conclusion + bibliography) list"
|
|
||||||
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
|
|
||||||
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
|
|
||||||
bibliography)"
|
|
||||||
\end{isar}
|
|
||||||
\caption{A monitor for the scholarly paper ontology.}
|
|
||||||
\label{fig:paper-onto-monitor}
|
|
||||||
\end{figure}
|
|
||||||
\<close>
|
|
||||||
text\<open> We might wish to add a component into our ontology that models figures to be included into
|
|
||||||
the document. This boils down to the exercise of modeling structured data in the style of a
|
|
||||||
functional programming language in HOL and to reuse the implicit HOL-type inside a suitable document
|
|
||||||
class \inlineisar+figure+:
|
|
||||||
\begin{isar}
|
|
||||||
datatype placement = h | t | b | ht | hb
|
|
||||||
doc_class figure = text_section +
|
|
||||||
relative_width :: "int" (* percent of textwidth *)
|
|
||||||
src :: "string"
|
|
||||||
placement :: placement
|
|
||||||
spawn_columns :: bool <= True
|
|
||||||
\end{isar}
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
text\<open> Alternatively, by including the HOL-libraries for rationals, it is possible to
|
|
||||||
use fractions or even mathematical reals. This must be counterbalanced by syntactic
|
|
||||||
and semantic convenience. Choosing the mathematical reals, \eg, would have the drawback that
|
|
||||||
attribute evaluation could be substantially more complicated.\<close>
|
|
||||||
|
|
||||||
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
|
|
||||||
\<open> Ouroboros II: figures \ldots \<close>
|
|
||||||
|
|
||||||
text\<open> The document class \inlineisar+figure+ --- supported by the \isadof text command
|
|
||||||
\inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper
|
|
||||||
such as @{docitem_ref \<open>fig_figures\<close>}.
|
|
||||||
\<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
|
|
||||||
during the exam and the preparation requires a very rigorous process, as the french
|
|
||||||
\<^emph>\<open>baccaleaureat\<close> and exams at The University of Sheffield.
|
|
||||||
|
|
||||||
We assume that the content has four different types of addressees, which have a different
|
|
||||||
\<^emph>\<open>view\<close> on the integrated document:
|
|
||||||
|
|
||||||
\<^item> the \<^emph>\<open>setter\<close>, \ie, the author of the exam,
|
|
||||||
\<^item> the \<^emph>\<open>checker\<close>, \ie, an internal person that checks
|
|
||||||
the exam for feasibility and non-ambiguity,
|
|
||||||
\<^item> the \<^emph>\<open>external examiner\<close>, \ie, an external person that checks
|
|
||||||
the exam for feasibility and non-ambiguity, and
|
|
||||||
\<^item> the \<^emph>\<open>student\<close>, \ie, the addressee of the exam.
|
|
||||||
\<close>
|
|
||||||
text\<open> The latter quality assurance mechanism is used in many universities,
|
|
||||||
where for organizational reasons the execution of an exam takes place in facilities
|
|
||||||
where the author of the exam is not expected to be physically present.
|
|
||||||
Furthermore, we assume a simple grade system (thus, some calculation is required).
|
|
||||||
|
|
||||||
\begin{figure}
|
|
||||||
\begin{isar}
|
|
||||||
doc_class Author = ...
|
|
||||||
datatype Subject = algebra | geometry | statistical
|
|
||||||
datatype Grade = A1 | A2 | A3
|
|
||||||
|
|
||||||
doc_class Header = examTitle :: string
|
|
||||||
examSubject :: Subject
|
|
||||||
date :: string
|
|
||||||
timeAllowed :: int -- minutes
|
|
||||||
|
|
||||||
datatype ContentClass = setter
|
|
||||||
| checker
|
|
||||||
| external_examiner
|
|
||||||
| student
|
|
||||||
|
|
||||||
doc_class Exam_item =
|
|
||||||
concerns :: "ContentClass set"
|
|
||||||
|
|
||||||
doc_class Exam_item =
|
|
||||||
concerns :: "ContentClass set"
|
|
||||||
|
|
||||||
type_synonym SubQuestion = string
|
|
||||||
\end{isar}
|
|
||||||
\caption{The core of the ontology modeling math exams.}
|
|
||||||
\label{fig:onto-exam}
|
|
||||||
\end{figure}
|
|
||||||
The heart of this ontology (see \autoref{fig:onto-exam}) is an alternation of questions and answers,
|
|
||||||
where the answers can consist of simple yes-no answers (QCM style check-boxes) or lists of formulas.
|
|
||||||
Since we do not
|
|
||||||
assume familiarity of the students with Isabelle (\inlineisar+term+ would assume that this is a
|
|
||||||
parse-able and type-checkable entity), we basically model a derivation as a sequence of strings
|
|
||||||
(see \autoref{fig:onto-questions}).
|
|
||||||
\begin{figure}
|
|
||||||
\begin{isar}
|
|
||||||
doc_class Answer_Formal_Step = Exam_item +
|
|
||||||
justification :: string
|
|
||||||
"term" :: "string"
|
|
||||||
|
|
||||||
doc_class Answer_YesNo = Exam_item +
|
|
||||||
step_label :: string
|
|
||||||
yes_no :: bool -- \<open>for checkboxes\<close>
|
|
||||||
|
|
||||||
datatype Question_Type =
|
|
||||||
formal | informal | mixed
|
|
||||||
|
|
||||||
doc_class Task = Exam_item +
|
|
||||||
level :: Level
|
|
||||||
type :: Question_Type
|
|
||||||
subitems :: "(SubQuestion *
|
|
||||||
(Answer_Formal_Step list + Answer_YesNo) list) list"
|
|
||||||
concerns :: "ContentClass set" <= "UNIV"
|
|
||||||
mark :: int
|
|
||||||
doc_class Exercise = Exam_item +
|
|
||||||
type :: Question_Type
|
|
||||||
content :: "(Task) list"
|
|
||||||
concerns :: "ContentClass set" <= "UNIV"
|
|
||||||
mark :: int
|
|
||||||
\end{isar}
|
|
||||||
\caption{An exam can contain different types of questions.}
|
|
||||||
\label{fig:onto-questions}
|
|
||||||
\end{figure}
|
|
||||||
|
|
||||||
In many institutions, it makes sense to have a rigorous process of validation
|
|
||||||
for exam subjects: is the initial question correct? Is a proof in the sense of the
|
|
||||||
question possible? We model the possibility that the @{term examiner} validates a
|
|
||||||
question by a sample proof validated by Isabelle (see \autoref{fig:onto-exam-monitor}).
|
|
||||||
In our scenario this sample proofs are completely \<^emph>\<open>intern\<close>, \ie, not exposed to the
|
|
||||||
students but just additional material for the internal review process of the exam.
|
|
||||||
\begin{figure}
|
|
||||||
\begin{isar}
|
|
||||||
doc_class Validation =
|
|
||||||
tests :: "term list" <="[]"
|
|
||||||
proofs :: "thm list" <="[]"
|
|
||||||
|
|
||||||
doc_class Solution = Exam_item +
|
|
||||||
content :: "Exercise list"
|
|
||||||
valids :: "Validation list"
|
|
||||||
concerns :: "ContentClass set" <= "{setter,checker,external_examiner}"
|
|
||||||
|
|
||||||
doc_class MathExam=
|
|
||||||
content :: "(Header + Author + Exercise) list"
|
|
||||||
global_grade :: Grade
|
|
||||||
where "\<lbrace>Author\<rbrace>$^+$ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>$^+$ "
|
|
||||||
\end{isar}
|
|
||||||
\caption{Validating exams.}
|
|
||||||
\label{fig:onto-exam-monitor}
|
|
||||||
\end{figure}
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
|
|
||||||
declare_reference*["fig_qcm"::figure]
|
|
||||||
|
|
||||||
text\<open> Using the \LaTeX{} package hyperref, it is possible to conceive an interactive
|
|
||||||
exam-sheets with multiple-choice and/or free-response elements
|
|
||||||
(see @{docitem_ref (unchecked) \<open>fig_qcm\<close>}). With the
|
|
||||||
help of the latter, it is possible that students write in a browser a formal mathematical
|
|
||||||
derivation---as part of an algebra exercise, for example---which is submitted to the examiners
|
|
||||||
electronically. \<close>
|
|
||||||
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>
|
|
||||||
|
|
||||||
chapter*[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>
|
|
||||||
|
|
||||||
section*[scholar_pide::example]\<open> A Scholarly Paper \<close>
|
|
||||||
text\<open> In \autoref{fig-Dogfood-II-bgnd1} and \autoref{fig-bgnd-text_section} we show how
|
|
||||||
hovering over links permits to explore its meta-information.
|
|
||||||
Clicking on a document class identifier permits to hyperlink into the corresponding
|
|
||||||
class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition
|
|
||||||
(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}).
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
open_monitor*["text-elements"::figure_group,
|
|
||||||
caption="''Exploring text elements.''"]
|
|
||||||
|
|
||||||
figure*["fig-Dogfood-II-bgnd1"::figure, spawn_columns=False,
|
|
||||||
relative_width="48",
|
|
||||||
src="''figures/Dogfood-II-bgnd1''"]
|
|
||||||
\<open>Exploring a Reference of a Text-Element.\<close>
|
|
||||||
|
|
||||||
figure*["fig-bgnd-text_section"::figure, spawn_columns=False,
|
|
||||||
relative_width="48",
|
|
||||||
src="''figures/Dogfood-III-bgnd-text_section''"]
|
|
||||||
\<open>Exploring the class of a text element.\<close>
|
|
||||||
|
|
||||||
close_monitor*["text-elements"]
|
|
||||||
|
|
||||||
|
|
||||||
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
|
|
||||||
caption="''Hyperlink to Class-Definition.''",relative_width="48",
|
|
||||||
src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''",
|
|
||||||
caption2="''Exploring an attribute.''",relative_width2="47",
|
|
||||||
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Hyperlinks.\<close>
|
|
||||||
|
|
||||||
|
|
||||||
declare_reference*["figDogfoodVIlinkappl"::figure]
|
|
||||||
text\<open> An ontological reference application in \autoref{figDogfoodVIlinkappl}: the ontology-dependant
|
|
||||||
antiquotation \inlineisar|@ {example ...}| refers to the corresponding text-elements. Hovering allows
|
|
||||||
for inspection, clicking for jumping to the definition. If the link does not exist or has a
|
|
||||||
non-compatible type, the text is not validated. \<close>
|
|
||||||
|
|
||||||
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
|
|
||||||
\<open> Exploring an attribute (hyperlinked to the class). \<close>
|
|
||||||
section*[cenelec_pide::example]\<open> CENELEC \<close>
|
|
||||||
declare_reference*[figfig3::figure]
|
|
||||||
text\<open> The corresponding view in @{docitem_ref (unchecked) \<open>figfig3\<close>} shows core part of a document,
|
|
||||||
coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows standard Isabelle antiquotations
|
|
||||||
@{cite "wenzel:isabelle-isar:2017"} into formal entities of a theory. This way, the informal parts
|
|
||||||
of a document get ``formal content'' and become more robust under change.\<close>
|
|
||||||
|
|
||||||
figure*[figfig3::figure,relative_width="80",src="''figures/antiquotations-PIDE''"]
|
|
||||||
\<open> Standard antiquotations referring to theory elements.\<close>
|
|
||||||
|
|
||||||
declare_reference*[figfig5::figure]
|
|
||||||
text\<open> The subsequent sample in @{docitem_ref (unchecked) \<open>figfig5\<close>} shows the definition of an
|
|
||||||
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
|
|
||||||
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
|
|
||||||
device. This condition can not be established inside the formal theory but has to be
|
|
||||||
checked by system integration tests.\<close>
|
|
||||||
|
|
||||||
figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"]
|
|
||||||
\<open> Defining a SRAC reference \ldots \<close>
|
|
||||||
figure*[figfig7::figure, relative_width="80", src="''figures/srac-as-es-application''"]
|
|
||||||
\<open> Using a SRAC as EC document reference. \<close>
|
|
||||||
|
|
||||||
text\<open> Now we reference in @{docitem_ref (unchecked) \<open>figfig7\<close>} this safety-related condition;
|
|
||||||
however, this happens in a context where general \<^emph>\<open>exported constraints\<close> are listed.
|
|
||||||
\isadof's checks establish that this is legal in the given ontology.
|
|
||||||
|
|
||||||
This example shows that ontological modeling is indeed adequate for large technical,
|
|
||||||
collaboratively developed documentations, where modifications can lead easily to incoherence.
|
|
||||||
The current checks help to systematically avoid this type of incoherence between formal and
|
|
||||||
informal parts. \<close>
|
|
||||||
|
|
||||||
chapter*[onto_future::technical]\<open> Monitor Classes \<close>
|
|
||||||
text\<open> Besides sub-typing, there is another relation between
|
text\<open> Besides sub-typing, there is another relation between
|
||||||
document classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
|
document classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
|
||||||
which is expressed by the occurrence of a \inlineisar+where+ clause
|
which is expressed by the occurrence of a \inlineisar+where+ clause
|
||||||
in the document class definition containing a regular
|
in the document class definition containing a regular
|
||||||
expression (see @{example \<open>scholar_onto\<close>}).
|
expression (see @{example (unchecked) \<open>scholar_onto\<close>}).
|
||||||
While class-extension refers to data-inheritance of attributes,
|
While class-extension refers to data-inheritance of attributes,
|
||||||
a monitor imposes structural constraints -- the order --
|
a monitor imposes structural constraints -- the order --
|
||||||
in which instances of monitored classes may occur. \<close>
|
in which instances of monitored classes may occur. \<close>
|
||||||
|
*)
|
||||||
text\<open>
|
text\<open>
|
||||||
The control of monitors is done by the commands:
|
The control of monitors is done by the commands:
|
||||||
\<^item> \inlineisar+open_monitor* + <doc-class>
|
\<^item> \inlineisar+open_monitor* + <doc-class>
|
||||||
|
@ -517,7 +109,20 @@ monitor are \<^emph>\<open>independent\<close> from a monitor; instances of inde
|
||||||
may occur freely. \<close>
|
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
|
end
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,430 @@
|
||||||
|
(*<*)
|
||||||
|
theory "04_IsaDofCaseStudies"
|
||||||
|
imports "03_IsaDof"
|
||||||
|
begin
|
||||||
|
(*>*)
|
||||||
|
|
||||||
|
chapter*[casestudies::example,main_author="Some(@{docitem ''adb''}::author)"]\<open> \isadof Case Studies \<close>
|
||||||
|
|
||||||
|
text\<open> In this section, we will use the \isadof document ontology language
|
||||||
|
for three different application scenarios: for scholarly papers, for mathematical
|
||||||
|
exam sheets as well as standardization documents where the concepts of the
|
||||||
|
standard are captured in the ontology. For space reasons, we will concentrate in all three
|
||||||
|
cases on aspects of the modeling due to space limitations.\<close>
|
||||||
|
|
||||||
|
section*[scholar_onto::example]\<open> The Scholar Paper Scenario: Eating One's Own Dog Food. \<close>
|
||||||
|
text\<open> The following ontology is a simple ontology modeling scientific papers. In this
|
||||||
|
\isadof application scenario, we deliberately refrain from integrating references to
|
||||||
|
(Isabelle) formal content in order demonstrate that \isadof is not a framework from
|
||||||
|
Isabelle users to Isabelle users only.
|
||||||
|
Of course, such references can be added easily and represent a particular strength
|
||||||
|
of \isadof.
|
||||||
|
|
||||||
|
|
||||||
|
\begin{figure}
|
||||||
|
\begin{isar}
|
||||||
|
doc_class title =
|
||||||
|
short_title :: "string option" <= None
|
||||||
|
|
||||||
|
doc_class subtitle =
|
||||||
|
abbrev :: "string option" <= None
|
||||||
|
|
||||||
|
doc_class author =
|
||||||
|
affiliation :: "string"
|
||||||
|
|
||||||
|
doc_class abstract =
|
||||||
|
keyword_list :: "string list" <= None
|
||||||
|
|
||||||
|
doc_class text_section =
|
||||||
|
main_author :: "author option" <= None
|
||||||
|
todo_list :: "string list" <= "[]"
|
||||||
|
\end{isar}
|
||||||
|
\caption{The core of the ontology definition for writing scholarly papers.}
|
||||||
|
\label{fig:paper-onto-core}
|
||||||
|
\end{figure}
|
||||||
|
The first part of the ontology \inlineisar+scholarly_paper+ (see \autoref{fig:paper-onto-core})
|
||||||
|
contains the document class definitions
|
||||||
|
with the usual text-elements of a scientific paper. The attributes \inlineisar+short_title+,
|
||||||
|
\inlineisar+abbrev+ etc are introduced with their types as well as their default values.
|
||||||
|
Our model prescribes an optional \inlineisar+main_author+ and a todo-list attached to an arbitrary
|
||||||
|
text section; since instances of this class are mutable (meta)-objects of text-elements, they
|
||||||
|
can be modified arbitrarily through subsequent text and of course globally during text evolution.
|
||||||
|
Since \inlineisar+author+ is a HOL-type internally generated by \isadof framework and can therefore
|
||||||
|
appear in the \inlineisar+main_author+ attribute of the \inlineisar+text_section+ class;
|
||||||
|
semantic links between concepts can be modeled this way.
|
||||||
|
|
||||||
|
The translation of its content to, \eg, Springer's \LaTeX{} setup for the Lecture Notes in Computer
|
||||||
|
Science Series, as required by many scientific conferences, is mostly straight-forward. \<close>
|
||||||
|
|
||||||
|
figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
|
||||||
|
\<open> Ouroboros I: This paper from inside \ldots \<close>
|
||||||
|
|
||||||
|
text\<open> @{docitem \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of thqqe present paper.
|
||||||
|
Note that the text uses \isadof's own text-commands containing the meta-information provided by
|
||||||
|
the underlying ontology.
|
||||||
|
We proceed by a definition of \inlineisar+introduction+'s, which we define as the extension of
|
||||||
|
\inlineisar+text_section+ which is intended to capture common infrastructure:
|
||||||
|
\begin{isar}
|
||||||
|
doc_class introduction = text_section +
|
||||||
|
comment :: string
|
||||||
|
\end{isar}
|
||||||
|
As a consequence of the definition as extension, the \inlineisar+introduction+ class
|
||||||
|
inherits the attributes \inlineisar+main_author+ and \inlineisar+todo_list+ together with
|
||||||
|
the corresponding default values.
|
||||||
|
|
||||||
|
As a variant of the introduction, we could add here an attribute that contains the formal
|
||||||
|
claims of the article --- either here, or, for example, in the keyword list of the abstract.
|
||||||
|
As type, one could use either the built-in type \inlineisar+term+ (for syntactically correct,
|
||||||
|
but not necessarily proven entity) or \inlineisar+thm+ (for formally proven entities). It suffices
|
||||||
|
to add the line:
|
||||||
|
\begin{isar}
|
||||||
|
claims :: "thm list"
|
||||||
|
\end{isar}
|
||||||
|
and to extent the \LaTeX-style accordingly to handle the additional field.
|
||||||
|
Note that \inlineisar+term+ and \inlineisar+thm+ are types reflecting the core-types of the
|
||||||
|
Isabelle kernel. In a corresponding conclusion section, one could model analogously an
|
||||||
|
achievement section; by programming a specific compliance check in SML, the implementation
|
||||||
|
of automated forms of validation check for specific categories of papers is envisageable.
|
||||||
|
Since this requires deeper knowledge in Isabelle programming, however, we consider this out
|
||||||
|
of the scope of this paper.
|
||||||
|
|
||||||
|
|
||||||
|
We proceed more or less conventionally by the subsequent sections (\autoref{fig:paper-onto-sections})
|
||||||
|
\begin{figure}
|
||||||
|
\begin{isar}
|
||||||
|
doc_class technical = text_section +
|
||||||
|
definition_list :: "string list" <= "[]"
|
||||||
|
|
||||||
|
doc_class example = text_section +
|
||||||
|
comment :: string
|
||||||
|
|
||||||
|
doc_class conclusion = text_section +
|
||||||
|
main_author :: "author option" <= None
|
||||||
|
|
||||||
|
doc_class related_work = conclusion +
|
||||||
|
main_author :: "author option" <= None
|
||||||
|
|
||||||
|
doc_class bibliography =
|
||||||
|
style :: "string option" <= "''LNCS''"
|
||||||
|
\end{isar}
|
||||||
|
\caption{Various types of sections of a scholarly papers.}
|
||||||
|
\label{fig:paper-onto-sections}
|
||||||
|
\end{figure}
|
||||||
|
and finish with a monitor class definition that enforces a textual ordering
|
||||||
|
in the document core by a regular expression (\autoref{fig:paper-onto-monitor}).
|
||||||
|
\begin{figure}
|
||||||
|
\begin{isar}
|
||||||
|
doc_class article =
|
||||||
|
trace :: "(title + subtitle + author+ abstract +
|
||||||
|
introduction + technical + example +
|
||||||
|
conclusion + bibliography) list"
|
||||||
|
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
|
||||||
|
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
|
||||||
|
bibliography)"
|
||||||
|
\end{isar}
|
||||||
|
\caption{A monitor for the scholarly paper ontology.}
|
||||||
|
\label{fig:paper-onto-monitor}
|
||||||
|
\end{figure}
|
||||||
|
\<close>
|
||||||
|
text\<open> We might wish to add a component into our ontology that models figures to be included into
|
||||||
|
the document. This boils down to the exercise of modeling structured data in the style of a
|
||||||
|
functional programming language in HOL and to reuse the implicit HOL-type inside a suitable document
|
||||||
|
class \inlineisar+figure+:
|
||||||
|
\begin{isar}
|
||||||
|
datatype placement = h | t | b | ht | hb
|
||||||
|
doc_class figure = text_section +
|
||||||
|
relative_width :: "int" (* percent of textwidth *)
|
||||||
|
src :: "string"
|
||||||
|
placement :: placement
|
||||||
|
spawn_columns :: bool <= True
|
||||||
|
\end{isar}
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
text\<open> Alternatively, by including the HOL-libraries for rationals, it is possible to
|
||||||
|
use fractions or even mathematical reals. This must be counterbalanced by syntactic
|
||||||
|
and semantic convenience. Choosing the mathematical reals, \eg, would have the drawback that
|
||||||
|
attribute evaluation could be substantially more complicated.\<close>
|
||||||
|
|
||||||
|
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
|
||||||
|
\<open> Ouroboros II: figures \ldots \<close>
|
||||||
|
|
||||||
|
text\<open> The document class \inlineisar+figure+ --- supported by the \isadof text command
|
||||||
|
\inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper
|
||||||
|
such as @{docitem_ref \<open>fig_figures\<close>}.
|
||||||
|
\<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
|
||||||
|
during the exam and the preparation requires a very rigorous process, as the french
|
||||||
|
\<^emph>\<open>baccaleaureat\<close> and exams at The University of Sheffield.
|
||||||
|
|
||||||
|
We assume that the content has four different types of addressees, which have a different
|
||||||
|
\<^emph>\<open>view\<close> on the integrated document:
|
||||||
|
|
||||||
|
\<^item> the \<^emph>\<open>setter\<close>, \ie, the author of the exam,
|
||||||
|
\<^item> the \<^emph>\<open>checker\<close>, \ie, an internal person that checks
|
||||||
|
the exam for feasibility and non-ambiguity,
|
||||||
|
\<^item> the \<^emph>\<open>external examiner\<close>, \ie, an external person that checks
|
||||||
|
the exam for feasibility and non-ambiguity, and
|
||||||
|
\<^item> the \<^emph>\<open>student\<close>, \ie, the addressee of the exam.
|
||||||
|
\<close>
|
||||||
|
text\<open> The latter quality assurance mechanism is used in many universities,
|
||||||
|
where for organizational reasons the execution of an exam takes place in facilities
|
||||||
|
where the author of the exam is not expected to be physically present.
|
||||||
|
Furthermore, we assume a simple grade system (thus, some calculation is required).
|
||||||
|
|
||||||
|
\begin{figure}
|
||||||
|
\begin{isar}
|
||||||
|
doc_class Author = ...
|
||||||
|
datatype Subject = algebra | geometry | statistical
|
||||||
|
datatype Grade = A1 | A2 | A3
|
||||||
|
|
||||||
|
doc_class Header = examTitle :: string
|
||||||
|
examSubject :: Subject
|
||||||
|
date :: string
|
||||||
|
timeAllowed :: int -- minutes
|
||||||
|
|
||||||
|
datatype ContentClass = setter
|
||||||
|
| checker
|
||||||
|
| external_examiner
|
||||||
|
| student
|
||||||
|
|
||||||
|
doc_class Exam_item =
|
||||||
|
concerns :: "ContentClass set"
|
||||||
|
|
||||||
|
doc_class Exam_item =
|
||||||
|
concerns :: "ContentClass set"
|
||||||
|
|
||||||
|
type_synonym SubQuestion = string
|
||||||
|
\end{isar}
|
||||||
|
\caption{The core of the ontology modeling math exams.}
|
||||||
|
\label{fig:onto-exam}
|
||||||
|
\end{figure}
|
||||||
|
The heart of this ontology (see \autoref{fig:onto-exam}) is an alternation of questions and answers,
|
||||||
|
where the answers can consist of simple yes-no answers (QCM style check-boxes) or lists of formulas.
|
||||||
|
Since we do not
|
||||||
|
assume familiarity of the students with Isabelle (\inlineisar+term+ would assume that this is a
|
||||||
|
parse-able and type-checkable entity), we basically model a derivation as a sequence of strings
|
||||||
|
(see \autoref{fig:onto-questions}).
|
||||||
|
\begin{figure}
|
||||||
|
\begin{isar}
|
||||||
|
doc_class Answer_Formal_Step = Exam_item +
|
||||||
|
justification :: string
|
||||||
|
"term" :: "string"
|
||||||
|
|
||||||
|
doc_class Answer_YesNo = Exam_item +
|
||||||
|
step_label :: string
|
||||||
|
yes_no :: bool -- \<open>for checkboxes\<close>
|
||||||
|
|
||||||
|
datatype Question_Type =
|
||||||
|
formal | informal | mixed
|
||||||
|
|
||||||
|
doc_class Task = Exam_item +
|
||||||
|
level :: Level
|
||||||
|
type :: Question_Type
|
||||||
|
subitems :: "(SubQuestion *
|
||||||
|
(Answer_Formal_Step list + Answer_YesNo) list) list"
|
||||||
|
concerns :: "ContentClass set" <= "UNIV"
|
||||||
|
mark :: int
|
||||||
|
doc_class Exercise = Exam_item +
|
||||||
|
type :: Question_Type
|
||||||
|
content :: "(Task) list"
|
||||||
|
concerns :: "ContentClass set" <= "UNIV"
|
||||||
|
mark :: int
|
||||||
|
\end{isar}
|
||||||
|
\caption{An exam can contain different types of questions.}
|
||||||
|
\label{fig:onto-questions}
|
||||||
|
\end{figure}
|
||||||
|
|
||||||
|
In many institutions, it makes sense to have a rigorous process of validation
|
||||||
|
for exam subjects: is the initial question correct? Is a proof in the sense of the
|
||||||
|
question possible? We model the possibility that the @{term examiner} validates a
|
||||||
|
question by a sample proof validated by Isabelle (see \autoref{fig:onto-exam-monitor}).
|
||||||
|
In our scenario this sample proofs are completely \<^emph>\<open>intern\<close>, \ie, not exposed to the
|
||||||
|
students but just additional material for the internal review process of the exam.
|
||||||
|
\begin{figure}
|
||||||
|
\begin{isar}
|
||||||
|
doc_class Validation =
|
||||||
|
tests :: "term list" <="[]"
|
||||||
|
proofs :: "thm list" <="[]"
|
||||||
|
|
||||||
|
doc_class Solution = Exam_item +
|
||||||
|
content :: "Exercise list"
|
||||||
|
valids :: "Validation list"
|
||||||
|
concerns :: "ContentClass set" <= "{setter,checker,external_examiner}"
|
||||||
|
|
||||||
|
doc_class MathExam=
|
||||||
|
content :: "(Header + Author + Exercise) list"
|
||||||
|
global_grade :: Grade
|
||||||
|
where "\<lbrace>Author\<rbrace>$^+$ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>$^+$ "
|
||||||
|
\end{isar}
|
||||||
|
\caption{Validating exams.}
|
||||||
|
\label{fig:onto-exam-monitor}
|
||||||
|
\end{figure}
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
declare_reference*["fig_qcm"::figure]
|
||||||
|
|
||||||
|
text\<open> Using the \LaTeX{} package hyperref, it is possible to conceive an interactive
|
||||||
|
exam-sheets with multiple-choice and/or free-response elements
|
||||||
|
(see @{docitem_ref (unchecked) \<open>fig_qcm\<close>}). With the
|
||||||
|
help of the latter, it is possible that students write in a browser a formal mathematical
|
||||||
|
derivation---as part of an algebra exercise, for example---which is submitted to the examiners
|
||||||
|
electronically. \<close>
|
||||||
|
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>
|
||||||
|
|
||||||
|
chapter*[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>
|
||||||
|
|
||||||
|
section*[scholar_pide::example]\<open> A Scholarly Paper \<close>
|
||||||
|
text\<open> In \autoref{fig-Dogfood-II-bgnd1} and \autoref{fig-bgnd-text_section} we show how
|
||||||
|
hovering over links permits to explore its meta-information.
|
||||||
|
Clicking on a document class identifier permits to hyperlink into the corresponding
|
||||||
|
class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition
|
||||||
|
(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}).
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
open_monitor*["text-elements"::figure_group,
|
||||||
|
caption="''Exploring text elements.''"]
|
||||||
|
|
||||||
|
figure*["fig-Dogfood-II-bgnd1"::figure, spawn_columns=False,
|
||||||
|
relative_width="48",
|
||||||
|
src="''figures/Dogfood-II-bgnd1''"]
|
||||||
|
\<open>Exploring a Reference of a Text-Element.\<close>
|
||||||
|
|
||||||
|
figure*["fig-bgnd-text_section"::figure, spawn_columns=False,
|
||||||
|
relative_width="48",
|
||||||
|
src="''figures/Dogfood-III-bgnd-text_section''"]
|
||||||
|
\<open>Exploring the class of a text element.\<close>
|
||||||
|
|
||||||
|
close_monitor*["text-elements"]
|
||||||
|
|
||||||
|
|
||||||
|
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
|
||||||
|
caption="''Hyperlink to Class-Definition.''",relative_width="48",
|
||||||
|
src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''",
|
||||||
|
caption2="''Exploring an attribute.''",relative_width2="47",
|
||||||
|
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Hyperlinks.\<close>
|
||||||
|
|
||||||
|
|
||||||
|
declare_reference*["figDogfoodVIlinkappl"::figure]
|
||||||
|
text\<open> An ontological reference application in \autoref{figDogfoodVIlinkappl}: the ontology-dependant
|
||||||
|
antiquotation \inlineisar|@ {example ...}| refers to the corresponding text-elements. Hovering allows
|
||||||
|
for inspection, clicking for jumping to the definition. If the link does not exist or has a
|
||||||
|
non-compatible type, the text is not validated. \<close>
|
||||||
|
|
||||||
|
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
|
||||||
|
\<open> Exploring an attribute (hyperlinked to the class). \<close>
|
||||||
|
section*[cenelec_pide::example]\<open> CENELEC \<close>
|
||||||
|
declare_reference*[figfig3::figure]
|
||||||
|
text\<open> The corresponding view in @{docitem_ref (unchecked) \<open>figfig3\<close>} shows core part of a document,
|
||||||
|
coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows standard Isabelle antiquotations
|
||||||
|
@{cite "wenzel:isabelle-isar:2017"} into formal entities of a theory. This way, the informal parts
|
||||||
|
of a document get ``formal content'' and become more robust under change.\<close>
|
||||||
|
|
||||||
|
figure*[figfig3::figure,relative_width="80",src="''figures/antiquotations-PIDE''"]
|
||||||
|
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||||
|
|
||||||
|
declare_reference*[figfig5::figure]
|
||||||
|
text\<open> The subsequent sample in @{docitem_ref (unchecked) \<open>figfig5\<close>} shows the definition of an
|
||||||
|
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
|
||||||
|
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
|
||||||
|
device. This condition can not be established inside the formal theory but has to be
|
||||||
|
checked by system integration tests.\<close>
|
||||||
|
|
||||||
|
figure*[figfig5::figure, relative_width="80", src="''figures/srac-definition''"]
|
||||||
|
\<open> Defining a SRAC reference \ldots \<close>
|
||||||
|
figure*[figfig7::figure, relative_width="80", src="''figures/srac-as-es-application''"]
|
||||||
|
\<open> Using a SRAC as EC document reference. \<close>
|
||||||
|
|
||||||
|
text\<open> Now we reference in @{docitem_ref (unchecked) \<open>figfig7\<close>} this safety-related condition;
|
||||||
|
however, this happens in a context where general \<^emph>\<open>exported constraints\<close> are listed.
|
||||||
|
\isadof's checks establish that this is legal in the given ontology.
|
||||||
|
|
||||||
|
This example shows that ontological modeling is indeed adequate for large technical,
|
||||||
|
collaboratively developed documentations, where modifications can lead easily to incoherence.
|
||||||
|
The current checks help to systematically avoid this type of incoherence between formal and
|
||||||
|
informal parts. \<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
(*<*)
|
||||||
|
end
|
||||||
|
(*>*)
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "06_Conclusion"
|
theory "06_Conclusion"
|
||||||
imports "03_IsaDof"
|
imports "04_IsaDofCaseStudies"
|
||||||
(* imports "05_DesignImpl *)
|
(* imports "05_DesignImpl *)
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
After Width: | Height: | Size: 124 KiB |
After Width: | Height: | Size: 56 KiB |
After Width: | Height: | Size: 214 KiB |
After Width: | Height: | Size: 135 KiB |
After Width: | Height: | Size: 73 KiB |
|
@ -0,0 +1,758 @@
|
||||||
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||||
|
<!-- Created with Inkscape (http://www.inkscape.org/) -->
|
||||||
|
|
||||||
|
<svg
|
||||||
|
xmlns:dc="http://purl.org/dc/elements/1.1/"
|
||||||
|
xmlns:cc="http://creativecommons.org/ns#"
|
||||||
|
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
|
||||||
|
xmlns:svg="http://www.w3.org/2000/svg"
|
||||||
|
xmlns="http://www.w3.org/2000/svg"
|
||||||
|
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
|
||||||
|
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
|
||||||
|
width="142.92122mm"
|
||||||
|
height="182.73724mm"
|
||||||
|
viewBox="0 0 142.92122 182.73724"
|
||||||
|
version="1.1"
|
||||||
|
id="svg8"
|
||||||
|
inkscape:version="0.92.4 (5da689c313, 2019-01-14)"
|
||||||
|
sodipodi:docname="document-hierarchy.svg">
|
||||||
|
<defs
|
||||||
|
id="defs2">
|
||||||
|
<marker
|
||||||
|
inkscape:isstock="true"
|
||||||
|
style="overflow:visible"
|
||||||
|
id="marker1659"
|
||||||
|
refX="0"
|
||||||
|
refY="0"
|
||||||
|
orient="auto"
|
||||||
|
inkscape:stockid="Arrow1Lstart">
|
||||||
|
<path
|
||||||
|
transform="matrix(0.8,0,0,0.8,10,0)"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1.00000003pt;stroke-opacity:1"
|
||||||
|
d="M 0,0 5,-5 -12.5,0 5,5 Z"
|
||||||
|
id="path1657"
|
||||||
|
inkscape:connector-curvature="0" />
|
||||||
|
</marker>
|
||||||
|
<marker
|
||||||
|
inkscape:stockid="Arrow1Lstart"
|
||||||
|
orient="auto"
|
||||||
|
refY="0"
|
||||||
|
refX="0"
|
||||||
|
id="marker1601"
|
||||||
|
style="overflow:visible"
|
||||||
|
inkscape:isstock="true"
|
||||||
|
inkscape:collect="always">
|
||||||
|
<path
|
||||||
|
id="path1599"
|
||||||
|
d="M 0,0 5,-5 -12.5,0 5,5 Z"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1.00000003pt;stroke-opacity:1"
|
||||||
|
transform="matrix(0.8,0,0,0.8,10,0)"
|
||||||
|
inkscape:connector-curvature="0" />
|
||||||
|
</marker>
|
||||||
|
<marker
|
||||||
|
inkscape:stockid="Arrow1Lend"
|
||||||
|
orient="auto"
|
||||||
|
refY="0"
|
||||||
|
refX="0"
|
||||||
|
id="Arrow1Lend"
|
||||||
|
style="overflow:visible"
|
||||||
|
inkscape:isstock="true">
|
||||||
|
<path
|
||||||
|
id="path1224"
|
||||||
|
d="M 0,0 5,-5 -12.5,0 5,5 Z"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1.00000003pt;stroke-opacity:1"
|
||||||
|
transform="matrix(-0.8,0,0,-0.8,-10,0)"
|
||||||
|
inkscape:connector-curvature="0" />
|
||||||
|
</marker>
|
||||||
|
<marker
|
||||||
|
inkscape:stockid="Arrow1Lstart"
|
||||||
|
orient="auto"
|
||||||
|
refY="0"
|
||||||
|
refX="0"
|
||||||
|
id="marker1601-3"
|
||||||
|
style="overflow:visible"
|
||||||
|
inkscape:isstock="true"
|
||||||
|
inkscape:collect="always">
|
||||||
|
<path
|
||||||
|
id="path1599-6"
|
||||||
|
d="M 0,0 5,-5 -12.5,0 5,5 Z"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1.00000003pt;stroke-opacity:1"
|
||||||
|
transform="matrix(0.8,0,0,0.8,10,0)"
|
||||||
|
inkscape:connector-curvature="0" />
|
||||||
|
</marker>
|
||||||
|
<marker
|
||||||
|
inkscape:stockid="Arrow1Lstart"
|
||||||
|
orient="auto"
|
||||||
|
refY="0"
|
||||||
|
refX="0"
|
||||||
|
id="marker1601-3-5"
|
||||||
|
style="overflow:visible"
|
||||||
|
inkscape:isstock="true"
|
||||||
|
inkscape:collect="always">
|
||||||
|
<path
|
||||||
|
id="path1599-6-3"
|
||||||
|
d="M 0,0 5,-5 -12.5,0 5,5 Z"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1.00000003pt;stroke-opacity:1"
|
||||||
|
transform="matrix(0.8,0,0,0.8,10,0)"
|
||||||
|
inkscape:connector-curvature="0" />
|
||||||
|
</marker>
|
||||||
|
<marker
|
||||||
|
inkscape:stockid="Arrow1Lstart"
|
||||||
|
orient="auto"
|
||||||
|
refY="0"
|
||||||
|
refX="0"
|
||||||
|
id="marker1601-3-5-6"
|
||||||
|
style="overflow:visible"
|
||||||
|
inkscape:isstock="true"
|
||||||
|
inkscape:collect="always">
|
||||||
|
<path
|
||||||
|
id="path1599-6-3-2"
|
||||||
|
d="M 0,0 5,-5 -12.5,0 5,5 Z"
|
||||||
|
style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1.00000003pt;stroke-opacity:1"
|
||||||
|
transform="matrix(0.8,0,0,0.8,10,0)"
|
||||||
|
inkscape:connector-curvature="0" />
|
||||||
|
</marker>
|
||||||
|
</defs>
|
||||||
|
<sodipodi:namedview
|
||||||
|
id="base"
|
||||||
|
pagecolor="#ffffff"
|
||||||
|
bordercolor="#666666"
|
||||||
|
borderopacity="1.0"
|
||||||
|
inkscape:pageopacity="0.0"
|
||||||
|
inkscape:pageshadow="2"
|
||||||
|
inkscape:zoom="1.1074481"
|
||||||
|
inkscape:cx="168.34273"
|
||||||
|
inkscape:cy="356.31218"
|
||||||
|
inkscape:document-units="mm"
|
||||||
|
inkscape:current-layer="layer1"
|
||||||
|
showgrid="true"
|
||||||
|
showguides="true"
|
||||||
|
inkscape:guide-bbox="true"
|
||||||
|
inkscape:window-width="1918"
|
||||||
|
inkscape:window-height="1153"
|
||||||
|
inkscape:window-x="0"
|
||||||
|
inkscape:window-y="45"
|
||||||
|
inkscape:window-maximized="0"
|
||||||
|
fit-margin-top="0"
|
||||||
|
fit-margin-left="0"
|
||||||
|
fit-margin-right="0"
|
||||||
|
fit-margin-bottom="0">
|
||||||
|
<inkscape:grid
|
||||||
|
type="xygrid"
|
||||||
|
id="grid835"
|
||||||
|
originx="-169.50709"
|
||||||
|
originy="-152.70917" />
|
||||||
|
<sodipodi:guide
|
||||||
|
position="31.576254,228.29082"
|
||||||
|
orientation="0,1"
|
||||||
|
id="guide963"
|
||||||
|
inkscape:locked="false" />
|
||||||
|
</sodipodi:namedview>
|
||||||
|
<metadata
|
||||||
|
id="metadata5">
|
||||||
|
<rdf:RDF>
|
||||||
|
<cc:Work
|
||||||
|
rdf:about="">
|
||||||
|
<dc:format>image/svg+xml</dc:format>
|
||||||
|
<dc:type
|
||||||
|
rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
|
||||||
|
<dc:title></dc:title>
|
||||||
|
</cc:Work>
|
||||||
|
</rdf:RDF>
|
||||||
|
</metadata>
|
||||||
|
<g
|
||||||
|
inkscape:label="Layer 1"
|
||||||
|
inkscape:groupmode="layer"
|
||||||
|
id="layer1"
|
||||||
|
transform="translate(-169.50707,38.446423)">
|
||||||
|
<rect
|
||||||
|
style="opacity:1;fill:#cccccc;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.43869787;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
|
||||||
|
id="rect981"
|
||||||
|
width="42.997875"
|
||||||
|
height="88.106232"
|
||||||
|
x="219.99796"
|
||||||
|
y="-38.227074" />
|
||||||
|
<g
|
||||||
|
id="g886"
|
||||||
|
transform="translate(47.624996,-11.112507)"
|
||||||
|
style="fill:#444444">
|
||||||
|
<rect
|
||||||
|
y="-15.208323"
|
||||||
|
x="174.625"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-5"
|
||||||
|
style="opacity:1;fill:#444444;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-3"
|
||||||
|
y="-7.8323059"
|
||||||
|
x="193.23451"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#444444;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-7.8323059"
|
||||||
|
x="193.23451"
|
||||||
|
id="tspan831-5"
|
||||||
|
sodipodi:role="line">header</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891"
|
||||||
|
transform="translate(74.612502,43.920842)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g897"
|
||||||
|
style="fill:#f36b21"
|
||||||
|
transform="translate(-1.5875,10.054167)">
|
||||||
|
<rect
|
||||||
|
y="-20.421793"
|
||||||
|
x="223.91573"
|
||||||
|
height="18.979565"
|
||||||
|
width="36.885277"
|
||||||
|
id="rect837-3"
|
||||||
|
style="opacity:1;fill:#f36b21;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.62139261;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-6"
|
||||||
|
y="-13.123973"
|
||||||
|
x="242.44704"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#f36b21;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-13.123973"
|
||||||
|
x="242.44704"
|
||||||
|
id="tspan831-7"
|
||||||
|
sodipodi:role="line">context</tspan><tspan
|
||||||
|
id="tspan860"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-4.3045287"
|
||||||
|
x="242.44704"
|
||||||
|
sodipodi:role="line">definition</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-6"
|
||||||
|
transform="translate(74.612507,56.091689)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-2"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-9"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-1"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-2"
|
||||||
|
transform="translate(74.612507,67.733374)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-7"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-0"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-9"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<text
|
||||||
|
xml:space="preserve"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:7.76111126px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
x="225.19823"
|
||||||
|
y="-30.478563"
|
||||||
|
id="text961"><tspan
|
||||||
|
sodipodi:role="line"
|
||||||
|
id="tspan959"
|
||||||
|
x="225.19823"
|
||||||
|
y="-30.478563"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:7.76111126px;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Bold';stroke-width:0.26458332">A</tspan></text>
|
||||||
|
<flowRoot
|
||||||
|
xml:space="preserve"
|
||||||
|
id="flowRoot965"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:26.66666603px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none"
|
||||||
|
transform="scale(0.26458333)"><flowRegion
|
||||||
|
id="flowRegion967"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold'"><rect
|
||||||
|
id="rect969"
|
||||||
|
width="840"
|
||||||
|
height="720"
|
||||||
|
x="280"
|
||||||
|
y="-257.48032"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold'" /></flowRegion><flowPara
|
||||||
|
id="flowPara971" /></flowRoot> <rect
|
||||||
|
style="opacity:1;fill:#cccccc;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.44001329;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
|
||||||
|
id="rect981-6"
|
||||||
|
width="42.997875"
|
||||||
|
height="88.635391"
|
||||||
|
x="269.21042"
|
||||||
|
y="1.989586" />
|
||||||
|
<g
|
||||||
|
id="g886-7"
|
||||||
|
transform="translate(96.837493,29.104156)"
|
||||||
|
style="fill:#444444">
|
||||||
|
<rect
|
||||||
|
y="-15.208323"
|
||||||
|
x="174.625"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-5-5"
|
||||||
|
style="opacity:1;fill:#444444;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-3-3"
|
||||||
|
y="-7.8323059"
|
||||||
|
x="193.23451"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#444444;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-7.8323059"
|
||||||
|
x="193.23451"
|
||||||
|
id="tspan831-5-5"
|
||||||
|
sodipodi:role="line">header</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-62"
|
||||||
|
transform="translate(123.82498,84.137505)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-9"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-1"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-2"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g897-7"
|
||||||
|
style="fill:#f36b21"
|
||||||
|
transform="translate(47.624997,50.270836)">
|
||||||
|
<rect
|
||||||
|
y="-20.421793"
|
||||||
|
x="223.91573"
|
||||||
|
height="18.979565"
|
||||||
|
width="36.885277"
|
||||||
|
id="rect837-3-0"
|
||||||
|
style="opacity:1;fill:#f36b21;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.62139261;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-6-9"
|
||||||
|
y="-13.123973"
|
||||||
|
x="242.44704"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#f36b21;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-13.123973"
|
||||||
|
x="242.44704"
|
||||||
|
id="tspan831-7-3"
|
||||||
|
sodipodi:role="line">context</tspan><tspan
|
||||||
|
id="tspan860-6"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-4.3045287"
|
||||||
|
x="242.44704"
|
||||||
|
sodipodi:role="line">definition</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-6-0"
|
||||||
|
transform="translate(123.82499,96.308352)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-2-62"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-9-6"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-1-1"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-2-8"
|
||||||
|
transform="translate(123.82499,107.95004)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-7-7"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-0-9"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-9-2"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<text
|
||||||
|
xml:space="preserve"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:7.76111126px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
x="274.41068"
|
||||||
|
y="9.7380981"
|
||||||
|
id="text961-5"><tspan
|
||||||
|
sodipodi:role="line"
|
||||||
|
id="tspan959-9"
|
||||||
|
x="274.41068"
|
||||||
|
y="9.7380981"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:7.76111126px;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Bold';stroke-width:0.26458332">C</tspan></text>
|
||||||
|
<rect
|
||||||
|
style="opacity:1;fill:#cccccc;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.44001329;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
|
||||||
|
id="rect981-6-2"
|
||||||
|
width="42.997875"
|
||||||
|
height="88.635391"
|
||||||
|
x="169.72708"
|
||||||
|
y="1.989586" />
|
||||||
|
<g
|
||||||
|
id="g886-7-8"
|
||||||
|
transform="translate(-2.6458241,29.104156)"
|
||||||
|
style="fill:#444444">
|
||||||
|
<rect
|
||||||
|
y="-15.208323"
|
||||||
|
x="174.625"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-5-5-9"
|
||||||
|
style="opacity:1;fill:#444444;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-3-3-7"
|
||||||
|
y="-7.8323059"
|
||||||
|
x="193.23451"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#444444;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-7.8323059"
|
||||||
|
x="193.23451"
|
||||||
|
id="tspan831-5-5-3"
|
||||||
|
sodipodi:role="line">header</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-62-6"
|
||||||
|
transform="translate(24.341684,84.137505)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-9-1"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-1-2"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-2-9"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g897-7-3"
|
||||||
|
style="fill:#f36b21"
|
||||||
|
transform="translate(-51.858318,50.270836)">
|
||||||
|
<rect
|
||||||
|
y="-20.421793"
|
||||||
|
x="223.91573"
|
||||||
|
height="18.979565"
|
||||||
|
width="36.885277"
|
||||||
|
id="rect837-3-0-1"
|
||||||
|
style="opacity:1;fill:#f36b21;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.62139261;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-6-9-9"
|
||||||
|
y="-13.123973"
|
||||||
|
x="242.44704"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#f36b21;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-13.123973"
|
||||||
|
x="242.44704"
|
||||||
|
id="tspan831-7-3-4"
|
||||||
|
sodipodi:role="line">context</tspan><tspan
|
||||||
|
id="tspan860-6-7"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-4.3045287"
|
||||||
|
x="242.44704"
|
||||||
|
sodipodi:role="line">definition</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-6-0-8"
|
||||||
|
transform="translate(24.341689,96.308352)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-2-62-4"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-9-6-5"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-1-1-0"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-2-8-3"
|
||||||
|
transform="translate(24.341689,107.95004)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-7-7-6"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-0-9-1"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-9-2-0"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<text
|
||||||
|
xml:space="preserve"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:7.76111126px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
x="174.92735"
|
||||||
|
y="9.7380981"
|
||||||
|
id="text961-5-6"><tspan
|
||||||
|
sodipodi:role="line"
|
||||||
|
id="tspan959-9-1"
|
||||||
|
x="174.92735"
|
||||||
|
y="9.7380981"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:7.76111126px;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Bold';stroke-width:0.26458332">B</tspan></text>
|
||||||
|
<rect
|
||||||
|
style="opacity:1;fill:#cccccc;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.44001332;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
|
||||||
|
id="rect981-6-2-5"
|
||||||
|
width="42.997875"
|
||||||
|
height="88.635406"
|
||||||
|
x="219.99796"
|
||||||
|
y="55.435402" />
|
||||||
|
<g
|
||||||
|
id="g886-7-8-4"
|
||||||
|
transform="translate(47.625,82.549945)"
|
||||||
|
style="fill:#444444">
|
||||||
|
<rect
|
||||||
|
y="-15.208323"
|
||||||
|
x="174.625"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-5-5-9-7"
|
||||||
|
style="opacity:1;fill:#444444;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-3-3-7-6"
|
||||||
|
y="-7.8323059"
|
||||||
|
x="193.23451"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#444444;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-7.8323059"
|
||||||
|
x="193.23451"
|
||||||
|
id="tspan831-5-5-3-5"
|
||||||
|
sodipodi:role="line">header</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-62-6-6"
|
||||||
|
transform="translate(74.612506,137.58325)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-9-1-9"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-1-2-3"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-2-9-7"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g897-7-3-4"
|
||||||
|
style="fill:#f36b21"
|
||||||
|
transform="translate(-1.587496,103.71658)">
|
||||||
|
<rect
|
||||||
|
y="-20.421793"
|
||||||
|
x="223.91573"
|
||||||
|
height="18.979565"
|
||||||
|
width="36.885277"
|
||||||
|
id="rect837-3-0-1-5"
|
||||||
|
style="opacity:1;fill:#f36b21;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.62139261;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-6-9-9-2"
|
||||||
|
y="-13.123973"
|
||||||
|
x="242.44704"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#f36b21;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-13.123973"
|
||||||
|
x="242.44704"
|
||||||
|
id="tspan831-7-3-4-5"
|
||||||
|
sodipodi:role="line">context</tspan><tspan
|
||||||
|
id="tspan860-6-7-4"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-4.3045287"
|
||||||
|
x="242.44704"
|
||||||
|
sodipodi:role="line">definition</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-6-0-8-7"
|
||||||
|
transform="translate(74.612511,149.7541)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-2-62-4-4"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-9-6-5-4"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-1-1-0-3"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<g
|
||||||
|
id="g891-2-8-3-0"
|
||||||
|
transform="translate(74.612511,161.39578)"
|
||||||
|
style="fill:#2a9c16">
|
||||||
|
<rect
|
||||||
|
y="-31.083334"
|
||||||
|
x="148.16667"
|
||||||
|
height="10.583333"
|
||||||
|
width="37.041668"
|
||||||
|
id="rect837-7-7-6-7"
|
||||||
|
style="opacity:1;fill:#2a9c16;fill-opacity:0.81415926;stroke:#000000;stroke-width:0.46499997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
|
||||||
|
<text
|
||||||
|
id="text833-0-9-1-8"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-size:7.05555534px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#2a9c16;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
xml:space="preserve"><tspan
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:600;font-stretch:normal;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Semi-Bold';fill:#080808;stroke-width:0.26458332"
|
||||||
|
y="-23.707317"
|
||||||
|
x="166.77618"
|
||||||
|
id="tspan831-9-2-0-6"
|
||||||
|
sodipodi:role="line">command</tspan></text>
|
||||||
|
</g>
|
||||||
|
<text
|
||||||
|
xml:space="preserve"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:7.76111126px;line-height:1.25;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Bold';text-align:center;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
|
||||||
|
x="225.19823"
|
||||||
|
y="63.183918"
|
||||||
|
id="text961-5-6-1"><tspan
|
||||||
|
sodipodi:role="line"
|
||||||
|
id="tspan959-9-1-4"
|
||||||
|
x="225.19823"
|
||||||
|
y="63.183918"
|
||||||
|
style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:7.76111126px;font-family:'Open Sans';-inkscape-font-specification:'Open Sans Bold';stroke-width:0.26458332">D</tspan></text>
|
||||||
|
<path
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.26458332px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:url(#marker1601)"
|
||||||
|
d="m 262.46667,-33.199991 c 30.49153,0.623102 31.75,0 31.75,0 -0.0639,46.016494 -0.52918,33.33747891 -0.52918,33.33747891"
|
||||||
|
id="path1174"
|
||||||
|
inkscape:connector-curvature="0"
|
||||||
|
sodipodi:nodetypes="ccc" />
|
||||||
|
<path
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.26458332px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:url(#marker1601-3)"
|
||||||
|
d="m 219.22289,-33.199995 c -30.49154,0.623102 -31.75001,0 -31.75001,0 0.0639,46.016495 0.52918,33.33748106 0.52918,33.33748106"
|
||||||
|
id="path1174-7"
|
||||||
|
inkscape:connector-curvature="0"
|
||||||
|
sodipodi:nodetypes="ccc" />
|
||||||
|
<path
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.26458332px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:url(#marker1601-3-5)"
|
||||||
|
d="m 186.93719,90.945262 c 0.6231,30.491598 0,31.750068 0,31.750068 46.0165,-0.0639 30.02112,-0.32034 30.02112,-0.32034"
|
||||||
|
id="path1174-7-5"
|
||||||
|
inkscape:connector-curvature="0"
|
||||||
|
sodipodi:nodetypes="ccc" />
|
||||||
|
<path
|
||||||
|
style="fill:none;stroke:#000000;stroke-width:0.26458332px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:url(#marker1601-3-5-6)"
|
||||||
|
d="m 295.78153,90.945286 c -0.6231,30.491664 0,31.750134 0,31.750134 -46.0165,-0.0639 -30.02112,-0.32034 -30.02112,-0.32034"
|
||||||
|
id="path1174-7-5-9"
|
||||||
|
inkscape:connector-curvature="0"
|
||||||
|
sodipodi:nodetypes="ccc" />
|
||||||
|
</g>
|
||||||
|
</svg>
|
After Width: | Height: | Size: 38 KiB |
After Width: | Height: | Size: 81 KiB |