From 688e823463a8321dbe2344f2b6ce95600cfe2310 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Tue, 11 Jan 2022 18:31:56 +0100 Subject: [PATCH] Make 2021-ITP-PMTI paper compile --- examples/scholarly_paper/2021-ITP-PMTI/ROOT | 1 + .../2021-ITP-PMTI/document/lstisadof.sty | 163 ++++++++++++++++ .../2021-ITP-PMTI/document/preamble.tex | 14 +- .../2021-ITP-PMTI/document/root.bib | 180 +++++++++++++++--- .../scholarly_paper/2021-ITP-PMTI/paper.thy | 10 +- 5 files changed, 332 insertions(+), 36 deletions(-) create mode 100755 examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof.sty diff --git a/examples/scholarly_paper/2021-ITP-PMTI/ROOT b/examples/scholarly_paper/2021-ITP-PMTI/ROOT index bb05c5c9..ebac2b74 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/ROOT +++ b/examples/scholarly_paper/2021-ITP-PMTI/ROOT @@ -15,3 +15,4 @@ session "2021-ITP-PMTI" = "Isabelle_DOF" + "figures/three-phase-odo.pdf" "figures/df-numerics-encshaft.png" "figures/wheel-df.png" + "lstisadof.sty" diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof.sty b/examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof.sty new file mode 100755 index 00000000..3bbe86a4 --- /dev/null +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof.sty @@ -0,0 +1,163 @@ +%% Copyright (C) 2018 The University of Sheffield +%% 2018 The University of Paris-Saclay +%% 2019 The University of Exeter +%% +%% License: +%% This program can be redistributed and/or modified under the terms +%% of the LaTeX Project Public License Distributed from CTAN +%% archives in directory macros/latex/base/lppl.txt; either +%% version 1.3c of the License, or (at your option) any later version. +%% OR +%% The 2-clause BSD-style license. +%% +%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause + +\definecolor{OliveGreen} {cmyk}{0.64,0,0.95,0.40} +\definecolor{BrickRed} {cmyk}{0,0.89,0.94,0.28} +\definecolor{Blue} {cmyk}{1,1,0,0} +\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0} + +%%%\lst@BeginAspect[keywords]{isar} +\gdef\lst@tagtypes{s} +\gdef\lst@TagKey#1#2{% + \lst@Delim\lst@tagstyle #2\relax + {Tag}\lst@tagtypes #1% + {\lst@BeginTag\lst@EndTag}% + \@@end\@empty{}} +\lst@Key{tag}\relax{\lst@TagKey\@empty{#1}} +\lst@Key{tagstyle}{}{\def\lst@tagstyle{#1}} +\lst@AddToHook{EmptyStyle}{\let\lst@tagstyle\@empty} +\gdef\lst@BeginTag{% + \lst@DelimOpen + \lst@ifextags\else + {\let\lst@ifkeywords\iftrue + \lst@ifmarkfirstintag \lst@firstintagtrue \fi}} +\lst@AddToHookExe{ExcludeDelims}{\let\lst@ifextags\iffalse} +\gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else} +\lst@Key{usekeywordsintag}t[t]{\lstKV@SetIf{#1}\lst@ifusekeysintag} +\lst@Key{markfirstintag}f[t]{\lstKV@SetIf{#1}\lst@ifmarkfirstintag} +\gdef\lst@firstintagtrue{\global\let\lst@iffirstintag\iftrue} +\global\let\lst@iffirstintag\iffalse + \lst@AddToHook{PostOutput}{\lst@tagresetfirst} + \lst@AddToHook{Output} + {\gdef\lst@tagresetfirst{\global\let\lst@iffirstintag\iffalse}} + \lst@AddToHook{OutputOther}{\gdef\lst@tagresetfirst{}} +\lst@AddToHook{Output} + {\ifnum\lst@mode=\lst@tagmode + \lst@iffirstintag \let\lst@thestyle\lst@gkeywords@sty \fi + \lst@ifusekeysintag\else \let\lst@thestyle\lst@gkeywords@sty\fi + \fi} +\lst@NewMode\lst@tagmode +\gdef\lst@Tag@s#1#2\@empty#3#4#5{% + \lst@CArg #1\relax\lst@DefDelimB {}{}% + {\ifnum\lst@mode=\lst@tagmode \expandafter\@gobblethree \fi}% + #3\lst@tagmode{#5}% + \lst@CArg #2\relax\lst@DefDelimE {}{}{}#4\lst@tagmode}% +\gdef\lst@BeginCDATA#1\@empty{% + \lst@TrackNewLines \lst@PrintToken + \lst@EnterMode\lst@GPmode{}\let\lst@ifmode\iffalse + \lst@mode\lst@tagmode #1\lst@mode\lst@GPmode\relax\lst@modetrue} +%%\lst@EndAspect + + + +% \gdef\lst@BeginTag{% +% \lst@DelimOpen +% \lst@ifextags\else +% {\let\lst@ifkeywords\iftrue +% \lst@ifmarkfirstintag\lst@firstintagtrue\fi\color{green}}} +% \gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else\color{green}} + +\def\beginlstdelim#1#2#3% +{% + \def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}% + \ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim% +} +\newcommand{\subscr}[1]{\ensuremath{_{\mbox{#1}}}} +\newcommand{\supscr}[1]{\ensuremath{^{\mbox{#1}}}} +\lstdefinestyle{ISAR}{% + language=% + ,basicstyle=\ttfamily% + ,showspaces=false% + ,showlines=false% + ,columns=flexible% + ,morecomment=[s]{(*}{*)}% + % ,moredelim=*[s][\rmfamily]{\{*}{*\}}% + ,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}} + ,showstringspaces=false% + ,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}% + ,literate={% + {...}{\,\ldots\,}3% + {\\}{\ensuremath{\isacartoucheopen}}1% + {\\at}{@}1% + {\\}{\ensuremath{\isacartoucheclose}}1% + {\\}{\ensuremath{\Gamma}}1% + {\\}{\ensuremath{\times}}1% + {\\}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}1% + {\\}{\ensuremath{\mathclose{\mid\mkern-4.5mu\rbrace}}}1% + {\\}{\ensuremath{\mathopen{\lbrack\mkern-3mu\lbrack}}}1% + {\\}{\ensuremath{\mathopen{\lbrace\mkern-4.5mu\mid}}}1% + {\\}{\ensuremath{\Rightarrow}}1% + {\{*}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1% + {*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1% + }% + % % Defining "tags" (text-antiquotations) based on 1-keywords + ,tag=**[s]{@\{}{\}}% + ,tagstyle=\color{CornflowerBlue}% + ,markfirstintag=true% + ,keywordstyle=\bfseries% + ,keywords={} + % Defining 2-keywords + ,keywordstyle=[2]{\color{Blue!60}\bfseries}% + ,alsoletter={*,-} + ,morekeywords=[2]{theory, begin, end, ML,section,subsection,paragraph,chapter,text}% + %,moredelim=[s][\textit]{<}{>} + % Defining 3-keywords + ,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}% + ,morekeywords=[3]{doc_class,declare_reference,update_instance*, + open_monitor*, close_monitor*, figure*, title*, subtitle*,declare_reference*,section*,text*}% + % Defining 4-keywords + ,keywordstyle=[4]{\color{black!60}\bfseries}% + ,morekeywords=[4]{where, imports}% + % Defining 5-keywords + ,keywordstyle=[5]{\color{BrickRed!70}\bfseries}% + ,morekeywords=[5]{datatype, typedecl, consts, theorem}% + % Defining 6-keywords + ,keywordstyle=[6]{\itshape}% + ,morekeywords=[6]{meta-args, ref, expr, class_id}% + % +}% +%% +\lstnewenvironment{isar}[1][]{\lstset{style=ISAR, + backgroundcolor=\color{black!2}, + frame=lines, + mathescape=true, + basicstyle=\footnotesize\ttfamily,#1}}{} +%%% +\def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]} + +\lstnewenvironment{out}[1][]{\lstset{ + backgroundcolor=\color{green!2}, + frame=lines,mathescape,breakatwhitespace=true + ,columns=flexible% + ,basicstyle=\footnotesize\rmfamily,#1}}{} + + +%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%% +\lstloadlanguages{ML} +\lstdefinestyle{sml}{basicstyle=\ttfamily,% + commentstyle=\itshape,% + keywordstyle=\bfseries\color{CornflowerBlue},% + ndkeywordstyle=\color{red},% + language=ML, + ,keywordstyle=[6]{\itshape}% + ,morekeywords=[6]{args_type}% + }% + +\lstnewenvironment{sml}[1][]{\lstset{style=sml, + backgroundcolor=\color{Blue!4}, + frame=lines, + basicstyle=\footnotesize\ttfamily,#1}}{} +%%% +\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]} diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex b/examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex index 0a30851f..eb5cf25c 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex @@ -1,10 +1,16 @@ -%% This is a placeholder for user-specific configuration and packages. +%% This is a placeholder for user-specific configuration and packages. \usepackage{stmaryrd} +\IfFileExists{beramono.sty}{\usepackage[scaled=0.88]{beramono}}{}% +\IfFileExists{upquote.sty}{\usepackage{upquote}}{}% +\usepackage{textcomp} +\usepackage{xcolor} +\usepackage{paralist} +\usepackage{listings} +\usepackage{lstisadof} +\usepackage{xspace} -\newcommand{\acs}[1]{} +\newcommand{\fixIsarList}{\vspace{-\topsep}\vspace{-\baselineskip}\mbox{}\\[0pt]\noindent} \title{} \author{<AUTHOR>} - - diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib index f9e86ab1..92fb2fda 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib @@ -13,6 +13,132 @@ @STRING{j-tosem= "" } @STRING{pub-acm:adr= "" } +@TechReport{ bsi:50128:2014, + type = {Standard}, + key = {BS EN 50128:2011}, + month = apr, + year = 2014, + series = {British Standards Publication}, + title = {BS EN 50128:2011: Railway applications -- Communication, + signalling and processing systems -- Software for railway + control and protecting systems}, + institution = {Britisch Standards Institute (BSI)}, + keywords = {CENELEC}, + abstract = {This European Standard is part of a group of related + standards. The others are EN 50126-1:1999 "Railway + applications -- The specification and demonstration of + Reliability, Availability, Maintainability and Safety + (RAMS) -- Part 1: Basic requirements and generic process -- + and EN 50129:2003 "Railway applications -- Communication, + signalling and processing systems -- Safety related + electronic systems for signalling". EN 50126-1 addresses + system issues on the widest scale, while EN 50129 addresses + the approval process for individual systems which can exist + within the overall railway control and protection system. + This European Standard concentrates on the methods which + need to be used in order to provide software which meets + the demands for safety integrity which are placed upon it + by these wider considerations. This European Standard + provides a set of requirements with which the development, + deployment and maintenance of any safety-related software + intended for railway control and protection applications + shall comply. It defines requirements concerning + organisational structure, the relationship between + organisations and division of responsibility involved in + the development, deployment and maintenanceactivities.} +} + +@InCollection{ brucker.ea:isabelledof:2019, + abstract = {DOF is a novel framework for defining ontologies and + enforcing them during document development and evolution. A + major goal of DOF is the integrated development of formal + certification documents (e. g., for Common Criteria or + CENELEC 50128) that require consistency across both formal + and informal arguments. + + To support a consistent development of formal and informal + parts of a document, we provide Isabelle/DOF, an + implementation of DOF on top of the formal methods + framework Isabelle/HOL. A particular emphasis is put on a + deep integration into Isabelle{\^a}s IDE, which allows for + smooth ontology development as well as immediate + ontological feedback during the editing of a document. + + In this paper, we give an in-depth presentation of the + design concepts of DOF's Ontology Definition Language + (ODL) and key aspects of the technology of its + implementation. Isabelle/DOF is the first ontology language + supporting machine-checked links between the formal and + informal parts in an LCF-style interactive theorem proving + environment. Sufficiently annotated, large documents can + easily be developed collabo- ratively, while ensuring their + consistency, and the impact of changes (in the formal and + the semi-formal content) is tracked automatically.}, + keywords = {Ontology, Formal Document Development, CERtification, DOF, + Isabelle/DOF}, + location = {Oslo}, + author = {Achim D. Brucker and Burkhart Wolff}, + booktitle = {Software Engineering and Formal Methods (SEFM)}, + language = {USenglish}, + url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019}, + publisher = {Springer-Verlag}, + address = {Heidelberg}, + series = {Lecture Notes in Computer Science}, + number = {11724}, + isbn = {3-540-25109-X}, + doi = {10.1007/978-3-030-30446-1_15}, + editor = {Peter C. {\"O}lveczky and Gwen Sala{\"u}n}, + pdf = {https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf}, + title = {{Isabelle/DOF}: Design and Implementation}, + classification= {conference}, + areas = {formal methods, software}, + categories = {isadof}, + year = {2019}, + public = {yes} +} + +@InCollection{ brucker.ea:isabelle-ontologies:2018, + abstract = {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 Isabelle/DOF, a novel Document + Ontology Framework on top of Isabelle. Isabelle/DOF allows + for conventional typesetting \emph{as well} as formal + development. We show how to model document ontologies + inside Isabelle/DOF, how to use the resulting + meta-information for enforcing a certain document + structure, and discuss ontology-specific IDE support.}, + keywords = {Isabelle/Isar, HOL, Ontologies}, + location = {Hagenberg, Austria}, + author = {Achim D. Brucker and Idir Ait-Sadoune and Paolo Crisafulli + and Burkhart Wolff}, + booktitle = {Conference on Intelligent Computer Mathematics (CICM)}, + language = {USenglish}, + publisher = {Springer-Verlag}, + address = {Heidelberg}, + series = {Lecture Notes in Computer Science}, + number = {11006}, + url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018}, + title = {Using the {Isabelle} Ontology Framework: Linking the + Formal with the Informal}, + classification= {conference}, + areas = {formal methods, software}, + categories = {isadof}, + public = {yes}, + year = {2018}, + doi = {10.1007/978-3-319-96812-4_3}, + pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf} +} % $Id: fmde.bib 6539 2010-01-29 10:33:20Z brucker $ @@ -4424,34 +4550,34 @@ isbn="978-3-540-48509-4" maiden name is Diana Senn.} } -@InCollection{ wenzel.ea:building:2007, - abstract = {We present the generic system framework of - Isabelle/Isarunderlying 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 tactical 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 systems. To demonstrate the technical - potential of the framework, we apply it to a concrete - formalmethods tool: the HOL-Z 3.0 environment, which is - geared towards the analysis of Z specifications and formal - proof of forward-refinements.}, - author = {Makarius Wenzel and Burkhart Wolff}, - booktitle = {\acs{tphols} 2007}, - editor = {Klaus Schneider and Jens Brandt}, - language = {USenglish}, +@InCollection{ wenzel.ea:building:2007, + abstract = {We present the generic system framework of + Isabelle/Isarunderlying 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 tactical 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 systems. To demonstrate the technical + potential of the framework, we apply it to a concrete + formalmethods tool: the HOL-Z 3.0 environment, which is + geared towards the analysis of Z specifications and formal + proof of forward-refinements.}, + author = {Makarius Wenzel and Burkhart Wolff}, + booktitle = {TPHOLs 2007}, + editor = {Klaus Schneider and Jens Brandt}, + language = {USenglish}, acknowledgement={none}, - pages = {352--367}, - publisher = pub-springer, - address = pub-springer:adr, - number = 4732, - series = s-lncs, - title = {Building Formal Method Tools in the {Isabelle}/{Isar} - Framework}, - doi = {10.1007/978-3-540-74591-4_26}, - year = 2007 + pages = {352--367}, + publisher = pub-springer, + address = pub-springer:adr, + number = 4732, + series = s-lncs, + title = {Building Formal Method Tools in the {Isabelle}/{Isar} + Framework}, + doi = {10.1007/978-3-540-74591-4_26}, + year = 2007 } @Article{ igarashi.ea:featherweight:2001, diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index c328e4a2..0624dd1b 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -29,7 +29,7 @@ author*[bu,email="\<open>wolff@lri.fr\<close>",affiliation = "\<open>LRI, Univer abstract*[abs, keywordlist="[\<open>Ontologies\<close>,\<open>Formal Documents\<close>,\<open>Formal Development\<close>,\<open>Isabelle/HOL\<close>,\<open>Ontology Alignment\<close>,\<open>OWL\<close>,\<open>UML/OCL\<close>]"] \<open> \<^dof> is a novel ontology framework on top of Isabelle - @{cite "10.1007/978-3-030-30446-1_15" and "10.1007/978-3-319-96812-4_3"}. + @{cite "brucker.ea:isabelledof:2019" and "brucker.ea:isabelle-ontologies:2018"}. \<^dof> allows for the formal development of ontologies as well as continuous checking that a formal document under development conforms to an underlying ontology. Such a document may contain text and code elements as well as formal Isabelle definitions and proofs. @@ -43,6 +43,7 @@ abstract*[abs, keywordlist="[\<open>Ontologies\<close>,\<open>Formal Documents\< content \<^bold>\<open>as well as\<close> formal proofs that establish relations between different ontologies in general and specific ontology instances in concrete cases. This concept is also called \<^emph>\<open>ontology alignment\<close> in the literature raised a substantial interest recently. + % Verify papers ontology alignment \<close> section*[introheader::introduction,main_author="Some(@{author ''bu''})"] @@ -96,7 +97,7 @@ in the code-elements of Isabelle's SML implementation, or were specifically supp C-program contexts in Isabelle/C @{cite "Tuong-IsabelleC:2019"}. However, programming antiquotations on the intern Isabelle API's is nothing for the -faint-hearted. Recently, \<^dof> @{cite "10.1007/978-3-030-30446-1_15" and "10.1007/978-3-319-96812-4_3"} +faint-hearted. Recently, \<^dof> @{cite "brucker.ea:isabelledof:2019" and "brucker.ea:isabelle-ontologies:2018"} has been designed as an Isabelle component that \<^emph>\<open>generates\<close> antiquotation languages from a more abstract description, namely an \<^emph>\<open>ontology\<close> that provides typed meta-data and typed reference mechanisms inside text- and ML-contexts. @@ -148,8 +149,7 @@ text\<open> subsection*[bgrnd_isadof::text_section]\<open>The \<^dof> Framework\<close> text\<open> \<^dof> ~@{cite "brucker.ea:isabelle-ontologies:2018" and - "brucker.ea:isabelledof:2019" and - "brucker.ea:isabelledof-sw"} + "brucker.ea:isabelledof:2019"} is a document ontology framework that extends Isabelle/HOL. We understand by a \<^emph>\<open>document ontology\<close> structured meta-data attached to an integrated document allowing classifying text-elements, connect them to typed meta-data, and establishing typed links between text- @@ -215,7 +215,7 @@ text\<open> ontology definition. Isabelle's session management allows for pre-compiling them before being imported in the actual target documentation required to be compliant to this ontology. -\vspace{-0.7cm}\<close> +%\vspace{-0.7cm}\<close> side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Req-Def-ex''", caption="''A Text-Element as Requirement.''",relative_width="48",