Import of DOF manual changes from /2021-ITP-PMTI
This commit is contained in:
Nicolas Méric
parent
eb9edd66d5
commit
3895ba550c
|
|
@ -119,10 +119,17 @@ text\<open>
|
|||
G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
|
||||
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
|
||||
\href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}.
|
||||
|
||||
\end{quote}
|
||||
A \<^BibTeX>-entry is available at:
|
||||
\<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019\<close>.
|
||||
\<^item> for an application of \<^isadof> in the context of certifications:
|
||||
\begin{quote}\small
|
||||
A.~D. Brucker and B.~Wolff.
|
||||
Using Ontologies in Formal Developments Targeting Certification.
|
||||
In W. Ahrendt and S. Tarifa, editors. \<^emph>\<open>Integrated Formal Methods (IFM)\<close>, number 11918.
|
||||
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
|
||||
\href{https://doi.org/10.1007/978-3-030-34968-4\_4}.
|
||||
\end{quote}
|
||||
\<close>
|
||||
subsubsection\<open>Availability\<close>
|
||||
text\<open>
|
||||
|
|
|
|||
|
|
@ -43,11 +43,11 @@ The current system framework offers moreover the following features:
|
|||
\<^item> an extensible front-end language Isabelle/Isar, and,
|
||||
\<^item> last but not least, an LCF style, generic theorem prover kernel as
|
||||
the most prominent and deeply integrated system component.
|
||||
|
||||
|
||||
\<close>
|
||||
text\<open>
|
||||
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers,
|
||||
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
|
||||
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure\<^boxed_sml>\<open>Context\<close>.
|
||||
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>.
|
||||
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
|
||||
ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>.
|
||||
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
|
||||
|
|
@ -70,13 +70,20 @@ declare_reference*["fig:dependency"::text_section]
|
|||
|
||||
|
||||
text\<open>
|
||||
We assume a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files) that can depend acyclically on each other.
|
||||
The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close> bindex>\<open>document-centric view\<close> of
|
||||
a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close>
|
||||
that may mutually depend and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
|
||||
\<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
|
||||
|
||||
Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files); dependencies are restricted to be
|
||||
acyclic at this level.
|
||||
Sub-documents can have different document types in order to capture documentations consisting of
|
||||
documentation, models, proofs, code of various forms and other technical artifacts. We call the
|
||||
main sub-document type, for historical reasons, \<^emph>\<open>theory\<close>-files. A theory file\<^bindex>\<open>theory!file\<close>
|
||||
consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body
|
||||
consisting of a sequence of \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
|
||||
consisting of a sequence of document elements called
|
||||
\<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
|
||||
the header consists of a sequence of commands used for introductory text elements not depending on
|
||||
any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a
|
||||
\<^boxed_theory_text>\<open>keyword\<close> section, for example:
|
||||
|
|
@ -96,30 +103,43 @@ text\<open> A text-element \<^index>\<open>text-element\<close> may look like th
|
|||
@{boxed_theory_text [display]\<open>
|
||||
text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl},
|
||||
we obtain in \<Gamma> for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>}
|
||||
so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||
contains characters and and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close>
|
||||
(here \<^theory_text>\<open>@{term "fac 5"}).\<close>
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
We distinguish fundamentally two different syntactic levels:
|
||||
\<^item> the \<^emph>\<open>outer-syntax\<close>\<^bindex>\<open>syntax!outer\<close>\<^index>\<open>outer syntax|see {syntax, outer}\<close> (\<^ie>, the
|
||||
syntax for commands) is processed by a lexer-library and parser combinators built on top, and
|
||||
\<^item> the \<^emph>\<open>inner-syntax\<close>\<^bindex>\<open>syntax!inner\<close>\<^index>\<open>inner syntax|see {syntax, inner}\<close> (\<^ie>, the
|
||||
syntax for \<open>\<lambda>\<close>-terms in HOL) with its own parametric polymorphism type checking.
|
||||
text\<open>While we concentrate in this manual on \<^theory_text>\<open>text\<close>-document elements --- this is the main
|
||||
use of \<^dof> in its current stage --- it is important to note that there are actually three
|
||||
families of ``ontology aware'' document elements with analogous
|
||||
syntax to standard ones. The difference is a bracket with meta-data of the form:
|
||||
@{theory_text [display,indent=5, margin=70]
|
||||
\<open>
|
||||
text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some semi-formal text \<close>
|
||||
ML*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some SML code \<close>
|
||||
value*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some annotated \<lambda>-term \<close>
|
||||
\<close>}
|
||||
|
||||
Depending on the family, we will speak about \<^emph>\<open>(formal) text-contexts\<close>,\<^index>\<open>formal text-contexts\<close>
|
||||
\<^emph>\<open>(ML) code-contexts\<close>\<^index>\<open>code-contexts\<close> and \<^emph>\<open>term-contexts\<close>\<^index>\<open>term-contexts\<close> if we refer
|
||||
to sub-elements inside the \<open>\<open>...\<close>\<close> cartouches of these command families. Note that the Isabelle
|
||||
framework allows for nesting cartouches that permits to support to switch into a different
|
||||
context. In general, this has also the effect that the evaluation of antiquotations changes.
|
||||
\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
|
||||
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
|
||||
\<close>
|
||||
text\<open>
|
||||
On the semantic level, we assume a validation process for an integrated document, where the
|
||||
semantics of a command is a transformation \<open>\<theta> \<rightarrow> \<theta>\<close> for some system state \<open>\<theta>\<close>.
|
||||
This document model can be instantiated with outer-syntax commands for common
|
||||
text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>.
|
||||
Thus, users can add informal text to a sub-document using a text command:
|
||||
This document model can be instantiated depending on the text-code-, or term-contexts.
|
||||
For common text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>,
|
||||
users can add informal text to a sub-document using a text command:
|
||||
@{boxed_theory_text [display] \<open>text\<open>This is a description.\<close>\<close> }
|
||||
This will type-set the corresponding text in, for example, a PDF document. However, this
|
||||
translation is not necessarily one-to-one: text elements can be enriched by formal, \<^ie>,
|
||||
machine-checked content via \<^emph>\<open>semantic macros\<close>, called antiquotations\<^bindex>\<open>antiquotation\<close>:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
|
||||
for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>
|
||||
\<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm "refl"}, we obtain in \<Gamma>
|
||||
for @{term \<open>fac 5\<close>} the result @{value \<open>fac 5\<close>}.\<close>\<close>
|
||||
}
|
||||
which is represented in the final document (\<^eg>, a PDF) by:
|
||||
@{boxed_pdf [display]
|
||||
|
|
@ -137,10 +157,12 @@ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.\<cl
|
|||
typeset. They represent the device for linking the formal with the informal.
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hierarchy''"]
|
||||
\<open>A Theory-Graph in the Document Model. \<close>
|
||||
|
||||
section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model\<close>
|
||||
section*[bgrnd21::introduction]\<open>Implementability of the Document Model in other ITP's\<close>
|
||||
text\<open>
|
||||
Batch-mode checkers for \<^dof> can be implemented in all systems of the LCF-style prover family,
|
||||
\<^ie>, systems with a type-checked \<open>term\<close>, and abstract \<open>thm\<close>-type for theorems
|
||||
|
|
|
|||
|
|
@ -100,7 +100,8 @@ text\<open>
|
|||
to instances, and class-invariants. Some concepts like advanced type-checking, referencing to
|
||||
formal entities of Isabelle, and monitors are due to its specific application in the
|
||||
Isabelle context. Conceptually, ontologies specified in ODL consist of:
|
||||
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) that describe concepts;
|
||||
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) \<^index>\<open>doc\_class\<close> that describe concepts;
|
||||
the keyword (\<^boxed_theory_text>\<open>onto_class\<close>) \<^index>\<open>onto\_class\<close> is accpted equally;
|
||||
\<^item> an optional document base class expressing single inheritance
|
||||
class extensions;
|
||||
\<^item> \<^emph>\<open>attributes\<close> specific to document classes, where
|
||||
|
|
@ -233,7 +234,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
|
|||
\<^item> \<open>doc_class_specification\<close>:\<^index>\<open>doc\_class\_specification@\<open>doc_class_specification\<close>\<close>
|
||||
We call document classes with an \<open>accepts_clause\<close>
|
||||
\<^emph>\<open>monitor classes\<close> or \<^emph>\<open>monitors\<close> for short.
|
||||
\<^rail>\<open> @@{command "doc_class"} class_id '=' (class_id '+')? (attribute_decl+) \<newline>
|
||||
\<^rail>\<open> (@@{command "doc_class"}| @@{command "onto_class"}) class_id '=' (class_id '+')? (attribute_decl+) \<newline>
|
||||
(invariant_decl *)
|
||||
(accepts_clause rejects_clause?)?\<close>
|
||||
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
|
||||
|
|
@ -319,12 +320,17 @@ supported on the Isabelle/Isar level. Note that some more advanced functionality
|
|||
is currently only available in the SML API's of the kernel.
|
||||
|
||||
\<^item> \<open>meta_args\<close> :
|
||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' term) *) \<close>
|
||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
|
||||
\<^item> \<open>upd_meta_args\<close> :
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') term) * ))\<close>
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
|
||||
\<^item> \<open>annotated_text_element\<close> :
|
||||
\<^rail>\<open>
|
||||
( @@{command "text*"}'[' meta_args ']' '\<open>' text '\<close>' |
|
||||
\<^rail>\<open>
|
||||
( ( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
||||
| @@{command "ML*"} '[' meta_args ']' '\<open>' SML_code '\<close>'
|
||||
| @@{command "term*"} '[' meta_args ']' '\<open>' HOL_term '\<close>'
|
||||
| @@{command "value*"}'[' meta_args ']' '\<open>' HOL_term '\<close>'
|
||||
)
|
||||
|
|
||||
( @@{command "open_monitor*"}
|
||||
| @@{command "close_monitor*"}
|
||||
| @@{command "declare_reference*"}
|
||||
|
|
@ -350,10 +356,14 @@ text\<open>Recall that with the exception of \<^theory_text>\<open>text* \<dots>
|
|||
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> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
subsection\<open>Ontologic Text-Contexts and their Management\<close>
|
||||
text\<open> With respect to the family of text elements,
|
||||
\<^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
|
||||
an instance of a document class. The class invariants were checked for all attribute values
|
||||
at creation time if not specified otherwise. Unspecified attributed values were represented
|
||||
by fresh free variables.
|
||||
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
|
||||
can be set by defaults in the class-definitions, or set at creation time, or modified at any
|
||||
point after creation via \<^theory_text>\<open>update_instance*[oid, ...]\<close>. The \<^theory_text>\<open>class_id\<close> is syntactically optional;
|
||||
|
|
@ -374,6 +384,35 @@ The precise presentation is decided in the \<^emph>\<open>layout definitions\<cl
|
|||
pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Code-Contexts and their Management\<close>
|
||||
|
||||
text\<open>The \<^theory_text>\<open>ML*[oid::cid, ...] \<open> \<dots> SML-code \<dots> \<close>\<close>-document elements proceed similarly :
|
||||
a referentiable meta-object of class \<^theory_text>\<open>cid\<close> is created, initialized with the optional
|
||||
attributes and bound to \<^theory_text>\<open>oid\<close>. The SML-code is type-checked and executed
|
||||
in the context of the SML toplevel of the Isabelle system as in the corresponding
|
||||
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Term-Contexts and their Management\<close>
|
||||
text\<open>The major commands providing term-contexts are
|
||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>Note that the meta-argument list is optional.\<close>.
|
||||
Wrt. to creation, track-ability and checking they are analogous to the ontological text and
|
||||
code-commands. However the argument terms may contain term-antiquotations stemming from an
|
||||
ontology definition. Both term-contexts ware type-checked and \<^emph>\<open>validated\<close> against
|
||||
the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers
|
||||
to a meta-object belonging to the document class \<open>A\<close>, for example).
|
||||
The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term
|
||||
denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
|
||||
executable HOL-functions to interact with meta-objects.
|
||||
|
||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||
to choose either to the normalisation-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or to a proof attempt via
|
||||
the \<^theory_text>\<open>auto\<close>. A failure of these strategies will be reported and regarded as non-validation
|
||||
of this meta-object. The latter leads to a failure of the entire command.
|
||||
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
declare_reference*["sec:advanced"::technical]
|
||||
(*>*)
|
||||
|
|
|
|||
|
|
@ -41,8 +41,8 @@
|
|||
\pagestyle{headings}
|
||||
|
||||
\uppertitleback{
|
||||
Copyright \copyright{} 2019--2021 University of Exeter, UK\\
|
||||
\phantom{Copyright \copyright{}} 2018--2021 Universit\'e Paris-Saclay, France\\
|
||||
Copyright \copyright{} 2019--2022 University of Exeter, UK\\
|
||||
\phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\
|
||||
\phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\
|
||||
|
||||
\smallskip
|
||||
|
|
@ -77,11 +77,13 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
|||
|
||||
\lowertitleback{%
|
||||
This manual describes \isadof version \isadofversion. The latest official
|
||||
release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest release. The latest development version as well as official releases are available at
|
||||
release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}).
|
||||
The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest
|
||||
release. The latest development version as well as official releases are available at
|
||||
\url{\dofurl}.
|
||||
|
||||
\paragraph*{Contributors.} We would like to thank the following contributors to \isadof
|
||||
(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, Chantal Keller, and Nicolas M{\'e}ric.
|
||||
(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric.
|
||||
|
||||
\paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay,
|
||||
France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
|
||||
|
|
@ -107,7 +109,7 @@ France, and therefore granted with public funds of the Program ``Investissements
|
|||
\hfill
|
||||
\begin{minipage}{8cm}
|
||||
\raggedleft\normalsize
|
||||
Laboratoire en Recherche en Informatique (LRI)\\
|
||||
Laboratoire des Methodes Formelles (LMF)\\
|
||||
Universit\'e Paris-Saclay\\
|
||||
91405 Orsay Cedex\\
|
||||
France
|
||||
|
|
|
|||
Loading…
Reference in New Issue