Fix some typos
This commit is contained in:
Nicolas Méric
parent
6927781d26
commit
5b618562a2
|
|
@ -140,7 +140,8 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
|
|||
the link between formal and informal content in documents in a machine
|
||||
checked way. These links can connect both text elements as well as formal
|
||||
modelling elements such as terms, definitions, code and logical formulas,
|
||||
alltogether *\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||
alltogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
|
|
|
|||
|
|
@ -91,7 +91,7 @@ text\<open>
|
|||
by simp\<close>}
|
||||
\<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
|
||||
@{boxed_pdf [display] \<open>The axiom refl\<close>}
|
||||
\<^item> a red background for For (S)ML-code:
|
||||
\<^item> a red background for (S)ML-code:
|
||||
@{boxed_sml [display] \<open>fun id x = x\<close>}
|
||||
\<^item> a yellow background for \LaTeX-code:
|
||||
@{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>}
|
||||
|
|
|
|||
|
|
@ -153,7 +153,7 @@ text\<open>
|
|||
"wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"} which
|
||||
in many features over-accomplishes the required features of \<^dof>. For example, current Isabelle
|
||||
versions offer cascade-syntaxes (different syntaxes and even parser-technologies which can be
|
||||
nested along the \<open>\<open>...\<close>\<close> barriers, while \<^dof> actually only requires a two-level syntax model.
|
||||
nested along the \<open>\<open>...\<close>\<close> barriers), while \<^dof> actually only requires a two-level syntax model.
|
||||
\<close>
|
||||
(* end experiment *)
|
||||
|
||||
|
|
|
|||
|
|
@ -267,7 +267,7 @@ users are:
|
|||
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
|
||||
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
|
||||
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
|
||||
\<^item> The file \<^boxed_bash>\<open>praemble.tex\<close>\<^index>\<open>praemble.tex\<close>, which allows users to add additional
|
||||
\<^item> The file \<^boxed_bash>\<open>preamble.tex\<close>\<^index>\<open>preamble.tex\<close>, which allows users to add additional
|
||||
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
|
||||
\<close>
|
||||
|
||||
|
|
@ -284,7 +284,7 @@ text\<open>
|
|||
\<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text,
|
||||
heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing
|
||||
between statements, definitions and proofs which is ontologically tracked. However, wrt.
|
||||
to the possible linking between the underlying formal theory and this mathematical presentation,
|
||||
the possible linking between the underlying formal theory and this mathematical presentation,
|
||||
it follows a pragmatic path without any ``deep'' linking to types, terms and theorems,
|
||||
deliberately not exploiting \<^isadof> 's full potential with this regard.
|
||||
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
|
||||
|
|
@ -346,7 +346,7 @@ context of this document; this is a decisive feature of \<^isadof> that conventi
|
|||
languages lack.\<close>
|
||||
|
||||
text\<open>We continue by the introduction of a main class: the text-element \<open>text_section\<close> (in contrast
|
||||
to \<open>figure\<close> or \<open>table\<close> or similar. Note that
|
||||
to \<open>figure\<close> or \<open>table\<close> or similar). Note that
|
||||
the \<open>main_author\<close> is typed with the class \<open>author\<close>, a HOL type that is automatically derived from
|
||||
the document class definition \<open>author\<close> shown above. It is used to express which author currently
|
||||
``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even
|
||||
|
|
@ -460,7 +460,7 @@ later is shown in \<^figure>\<open>fig01\<close> in its presentation as the inte
|
|||
|
||||
Note that the use in the ontology-generated antiquotation \<^theory_text>\<open>@{definition X4}\<close>
|
||||
is type-checked; referencing \<^verbatim>\<open>X4\<close> as \<^theory_text>\<open>theorem\<close> would be a type-error and be reported directly
|
||||
by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. to the sub-typing
|
||||
by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. the sub-typing
|
||||
hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jedit; a click will cause the IDE to present the
|
||||
defining occurrence of this text-element in the integrated source.
|
||||
|
||||
|
|
@ -528,7 +528,7 @@ doc_class related_work = conclusion +
|
|||
\<close>}
|
||||
*)
|
||||
text\<open> In the following, we present some other text-elements provided by the Common Ontology Library
|
||||
in @{theory "Isabelle_DOF.Isa_COL"}. it provides a document class for figures:
|
||||
in @{theory "Isabelle_DOF.Isa_COL"}. It provides a document class for figures:
|
||||
|
||||
@{boxed_theory_text [display]\<open>
|
||||
datatype placement = h | t | b | ht | hb
|
||||
|
|
@ -651,7 +651,7 @@ text\<open>
|
|||
which is usually a collaborative 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
|
||||
of what has to be demonstrated and where, and how the traceability of requirements through
|
||||
design-models over code to system environment assumptions has to be assured.
|
||||
|
||||
In the sequel, we present a simplified version of an ontological model used in a
|
||||
|
|
@ -675,7 +675,7 @@ doc_class assumption = requirement +
|
|||
|
||||
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
|
||||
like an explication of 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.
|
||||
|
|
@ -683,23 +683,23 @@ 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
|
||||
certification process, be 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>
|
||||
within the certification process, be 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
|
||||
of the evaluation target. Their traceability throughout the certification
|
||||
is therefore particularly critical. This is naturally modeled as follows:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class ec = assumption +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
doc_class srac = ec +
|
||||
doc_class SRAC = ec +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
\<close>}
|
||||
|
||||
|
|
@ -725,7 +725,7 @@ subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
|
|||
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
|
||||
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
|
||||
conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
|
||||
conforming to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
|
||||
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.\<close>
|
||||
|
||||
|
|
@ -882,14 +882,14 @@ underlying logical context, which turns the arguments into \<^emph>\<open>formal
|
|||
source, in contrast to the free-form antiquotations which basically influence the presentation.
|
||||
|
||||
We still mention a few of these document antiquotations here:
|
||||
\<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> ou \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference
|
||||
\<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> or \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference
|
||||
to a theorem; the additional "style" argument changes the presentation by printing the
|
||||
formula into the output instead of the reference itself,
|
||||
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows to derive \<open>prop\<close> on the fly, thus garantee
|
||||
that it is a corrollary of the current context,
|
||||
\<^item> \<^theory_text>\<open>@{term \<open>term\<close> }\<close> parses and type-checks \<open>term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{ML \<open>ml-term\<close> }\<close> pa,rses and type-checks \<open>ml-term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{ML \<open>ml-term\<close> }\<close> parses and type-checks \<open>ml-term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{ML_file \<open>ml-file\<close> }\<close> parses the path for \<open>ml-file\<close> and
|
||||
verifies its existance in the (Isabelle-virtual) file-system,
|
||||
\<^item> ...
|
||||
|
|
@ -900,9 +900,9 @@ Isabelle. This may be over-precise and a burden to readers not familiar with Isa
|
|||
motivate authors to choose the aforementioned freeform-style.
|
||||
\<close>
|
||||
|
||||
subsection\<open>A \<^verbatim>\<open>technical_report\<close> in tight-checking-style: \<open>MyCommentedIsabelle\<close> - Programming Manual \<close>
|
||||
subsection\<open>A \<^verbatim>\<open>technical_report\<close> in tight-checking-style: \<open>TR_MyCommentedIsabelle\<close> - Programming Manual \<close>
|
||||
|
||||
text\<open>An example of tight checking is a small programming programming manual developed by the
|
||||
text\<open>An example of tight checking is a small programming manual developed by the
|
||||
second author in order to document programming trick discoveries while implementing in Isabelle.
|
||||
While not necessarily a meeting standards of a scientific text, it appears to us that this information
|
||||
is often missing in the Isabelle community.
|
||||
|
|
@ -934,9 +934,9 @@ figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabel
|
|||
\<open>A table with a number of SML functions, together with their type.\<close>
|
||||
|
||||
text\<open>
|
||||
\<open>MyCommentedIsabelle\<close> is written according to the @{theory "Isabelle_DOF.technical_report"}
|
||||
ontology. \<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source gives an idea why
|
||||
it tight-checking allows for keeping track of underlying Isabelle changes:
|
||||
\<open>TR_MyCommentedIsabelle\<close> is written according to the @{theory "Isabelle_DOF.technical_report"}
|
||||
ontology. \<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why
|
||||
its tight-checking allows for keeping track of underlying Isabelle changes:
|
||||
Any reference to an SML operation in some library module is type-checked, and the displayed
|
||||
SML-type really corresponds to the type of the operations in the underlying SML environment.
|
||||
In the pdf output, these text-fragments were displayed verbatim.
|
||||
|
|
@ -976,7 +976,7 @@ document generation (\<^eg>, HTML) which, naturally, are only available to docum
|
|||
too complex native \<^LaTeX>-commands.
|
||||
|
||||
Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
|
||||
create dangeling references during the document generation that break the document generation.
|
||||
create dangling references during the document generation that break the document generation.
|
||||
|
||||
Finally, we recommend to use the @{command "check_doc_global"} command at the end of your
|
||||
document to check the global reference structure.
|
||||
|
|
|
|||
|
|
@ -119,7 +119,7 @@ text\<open>
|
|||
|
||||
text\<open>
|
||||
The \<^isadof> ontology specification language consists basically on a notation for document classes,
|
||||
where the attributes were typed with HOL-types and can be instantiated by terms HOL-terms, \<^ie>,
|
||||
where the attributes were typed with HOL-types and can be instantiated by HOL-terms, \<^ie>,
|
||||
the actual parsers and type-checkers of the Isabelle system were reused. This has the particular
|
||||
advantage that \<^isadof> commands can be arbitrarily mixed with Isabelle/HOL commands providing the
|
||||
machinery for type declarations and term specifications such
|
||||
|
|
@ -153,7 +153,7 @@ text\<open>
|
|||
\<^boxed_theory_text>\<open>_ option\<close>, \<^boxed_theory_text>\<open>_ list\<close>, \<^boxed_theory_text>\<open>_ set\<close>, or products
|
||||
\<^boxed_theory_text>\<open>_ \<times> _\<close>. As a consequence of the
|
||||
document model, ODL definitions may be arbitrarily intertwined with standard HOL type definitions.
|
||||
Finally, document class definitions result in themselves in a HOL-types in order to allow \<^emph>\<open>links\<close>
|
||||
Finally, document class definitions result in themselves in a HOL-type in order to allow \<^emph>\<open>links\<close>
|
||||
to and between ontological concepts.
|
||||
\<close>
|
||||
|
||||
|
|
@ -167,7 +167,7 @@ text\<open>
|
|||
in \<^isadof>:
|
||||
\<^item> \<open>name\<close>:\<^index>\<open>name@\<open>name\<close>\<close>
|
||||
with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers
|
||||
(called \<open>short_id\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers
|
||||
(called \<open>short_ident\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers
|
||||
in \<^boxed_theory_text>\<open> ... \<close> which might contain certain ``quasi-letters'' such
|
||||
as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~@{cite "wenzel:isabelle-isar:2020"} for
|
||||
details).
|
||||
|
|
@ -230,7 +230,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
|
|||
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
|
||||
\<^rail>\<open> name '::' '"' type '"' default_clause? \<close>
|
||||
\<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close>
|
||||
An invariants can be specified as predicate over document classes represented as
|
||||
Invariants can be specified as predicates over document classes represented as
|
||||
records in HOL. Note that sufficient type information must be provided in order to
|
||||
disambiguate the argument of the \<open>\<lambda>\<close>-expression.
|
||||
\<^rail>\<open> 'inv' (name '::')? '"' term '"' \<close>
|
||||
|
|
@ -254,7 +254,7 @@ text\<open>
|
|||
\inlineltx|\newisadof[]{}|\<^index>\<open>newisadof@\inlineltx{\newisadof}\<close>\<^index>\<open>document class!PDF\<close>
|
||||
command for defining a dedicated layout for a document class in \<^LaTeX>. Such a document
|
||||
class-specific \<^LaTeX>-definition can not only provide a specific layout (\<^eg>, a specific
|
||||
highlighting, printing of certain attributes), it can also generate entries in in the table of
|
||||
highlighting, printing of certain attributes), it can also generate entries in the table of
|
||||
contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure
|
||||
of the \<^boxed_theory_text>\<open>doc_class\<close>-command:
|
||||
|
||||
|
|
@ -339,7 +339,7 @@ layout (such as \<^LaTeX>); these commands have to be wrapped into
|
|||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
|
||||
|
||||
subsection\<open>Ontologic Text-Elements and their Management\<close>
|
||||
text\<open> \<^theory_text>\<open>text*[oid::cid, ...] \<open>\<open>\<close> \<dots> text \<dots> \<open>\<close>\<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
text\<open> \<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
an object of meta-data belonging to the class \<^theory_text>\<open>cid\<close>. This is viewed as the \<^emph>\<open>definition\<close> of
|
||||
an instance of a document class. This instance object is attached to the text-element
|
||||
and makes it thus "trackable" for \<^isadof>, \<^ie>, it can be referenced via the \<^theory_text>\<open>oid\<close>, its attributes
|
||||
|
|
@ -1039,7 +1039,7 @@ text\<open>
|
|||
\<^path>\<open>llncs.cls\<close>), which cannot be re-distributed due to copyright restrictions.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Developing Ontologies and their Represenation Mappings\<close>
|
||||
subsection\<open>Developing Ontologies and their Representation Mappings\<close>
|
||||
text\<open>
|
||||
The document core \<^emph>\<open>may\<close>, but \<^emph>\<open>must\<close> not use Isabelle definitions or proofs for checking the
|
||||
formal content---this manual is actually an example of a document not containing any proof.
|
||||
|
|
@ -1194,7 +1194,7 @@ text\<open>
|
|||
|
||||
subsection\<open>Tips, Tricks, and Known Limitations\<close>
|
||||
text\<open>
|
||||
In this sectin, we sill discuss several tips and tricks for developing
|
||||
In this section, we will discuss several tips and tricks for developing
|
||||
new or adapting existing document templates or \<^LaTeX>-represenations of ontologies.
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue