forked from Isabelle_DOF/Isabelle_DOF
Removed example - not needed as we have Chapter 3 (and various examples in the actual distribution).
This commit is contained in:
parent
898656077f
commit
7c66be090a
|
|
@ -659,8 +659,6 @@ super-classes. Overloading of attributes is not permitted in
|
|||
\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
subsection*["commonlib"::technical]\<open>Common Ontology Library (COL)\<close>
|
||||
text\<open> The COL library is used to capture a couple of text-elements
|
||||
that are expected to be common to all document types, a class
|
||||
|
|
@ -702,199 +700,6 @@ by a text-element with a higher level, \ie{}, must contain a section or subsecti
|
|||
\<close>
|
||||
|
||||
|
||||
section\<open>Example\<close>
|
||||
text\<open>We illustrate the design of \dof by modeling a small ontology
|
||||
that can be used for writing formal specifications that, \eg, could
|
||||
build the basis for an ontology for certification documents used in
|
||||
processes such as Common Criteria~@{cite "cc:cc-part3:2006"} or CENELEC
|
||||
50128~@{cite "bsi:50128:2014"}.@{footnote \<open>The \isadof distribution
|
||||
contains an ontology for writing documents for a certification
|
||||
according to CENELEC 50128.\<close>} Moreover, in examples of certification
|
||||
documents, we refer to a controller of a steam boiler that is
|
||||
inspired by the famous steam boiler formalization
|
||||
challenge~@{cite "abrial:steam-boiler:1996"}.\<close>
|
||||
|
||||
text\<open>
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class title = short_title :: "string option" <= "None"
|
||||
doc_class author = email :: "string" <= "''''"
|
||||
|
||||
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
||||
|
||||
doc_class abstract =
|
||||
keywordlist :: "string list" <= []
|
||||
safety_level :: "classification" <= "SIL3"
|
||||
doc_class text_section =
|
||||
authored_by :: "author set" <= "{}"
|
||||
level :: "int option" <= "None"
|
||||
|
||||
type_synonym notion = string
|
||||
|
||||
doc_class introduction = text_section +
|
||||
authored_by :: "author set" <= "UNIV"
|
||||
uses :: "notion set"
|
||||
doc_class claim = introduction +
|
||||
based_on :: "notion list"
|
||||
doc_class technical = text_section +
|
||||
formal_results :: "thm list"
|
||||
doc_class "d$$efinition" = technical +
|
||||
is_formal :: "bool"
|
||||
property :: "term list" <= "[]"
|
||||
|
||||
datatype kind = expert_opinion | argument | proof
|
||||
|
||||
doc_class result = technical +
|
||||
evidence :: kind
|
||||
property :: "thm list" <= "[]"
|
||||
doc_class example = technical +
|
||||
referring_to :: "(notion + d$$efinition) set" <= "{}"
|
||||
doc_class "conclusion" = text_section +
|
||||
establish :: "(claim \<times> result) set"
|
||||
\end{isar}%$
|
||||
|
||||
\caption{An example ontology modeling simple certification documents, including
|
||||
scientific papers such as~@{cite "brucker.ea:isabelle-ontologies:2018"}; also
|
||||
recall \autoref{fig:dof-ide}.}\label{lst:doc}
|
||||
\end{figure}
|
||||
\<close>
|
||||
text\<open>
|
||||
\autoref{lst:doc} shows an example ontology for mathematical papers
|
||||
(an extended version of this ontology was used for writing
|
||||
@{cite "brucker.ea:isabelle-ontologies:2018"}, also recall
|
||||
\autoref{fig:dof-ide}). The commands \inlineisar+datatype+ (modeling
|
||||
fixed enumerations) and \inlineisar+type_synonym+ (defining type
|
||||
synonyms) are standard mechanisms in HOL systems. Since ODL is an
|
||||
add-on, we have to quote sometimes constant symbols (\eg,
|
||||
\inlineisar+"proof"+) to avoid confusion with predefined keywords. ODL
|
||||
admits overriding (such as \inlineisar+authored_by+ in the document
|
||||
class \inlineisar+introduction+), where it is set to another library
|
||||
constant, but no overloading. All \inlineisar+text_section+ elements
|
||||
have an optional \inlineisar+level+ attribute, which will be used in
|
||||
the output generation for the decision if the context is a section
|
||||
header and its level (\eg, chapter, section, subsection). While
|
||||
\<open>within\<close> an inheritance hierarchy overloading is prohibited,
|
||||
attributes may be re-declared freely in independent parts (as is the
|
||||
case for \inlineisar+property+).\<close>
|
||||
|
||||
|
||||
text\<open>
|
||||
We can now annotate a text as follows. First, we have to place a
|
||||
particular document into the context of our conceptual example
|
||||
ontology (\autoref{lst:doc}):
|
||||
\begin{isar}
|
||||
theory Steam_Boiler
|
||||
imports
|
||||
tiny_cert (* The ontology defined in Listing 1.1. *)
|
||||
begin
|
||||
\end{isar}
|
||||
This opens a new document (theory), called
|
||||
\texttt{Steam\_Boiler} that imports our conceptual example ontology
|
||||
``\texttt{tiny\_cert}'' (stored in a file
|
||||
\texttt{tiny\_cert.thy}).\footnote{The usual import-mechanisms of the
|
||||
Isabelle document model applies also to ODL: ontologies can be
|
||||
extended, several ontologies may be imported, a document can
|
||||
validate several ontologies.}
|
||||
|
||||
\noindent Now we can continue to annotate our text as follows:
|
||||
\begin{isar}
|
||||
title*[a] \<Open>The Steam Boiler Controller\<Close>
|
||||
abstract*[abs, safety_level="SIL4", keywordlist = "[''controller'']"]\<Open>
|
||||
We present a formalization of a program which serves to control the
|
||||
level of water in a steam boiler.
|
||||
\<Close>
|
||||
|
||||
section*[intro::introduction]\<Open>Introduction\<Close>
|
||||
text\<Open>We present ...\<Close>
|
||||
|
||||
section*[T1::technical]\<Open>Physical Environment\<Close>
|
||||
text\<Open>
|
||||
The system comprises the following units
|
||||
[*] the steam-boiler
|
||||
[*] a device to measure the quantity of water in the steam-boiler
|
||||
[*] ...
|
||||
\<Close>
|
||||
\end{isar}
|
||||
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
Where \inlineisar+title*[a ...]+ is a predefined macro for
|
||||
\inlineisar+text*[a::title,...]\<Open>...\<Close>+ (similarly \inlineisar+abstract*+).
|
||||
The macro \inlineisar+section*+ assumes a class-id referring to a class that has
|
||||
a \inlineisar+level+ attribute. We continue our example text:
|
||||
\begin{isar}[mathescape]
|
||||
text*[c1::contrib_claim, based_on="[''pumps'',''steam boiler'']" ]\<Open>
|
||||
As indicated in <@>{introduction "intro"}, we the water level of the
|
||||
boiler is always between the minimum a$$nd the maximum allowed level.
|
||||
\<Close>
|
||||
\end{isar}
|
||||
\<close>
|
||||
text\<open>
|
||||
The first text element in this example fragment \<^emph>\<open>defines\<close> the
|
||||
text entity \inlineisar+c1+ and also references the formerly defined
|
||||
text element \inlineisar+intro+ (which will be represented in the PDF
|
||||
output, for example, by a text anchor ``Section 1'' and a hyperlink to
|
||||
its beginning). The antiquotation \inlineisar+<@>{introduction ...}+,
|
||||
which is automatically generated from the ontology, is immediately
|
||||
validated (the link to \inlineisar+intro+ is defined) and type-checked (it
|
||||
is indeed a link to an \inlineisar+introduction+
|
||||
text-element). Moreover, the IDE automatically provides editing and
|
||||
development support such as auto-completion or the possibility to
|
||||
``jump'' to its definition by clicking on the antiquotation. The
|
||||
consistency checking ensures, among others, that the final document
|
||||
will not contain any ``dangling references'' or references to entities of
|
||||
another type.
|
||||
\<close>
|
||||
text\<open>
|
||||
\dof as such does not require a particular evaluation strategy;
|
||||
however, if the underlying implementation is based on a
|
||||
declaration-before-use strategy, a mechanism for forward declarations
|
||||
of references is necessary:
|
||||
\begin{isar}
|
||||
declare_reference* [<meta-args>]
|
||||
\end{isar}
|
||||
This command declares the existence of a text-element and allows for
|
||||
referencing it, although the actual text-element will occur later in
|
||||
the document.
|
||||
\<close>
|
||||
|
||||
|
||||
subsection\<open>Editing Documents with Ontology Meta-Data: Inner Syntax\<close>
|
||||
text\<open>We continue our running example as follows:
|
||||
\begin{isar}[mathescape]
|
||||
text*[d1::definition]\<Open>
|
||||
We define the water level <@>{term "level"} of a system state
|
||||
<@>{term "\<sigma>"} of the steam boiler as follows:
|
||||
\<Close>
|
||||
definition level :: "state \<rightarrow> real" where
|
||||
"level \<sigma> = level0 + ..."
|
||||
update_instance*[d1::definition,
|
||||
property += "[<@>{term ''level \<sigma> = level0 + ...''}]"]
|
||||
|
||||
text*[only::result,evidence="proof"]\<Open>
|
||||
The water level is never lower than <@>{term "level0"}:
|
||||
\<Close>
|
||||
theorem level_always_above_level_0: "\<forall> \<sigma>. level \<sigma> \<geq> level0"
|
||||
unfolding level_def
|
||||
by auto
|
||||
update_instance*[only::result,
|
||||
property += "[<@>{thm ''level_always_above_level_0''}]"]
|
||||
\end{isar}
|
||||
\<close>
|
||||
text\<open>
|
||||
As mentioned earlier, instances of document classes are mutable. We
|
||||
use this feature to modify meta-data of these text-elements and
|
||||
``assign'' them to the property-list afterwards and add results
|
||||
from Isabelle definitions and proofs. The notation
|
||||
\inlineisar|A+=X| stands for \inlineisar|A := A + X|. This mechanism
|
||||
can also be used to define the required relation between \<^emph>\<open>claims\<close>
|
||||
and \<^emph>\<open>results\<close> required in the \inlineisar|establish|-relation
|
||||
required in a \inlineisar|summary|.
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
section*["document-templates"::technical]\<open>Defining Document Templates\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
|
|||
Loading…
Reference in New Issue