From 862d487b9074ca987635a8013c18f2bc8f42dbe6 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 30 Oct 2018 00:27:07 +0000 Subject: [PATCH] Cleanup. --- .../scholarly/document/IsaDofApplications.tex | 928 ------------------ 1 file changed, 928 deletions(-) delete mode 100644 examples/scholarly/document/IsaDofApplications.tex diff --git a/examples/scholarly/document/IsaDofApplications.tex b/examples/scholarly/document/IsaDofApplications.tex deleted file mode 100644 index a4de1431..00000000 --- a/examples/scholarly/document/IsaDofApplications.tex +++ /dev/null @@ -1,928 +0,0 @@ -% This file was modified by the DOF LaTeX converter, version 0.0.3 -% -\begin{isabellebody}% -\setisabellecontext{IsaDofApplications}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -\ \isanewline -% -\endisadelimtheory -% -\isaDofTitle% -% -[label={tit}, type={title}]% -{Using The Isabelle Ontology Framework}% -% -\isaDofSubtitle% -% -[label={stit}, type={subtitle}]% -{Linking the Formal with the Informal}% -% -\isaDofTextAuthor% -% -[label={adb}, type={author}, email={a.brucker{\isacharat}sheffield.ac.uk}, orcid={0000-0002-6355-1200}, - affiliation={University of Sheffield, Sheffield, UK}]% -{Achim D. Brucker}% -% -\isaDofTextAuthor% -% -[label={idir}, type={author}, email={idir.aitsadoune{\isacharat}centralesupelec.fr}, - affiliation = {CentraleSupelec, Paris, France}]% -{Idir Ait-Sadoune}% -% -\isaDofTextAuthor% -% -[label={paolo}, type={author},email={paolo.crisafulli{\isacharat}irt-systemx.fr}, - affiliation = {IRT-SystemX, Paris, France}]% -{Paolo Crisafulli}% -% -\isaDofTextAuthor% -% -[label={bu}, type={author}, email={wolff{\isacharat}lri.fr}, - affiliation={Universit\'e Paris-Sud, Paris, France}]% -{Burkhart Wolff}% -% -\isaDofTextAbstract% -% -[label={abs}, type={abstract}, keywordlist={Ontology,Ontological Modeling,Isabelle/DOF}]% -{ -While Isabelle is mostly known as part of Isabelle/HOL (an interactive -theorem prover), it actually provides a framework for developing a wide -spectrum of applications. A particular strength -of the Isabelle framework is the combination of text editing, formal verification, -and code generation. - -Up to now, Isabelle's document preparation system lacks a mechanism -for ensuring the structure of different document types (as, e.g., -required in certification processes) in general and, in particular, -mechanism for linking informal and formal parts of a document. - -In this paper, we present \isadof, a novel Document Ontology Framework -on top of Isabelle. \isadof allows for conventional typesetting -\emph{as well} as formal development. We show how to model document - ontologies inside \isadof, how to use the resulting meta-information -for enforcing a certain document structure, and discuss ontology-specific IDE support.}% -% -\isaDofSectionIntroduction% -% -[label={intro}, type={introduction}]% -{Introduction}% -% -\isaDofTextIntroduction% -% -[label={introtext}, type={introduction}]% -{ -The linking of the \emph{formal} to the \emph{informal} is perhaps the -most pervasive challenge in the digitization of knowledge and its -propagation. This challenge incites numerous research efforts -summarized under the labels {\isacharbackquote}{\isacharbackquote}semantic web'', {\isacharbackquote}{\isacharbackquote}data mining'', or any -form of advanced {\isacharbackquote}{\isacharbackquote}semantic'' text processing. A key role in -structuring this linking play \emph{document ontologies} (also called -\emph{vocabulary} in the semantic web -community~\cite{w3c:ontologies:2015}), \ie, a machine-readable form of -the structure of documents as well as the document discourse. -Such ontologies can be used for the scientific discourse within scholarly -articles, mathematical libraries, and in the engineering discourse -of standardized software certification documents\cite{boulanger:cenelec-50128:2015,cc:cc-part3:2006}. -Further applications are the domain-specific discourse in juridical texts or medical reports. -In general, an ontology is a formal explicit description of \emph{concepts} -in a domain of discourse (called \emph{classes}), properties of each concept -describing \emph{attributes} of the concept, as well as \emph{links} between -them. A particular link between concepts is the \emph{is-a} relation declaring -the instances of a subclass to be instances of the super-class. - -The main objective of this paper is to present \isadof, a novel -framework to \emph{model} typed ontologies and to \emph{enforce} them during -document evolution. Based on Isabelle infrastructures, ontologies may refer to -types, terms, proven theorems, code, or established assertions. -Based on a novel adaption of the Isabelle IDE, a document is checked to be -\emph{conform} to a particular ontology---\isadof is -designed to give fast user-feedback \emph{during the capture of -content}. This is particularly valuable in case of document changes, -where the \emph{coherence} between the formal and the informal parts of the -content can be mechanically checked. - -To avoid any misunderstanding: \isadof is \emph{not a theory in HOL} -on ontologies and operations to track and trace links in texts, -it is an \emph{environment to write structured text} which \emph{may contain} -Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and -scientific papers---as the present one, which is written in \isadof -itself. \isadof is a plugin into the Isabelle/Isar -framework in the style of~\cite{wenzel.ea:building:2007}.}% -% -\isaDofDeclareReferenceTextSection% -% -[label={bgrnd}, type={text_section}]% -% -% -\isaDofDeclareReferenceTextSection% -% -[label={isadof}, type={text_section}]% -% -% -\isaDofDeclareReferenceTextSection% -% -[label={ontomod}, type={text_section}]% -% -% -\isaDofDeclareReferenceTextSection% -% -[label={ontopide}, type={text_section}]% -% -% -\isaDofDeclareReferenceTextSection% -% -[label={conclusion}, type={text_section}]% -% -\begin{isamarkuptext}% -The plan of the paper is follows: we start by introducing the underlying -Isabelel sytem (\autoref{bgrnd}) followed by presenting the -essentials of \isadof and its ontology language (\autoref{isadof}). -It follows \autoref{ontomod}, where we present three application -scenarios from the point of view of the ontology modeling. In \autoref{ontopide} -we discuss the user-interaction generated from the ontological definitions. Finally, we draw -conclusions and discuss related work in \autoref{conclusion}.% -\end{isamarkuptext}\isamarkuptrue% -% -% -\isaDofSectionTextSection% -% -[label={bgrnd}, type={text_section}, - text_section.main_author={Some({\isacharat}{docitem adb}::author)}]% -{Background: The Isabelle System}% -% -\begin{isamarkuptext}% -While Isabelle is widely perceived as an interactive theorem prover -for HOL (Higher-order Logic)~\cite{nipkow.ea:isabelle:2002}, we -would like to emphasize the view that Isabelle is far more than that: -it is the \emph{Eclipse of Formal Methods Tools}. This refers to the -``\textsl{generic system framework of Isabelle/Isar underlying recent - versions of Isabelle. Among other things, Isar provides an - infrastructure for Isabelle plug-ins, comprising extensible state - components and extensible syntax that can be bound to ML - programs. Thus, the Isabelle/Isar architecture may be understood as - an extension and refinement of the traditional `LCF approach', with - explicit infrastructure for building derivative - \emph{systems}.}''~\cite{wenzel.ea:building:2007} - - The current system framework offers moreover the following features: -\begin{compactitem} -\item a build management grouping components into to pre-compiled sessions, -\item a prover IDE (PIDE) framework~\cite{wenzel:asynchronous:2014} with - various front-ends -\item documentation - and code generators, -\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. -\end{compactitem}% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofFigure% -% -[label={architecture}, type={figure},relative_width={100}, - src={figures/isabelle-architecture}]% -{The system architecture of Isabelle (left-hand side) and the - asynchronous communication between the Isabelle system and - the IDE (right-hand side).}% -% -\begin{isamarkuptext}% -The Isabelle system architecture shown in \autoref{architecture} - comes with many layers, with Standard ML (SML) at the bottom layer as implementation -language. The architecture actually foresees a \emph{Nano-Kernel} (our terminology) which -resides in the SML structure \texttt{Context}. This structure provides a kind of container called -\emph{context} 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 support for higher specification constructs -were built.% -\end{isamarkuptext}\isamarkuptrue% -% -\begin{isamarkuptext}% -We would like to detail the documentation generation of the architecture, -which is based on literate specification commands such as \inlineisar+section+ \ldots, -\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc. -Thus, a user can add a simple text: -\begin{isar} - text\This is a description.\ -\end{isar} -These text-commands can be arbitrarily mixed with other commands stating definitions, proofs, code, etc., -and will result in the corresponding output in generated \LaTeX{} or HTML documents. -Now, \emph{inside} the textual content, it is possible to embed a \emph{text-antiquotation}: -\begin{isar} - text\According to the reflexivity axiom @{thm refl}, we obtain in \ - for @{term "fac 5"} the result @{value "fac 5"}.\ -\end{isar} -which is represented in the generated output by: -\begin{out} - According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ - the result $120$. -\end{out} -where \inlineisar+refl+ is actually the reference to the axiom of reflexivity in HOL. -For the antiquotation \inlineisar+@{value "fac 5"}+ we assume the usual definition for -\inlineisar+fac+ in HOL.% -\end{isamarkuptext}\isamarkuptrue% -% -\begin{isamarkuptext}% -Thus, antiquotations can refer to formal content, can be type-checked before being -displayed and can be used for calculations before actually being typeset. When editing, -Isabelle's PIDE offers auto-completion and error-messages while typing the above -\emph{semi-formal} content.% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofSectionTextSection% -% -[label={isadof}, type={text_section}, - text_section.main_author={Some({\isacharat}{docitem adb}::author)}]% -{\isadof}% -% -\begin{isamarkuptext}% -An \isadof document consists of three components: -\begin{compactitem} -\item the \emph{ontology definition} (which is an Isabelle theory file with definitions - for document-classes and all auxiliary datatypes. -\item the \emph{core} of the document itself which is an Isabelle theory - importing the ontology definition. \isadof provides an own family of text-element - commands such as \inlineisar+title*+, \inlineisar+section*+, \inlineisar+text*+, etc., - which can be annotated with meta-information defined in the underlying ontology definition. -\item the \emph{layout definition} for the given ontology exploiting this meta-information. -\end{compactitem} -\isadof is a novel Isabelle system component providing specific support for all these three parts. -Note that the document core \emph{may}, but \emph{must} not -use Isabelle definitions or proofs for checking the formal content---the -present paper is actually an example of a document not containing any proof. - - The document generation process of \isadof is currently restricted to \LaTeX, which means -that the layout is defined by a set of \LaTeX{} style files. Several layout -definitions for one ontology are possible and pave the way that different \emph{views} for -the same central document were generated, addressing the needs of different purposes and/or target -readers. - - While the ontology and the layout definition will have to be developed by an expert -with knowledge over Isabelle and \isadof and the back end technology depending on the layout -definition, the core is intended to require only minimal knowledge of these two. Document core -authors \emph{can} use \LaTeX{} commands in their source, but this limits the possibility -of using different representation technologies, \eg, HTML, and increases the risk of arcane -error-messages in generated \LaTeX{}. - - 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, 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 -as enumerations. In particular, document class definitions provide: -\begin{compactitem} -\item a HOL-type for each document class as well as inheritance, -\item support for attributes with HOL-types and optional default values, -\item support for overriding of attribute defaults but not overloading, and -\item text-elements annotated with document classes; they are mutable - instances of document classes. -\end{compactitem} -Attributes referring to other ontological concepts are called \emph{links}. -The HOL-types inside the document specification language support built-in types for Isabelle/HOL \inlineisar+typ+'s, -\inlineisar+term+'s, and \inlineisar+thm+'s reflecting internal Isabelle's internal types -for these entities; when denoted in HOL-terms to instantiate an attribute, for example, there is a -specific syntax (called \emph{inner syntax antiquotations}) that is checked by \isadof -for consistency. - -Document classes can have a \inlineisar+where+ clause containing a regular -expression over class names. Classes with such a \inlineisar+where+ were called \emph{monitor classes}. -While document classes and their inheritance relation structure meta-data of text-elements -in an object-oriented manner, monitor classes enforce structural organization -of documents via the language specified by the regular expression -enforcing a sequence of text-elements that must belong to the corresponding classes. - -To start using \isadof, one creates an Isabelle project (with the name -\inlinebash{IsaDofApplications}): -\begin{bash} - isabelle DOF_mkroot -o scholarly_paper -t lncs -d IsaDofApplications -\end{bash} -where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and -\inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in Computer Science series. The project -can be formally checked, including the generation of the article in PDF using the -following command: -\begin{bash} - isabelle build -d . IsaDofApplications -\end{bash}% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofSectionTechnical% -% -[label={ontomod}, type={technical}]% -{Modeling Ontologies in \isadof}% -% -\begin{isamarkuptext}% -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.% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofSubsectionExample% -% -[label={scholar_onto}, type={example}]% -{The Scholar Paper Scenario: Eating One's Own Dog Food.}% -% -\begin{isamarkuptext}% -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.% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofFigure% -% -[label={fig1}, type={figure}, spawn_columns=False,relative_width={95}, - src={figures/Dogfood-Intro}]% -{Ouroboros I: This paper from inside \ldots}% -% -\begin{isamarkuptext}% -\autoref{fig1} shows the corresponding view in the Isabelle/PIDE of the 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 ~~ \subtitle\ ~~ \author\$^+$+ ~~ abstract ~~ - introduction ~~ \technical || example\$^+$ ~~ conclusion ~~ - bibliography)" -\end{isar} -\caption{A monitor for the scholarly paper ontology.} -\label{fig:paper-onto-monitor} -\end{figure}% -\end{isamarkuptext}\isamarkuptrue% -% -\begin{isamarkuptext}% -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 :: "string" (* percent of textwidth *) - src :: "string" - placement :: placement - spawn_columns :: bool <= True -\end{isar}% -\end{isamarkuptext}\isamarkuptrue% -% -\begin{isamarkuptext}% -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.% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofFigure% -% -[label={fig_figures}, type={figure}, spawn_columns=False,relative_width={85}, - src={figures/Dogfood-figures}]% -{Ouroboros II: figures \ldots}% -% -\begin{isamarkuptext}% -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 \autoref{fig_figures}.% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofSubsectionExample% -% -[label={mathex_onto}, type={example}]% -{The Math-Exam Scenario}% -% -\begin{isamarkuptext}% -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{baccaleaureat} and exams at The University of Sheffield. - -We assume that the content has four different types of addressees, which have a different -\emph{view} on the integrated document -\begin{compactitem} -\item the \emph{setter}, \ie, the author of the exam, -\item the \emph{checker}, \ie, an internal person that checks the exam for feasibility -and non-ambiguity, -\item the \emph{external examiner}, \ie, an external person that checks the exam for -feasibility and non-ambiguity, and -\item the \emph{student}, \ie, the addressee of the exam. -\end{compactitem} -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 -- \isa{for\ checkboxes} - -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 \isa{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{intern}, \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 "\Author\$^+$ ~~ Header ~~ \Exercise ~~ Solution\$^+$ " -\end{isar} -\caption{Validating exams.} -\label{fig:onto-exam-monitor} -\end{figure}% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofDeclareReferenceFigure% -% -[label={{fig_qcm}}, type={figure}]% -% -\begin{isamarkuptext}% -Using the \LaTeX{} package hyperref, it is possible to conceive an interactive -exam-sheets with multiple-choice and/or free-response elements -(see \autoref{fig_qcm}). 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.% -\end{isamarkuptext}\isamarkuptrue% -% -% -\isaDofFigure% -% -[label={fig_qcm}, type={figure}, spawn_columns=False,relative_width={90}, - src={figures/InteractiveMathSheet}]% -{A Generated QCM Fragment \ldots}% -% -\isaDofSubsectionExample% -% -[label={cenelec_onto}, type={example}]% -{The Certification Scenario following CENELEC}% -% -\begin{isamarkuptext}% -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.% -\end{isamarkuptext}\isamarkuptrue% -% -\begin{isamarkuptext}% -In the sequel, we present a simplified version of an ontological model used in a -case-study~\cite{bezzecchi.ea:making:2018}. We start with an introduction of the concept of requirement -(see \autoref{fig:conceptual}). -\begin{figure} -\begin{isar} -doc_class requirement = long_name :: "string option" - -doc_class requirement_analysis = no :: "nat" - where "requirement_item +" - -doc_class hypothesis = requirement + - hyp_type :: hyp_type <= physical (* default *) - -datatype ass_kind = informal | semiformal | formal - -doc_class assumption = requirement + - assumption_kind :: ass_kind <= informal -\end{isar} -\caption{Modeling requirements.} -\label{fig:conceptual} -\end{figure} -Such ontologies can be enriched by larger explanations and examples, which may help -the team of engineers substantially when developing the central document for a certification, -like an explication what is precisely the difference between an \emph{hypothesis} and an -\emph{assumption} in the context of the evaluation standard. Since the PIDE makes for each -document class its definition available by a simple mouse-click, this kind on meta-knowledge -can be made far more accessible during the document evolution. - -For example, the term of category \emph{assumption} is used for domain-specific assumptions. -It has formal, semi-formal and informal sub-categories. They have to be -tracked and discharged by appropriate validation procedures within a -certification process, by it by test or proof. It is different from a hypothesis, which is -globally assumed and accepted. - - In the sequel, the category \emph{exported constraint} (or \emph{ec} for short) -is used for formal assumptions, that arise during the analysis, -design or implementation and have to be tracked till the final -evaluation target, and discharged by appropriate validation procedures -within the certification process, by it by test or proof. A particular class of interest -is the category \emph{safety related application condition} (or \emph{srac} -for short) which is used for \emph{ec}'s that establish safety properties -of the evaluation target. Their track-ability throughout the certification -is therefore particularly critical. This is naturally modeled as follows: -\begin{isar} -doc_class ec = assumption + - assumption_kind :: ass_kind <= (*default *) formal - -doc_class srac = ec + - assumption_kind :: ass_kind <= (*default *) formal -\end{isar}% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofSectionTechnical% -% -[label={ontopide}, type={technical}]% -{Ontology-based IDE support}% -% -\begin{isamarkuptext}% -We present a selection of interaction scenarios \autoref{scholar_onto} -and \autoref{cenelec_onto} with Isabelle/PIDE instrumented by \isadof.% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofSubsectionExample% -% -[label={scholar_pide}, type={example}]% -{A Scholarly Paper}% -% -\begin{isamarkuptext}% -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}).% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofSideBySideFigure% -% -[label={{text-elements}}, type={side_by_side_figure},anchor={fig-Dogfood-II-bgnd1} - ,caption={Exploring a Reference of a Text-Element.} - ,relative_width={48} - ,src={figures/Dogfood-II-bgnd1} - ,anchor2={fig-bgnd-text_section} - ,caption2={Exploring the class of a text element.} - ,relative_width2={47} - ,src2={figures/Dogfood-III-bgnd-text_section} -]% -{Exploring text elements.}% -% -\isaDofSideBySideFigure% -% -[label={{hyperlinks}}, type={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} -]% -{Hyperlinks.}% -% -\isaDofDeclareReferenceFigure% -% -[label={{figDogfoodVIlinkappl}}, type={figure}]% -% -\begin{isamarkuptext}% -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.% -\end{isamarkuptext}\isamarkuptrue% -% -% -\isaDofFigure% -% -[label={figDogfoodVIlinkappl}, type={figure},relative_width={80}, - src={figures/Dogfood-V-attribute}]% -{Exploring an attribute (hyperlinked to the class).}% -% -\isaDofSubsectionExample% -% -[label={cenelec_pide}, type={example}]% -{CENELEC}% -% -\isaDofDeclareReferenceFigure% -% -[label={figfig3}, type={figure}]% -% -\begin{isamarkuptext}% -The corresponding view in \autoref{figfig3} shows core part of a document, -coherent to the \autoref{cenelec_onto}. 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.% -\end{isamarkuptext}\isamarkuptrue% -% -% -\isaDofFigure% -% -[label={figfig3}, type={figure},relative_width={80}, - src={figures/antiquotations-PIDE}]% -{Standard antiquotations referring to theory elements.}% -% -\isaDofDeclareReferenceFigure% -% -[label={figfig5}, type={figure}]% -% -\begin{isamarkuptext}% -The subsequent sample in \autoref{figfig5} shows the definition of an -\emph{safety-related application condition}, 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.% -\end{isamarkuptext}\isamarkuptrue% -% -% -\isaDofFigure% -% -[label={figfig5}, type={figure},relative_width={80}, - src={figures/srac-definition}]% -{Defining a SRAC reference \ldots}% -% -\isaDofFigure% -% -[label={figfig7}, type={figure},relative_width={80}, - src={figures/srac-as-es-application}]% -{Using a SRAC as EC document reference.}% -% -\begin{isamarkuptext}% -Now we reference in \autoref{figfig7} this safety-related condition; -however, this happens in a context where general \emph{exported constraints} 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.% -\end{isamarkuptext}\isamarkuptrue% -% -\isaDofSectionConclusion% -% -[label={conclusion}, type={conclusion}]% -{Conclusion and Related Work}% -% -\begin{isamarkuptext}% -We have demonstrated the use of \isadof, a novel ontology modeling and enforcement -IDE deeply integrated into the Isabelle/Isar Framework. The two most distinguishing features are -\begin{compactitem} -\item \isadof and its ontology language are a strongly typed language that allows - for referring (albeit not reasoning) to entities of Isabelle/HOL, most notably types, terms, - and (formally proven) theorems, and -\item \isadof is supported by the Isabelle/PIDE framework; thus, the advantages of an IDE for - text-exploration (which is the type of this link? To which text element does this link refer? - Which are the syntactic alternatives here?) were available during editing - instead of a post-hoc validation process. -\end{compactitem}% -\end{isamarkuptext}\isamarkuptrue% -% -\begin{isamarkuptext}% -Of course, a conventional batch-process also exists which can be used -for the validation of large document bases in a conventional continuous build process. -This combination of formal and semi-informal elements, as well as a systematic enforcement -of the coherence to a document ontology of the latter, is, as we believe, novel and offers -a unique potential for the semantic treatment of scientific texts and technical documentations.% -\end{isamarkuptext}\isamarkuptrue% -% -\begin{isamarkuptext}% -To our knowledge, this is the first ontology-driven framework for -editing mathematical and technical documents that focuses particularly -on documents mixing formal and informal content---a type of documents -that is very common in technical certification processes. We see -mainly one area of related works: IDEs and text editors that support -editing and checking of documents based on an ontology. There is a -large group of ontology editors (\eg, Prot{\'e}g{\'e}~\cite{protege}, -Fluent Editor~\cite{cognitum}, NeOn~\cite{neon}, or -OWLGrEd~\cite{owlgred}). With them, we share the support for defining -ontologies as well as auto-completion when editing documents based on -an ontology. While our ontology definitions are currently based on a -textual definition, widely used ontology editors (\eg, -OWLGrEd~\cite{owlgred}) also support graphical notations. This could -be added to \isadof in the future. A unique feature of \isadof is the -deep integration of formal and informal text parts. The only other -work in this area wea are aware of is rOntorium~\cite{rontorium}, a plugin -for Prot{\'e}g{\'e} that integrates R~\cite{adler:r:2010} into an -ontology environment. Here, the main motivation behind this -integration is to allow for statistically analyze ontological -documents. Thus, this is complementary to our work.% -\end{isamarkuptext}\isamarkuptrue% -% -\begin{isamarkuptext}% -\isadof in its present form has a number of technical short-comings as well - as potentials not yet explored. On the long list of the short-comings is the - fact that strings inside HOL-terms do not support, for example, Unicode. - For the moment, \isadof is conceived as an - add-on for Isabelle/HOL; a much deeper integration of \isadof into Isabelle - could increase both performance and uniformity. Finally, different target - presentation (such as HTML) would be highly desirable in particular for the - math exam scenarios. And last but not least, it would be desirable that PIDE - itself is ``ontology-aware'' and can, for example, use meta-information - to control read- and write accesses of \emph{parts} of documents.% -\end{isamarkuptext}\isamarkuptrue% -% -\isamarkupparagraph{Availability.% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -The implementation of the framework, the discussed ontology definitions, - and examples are available at - \url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.% -\end{isamarkuptext}\isamarkuptrue% -% -\isamarkupparagraph{Acknowledgement.% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -This work was partly supported by the framework of IRT SystemX, Paris-Saclay, France, -and therefore granted with public funds within the scope of the -Program ``Investissements d’Avenir''.% -\end{isamarkuptext}\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: \ No newline at end of file