From c92376871c7b922c5ea22f691a22c9101d7df4e7 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 17 Aug 2019 09:46:17 +0100 Subject: [PATCH 1/2] Fixes spacing. --- .../Isabelle_DOF-Manual/document/root.bib | 88 +++++++++---------- 1 file changed, 40 insertions(+), 48 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib index eb82838..68d9787 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib +++ b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib @@ -3,7 +3,7 @@ @STRING{s-lncs = "LNCS" } @Misc{ w3c:ontologies:2015, - author = {W3C}, + author = {W3C}, title = {Ontologies}, organisation = {W3c}, url = {https://www.w3.org/standards/semanticweb/ontology}, @@ -11,25 +11,19 @@ } @Misc{ doors, - author = {IBM}, + author = {IBM}, title = {{IBM} Engineering Requirements Management {DOORS} Family}, note = {\url{https://www.ibm.com/us-en/marketplace/requirements-management}}, year = 2019 } -@Manual{ wenzel:isabelle-isar:2019, - title = {The Isabelle/Isar Reference Manual}, - author = {Makarius Wenzel}, - OPTorganization = {}, - OPTaddress = {}, - OPTedition = {}, - OPTmonth = {}, - year = {2019}, - note = {Part of the Isabelle distribution.}, - OPTannote = {} +@Manual{ wenzel:isabelle-isar:2019, + title = {The Isabelle/Isar Reference Manual}, + author = {Makarius Wenzel}, + year = 2019, + note = {Part of the Isabelle distribution.} } - @InCollection{ brucker.ea:isabelledof:2019, abstract = {DOF is a novel framework for defining ontologies and enforcing them during document development and evolution. A @@ -124,7 +118,7 @@ title = {{CENELEC} 50128 and {IEC} 62279 Standards}, publisher = {Wiley-ISTE}, year = 2015, - address = {Boston}, + address = {Boston} } @Booklet{ cc:cc-part3:2006, @@ -242,7 +236,7 @@ volume = 8558, publisher = pub-springer, year = 2014, - doi = {10.1007/978-3-319-08970-6}, + doi = {10.1007/978-3-319-08970-6} } @InProceedings{ bezzecchi.ea:making:2018, @@ -284,38 +278,37 @@ location = {Toulouse} } -@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}, +@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 } %%%%%%%%%%%%%%%%%%%%%% - @Misc{ datarefman19, title = {Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}, @@ -359,7 +352,7 @@ booktitle = {UITP}, pages = {84--94}, year = 2014, - doi = {10.4204/EPTCS.167.10}, + doi = {10.4204/EPTCS.167.10} } @InProceedings{ DBLP:conf/mkm/BarrasGHRTWW13, @@ -372,7 +365,7 @@ booktitle = {MKM}, pages = {359--363}, year = 2013, - doi = {10.1007/978-3-642-39320-4_29}, + doi = {10.1007/978-3-642-39320-4_29} } @Article{ Faithfull:2018:COQ:3204179.3204223, @@ -488,7 +481,6 @@ the development, deployment and maintenanceactivities.} } - @Article{ Regular-Sets-AFP, author = {Alexander Krauss and Tobias Nipkow}, title = {Regular Sets and Expressions}, @@ -521,7 +513,7 @@ author = {Makarius Wenzel}, title = {The {Isabelle} System Manual}, year = 2019, - note = {Part of the Isabelle distribution.} + note = {Part of the Isabelle distribution.} } @Booklet{ chervet:keycommand:2010, @@ -552,5 +544,5 @@ @Book{ eijkhout:latex-cs:2012, author = {Victor Eijkhout}, title = {The Computer Science of TeX and LaTeX}, - year = 2012, + year = 2012 } From 4692201cb0939436dd51d329bded1125df8485ed Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 17 Aug 2019 10:02:13 +0100 Subject: [PATCH 2/2] Normalized BibTeX keys. --- .../Isabelle_DOF-Manual/01_Introduction.thy | 2 +- .../Isabelle_DOF-Manual/02_Background.thy | 10 +-- .../Isabelle_DOF-Manual/03_GuidedTour.thy | 4 +- .../Isabelle_DOF-Manual/04_RefMan.thy | 4 +- .../Isabelle_DOF-Manual/05_Implementation.thy | 2 +- .../Isabelle_DOF-Manual/document/root.bib | 75 +++---------------- 6 files changed, 20 insertions(+), 77 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy index eb68c01..4d7f183 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy @@ -33,7 +33,7 @@ have to follow a structure. In practice, large groups of developers have to pro set of documents where the consistency is notoriously difficult to maintain. In particular, certifications are centered around the \<^emph>\traceability\ of requirements throughout the entire set of documents. While technical solutions for the traceability problem exists (most notably: -DOORS~\cite{doors}), they are weak in the treatment of formal entities (such as formulas and their +DOORS~\cite{ibm:doors:2019}), they are weak in the treatment of formal entities (such as formulas and their logical contexts). Further applications are the domain-specific discourse in juridical texts or medical reports. diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index fbed43a..80792fa 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -137,9 +137,9 @@ text\ theorems (protected by a kernel). This includes, \eg, ProofPower, HOL4, HOL-light, Isabelle, or Coq and its derivatives. \dof is, however, designed for fast interaction in an IDE. If a user wants to benefit from this experience, only Isabelle and Coq have the necessary infrastructure of - asynchronous proof-processing and support by a PIDE~@{cite "DBLP:conf/itp/Wenzel14" and - "DBLP:journals/corr/Wenzel14" and "DBLP:conf/mkm/BarrasGHRTWW13" - and "Faithfull:2018:COQ:3204179.3204223"} which in many features over-accomplishes the required + asynchronous proof-processing and support by a PIDE~@{cite "wenzel:asynchronous:2014" and + "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 \inlineisar+\ ... \ + barriers, while \dof actually only requires a two-level @@ -158,8 +158,8 @@ text\ Isabelle provides, beyond the features required for \dof, a lot of additional benefits. For example, it also allows the asynchronous evaluation and checking of the document - content~@{cite "DBLP:conf/itp/Wenzel14" and "DBLP:journals/corr/Wenzel14" and - "DBLP:conf/mkm/BarrasGHRTWW13"} and is dynamically extensible. Its PIDE provides a + content~@{cite "wenzel:asynchronous:2014" and "wenzel:system:2014" and + "barras.ea:pervasive:2013"} and is dynamically extensible. Its PIDE provides a \<^emph>\continuous build, continuous check\ functionality, syntax highlighting, and auto-completion. It also provides infrastructure for displaying meta-information (\eg, binding and type annotation) as pop-ups, while hovering over sub-expressions. A fine-grained dependency analysis allows the diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 70faafa..cf0b0fc 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -115,8 +115,8 @@ text\ This will create a directory \texttt{\isadofdirn} containing \isadof distribution. Next, we need to invoke the \inlinebash|install| script. If necessary, the installations automatically downloads additional dependencies from the AFP (\url{https://www.isa-afp.org}), -namely the AFP entries ``Functional Automata''~@{cite "Functional-Automata-AFP"} and ``Regular -Sets and Expressions''~@{cite "Regular-Sets-AFP"}. This might take a few minutes to complete. +namely the AFP entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} and ``Regular +Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a few minutes to complete. Moreover, the installation script applies a patch to the Isabelle system, which requires \<^emph>\write permissions for the Isabelle system directory\ and registers \isadof as Isabelle component. diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index f67b3cd..5ed1caa 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -257,12 +257,12 @@ text\ mathematical notations for $\lambda$-terms in Isabelle/HOL. Example expressions are: \inlineisar|1+2| (arithmetics), \inlineisar|[1,2,3]| (lists), \inlineisar|''ab c''| (strings), \inlineisar|{1,2,3}| (sets), \inlineisar|(1,2,3)| (tuples), - \inlineisar|\ x. P(x) \ Q x = C| (formulas). For details, see~@{cite "nipkowMain19"}. + \inlineisar|\ x. P(x) \ Q x = C| (formulas). For details, see~@{cite "nipkow:whats:2019"}. \ text\ Advanced ontologies can, \eg, use recursive function definitions with - pattern-matching~@{cite "functions19"}, extensible record + pattern-matching~@{cite "kraus:defining:2019"}, extensible record pecifications~@{cite "wenzel:isabelle-isar:2019"}, and abstract type declarations. \ diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy index 5381ff3..2947773 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy @@ -228,7 +228,7 @@ text\ is \emph{enabled} for this class; in this case, the \inlineisar+next+-operation is executed. The transformed automaton recognizing the rest-language is stored in \inlineisar+docobj_tab+ if possible; otherwise, if \inlineisar+next+ fails, an error is reported. The automata implementation - is, in large parts, generated from a formalization of functional automata~\cite{Functional-Automata-AFP}. + is, in large parts, generated from a formalization of functional automata~\cite{nipkow.ea:functional-Automata-afp:2004}. \ section\The \LaTeX-Core of \isadof\ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib index 68d9787..4557dc6 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib +++ b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib @@ -10,7 +10,7 @@ year = 2015 } -@Misc{ doors, +@Misc{ ibm:doors:2019, author = {IBM}, title = {{IBM} Engineering Requirements Management {DOORS} Family}, note = {\url{https://www.ibm.com/us-en/marketplace/requirements-management}}, @@ -308,8 +308,7 @@ year = 2007 } -%%%%%%%%%%%%%%%%%%%%%% -@Misc{ datarefman19, +@Misc{ biendarra.ea:defining:2019, title = {Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}, author = {Julian Biendarra and Jasmin Christian Blanchette and @@ -319,34 +318,21 @@ year = 2019 } -@Misc{ functions19, +@Misc{ kraus:defining:2019, title = {Defining Recursive Functions in Isabelle/HOL}, author = {Alexander Kraus}, note = {\url{https://isabelle.in.tum.de/doc/functions.pdf}}, year = 2019 } -@Misc{ nipkowMain19, +@Misc{ nipkow:whats:2019, title = {What's in Main}, author = {Tobias Nipkow}, note = {\url{https://isabelle.in.tum.de/doc/main.pdf}}, year = 2019 } -@InProceedings{ DBLP:conf/itp/Wenzel14, - author = {Makarius Wenzel}, - title = {Asynchronous User Interaction and Tool Integration in - Isabelle/PIDE}, - booktitle = {Interactive Theorem Proving (ITP)}, - pages = {515--530}, - year = 2014, - doi = {10.1007/978-3-319-08970-6_33}, - timestamp = {Sun, 21 May 2017 00:18:59 +0200}, - biburl = {https://dblp.org/rec/bib/conf/itp/Wenzel14}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} - -@InProceedings{ DBLP:journals/corr/Wenzel14, +@InProceedings{ wenzel:system:2014, author = {Makarius Wenzel}, title = {System description: Isabelle/{jEdit} in 2014}, booktitle = {UITP}, @@ -355,7 +341,7 @@ doi = {10.4204/EPTCS.167.10} } -@InProceedings{ DBLP:conf/mkm/BarrasGHRTWW13, +@InProceedings{ barras.ea:pervasive:2013, author = {Bruno Barras and Lourdes Del Carmen Gonz{\'{a}}lez{-}Huesca and Hugo Herbelin and Yann R{\'{e}}gis{-}Gianas and Enrico Tassi and Makarius Wenzel @@ -368,7 +354,7 @@ doi = {10.1007/978-3-642-39320-4_29} } -@Article{ Faithfull:2018:COQ:3204179.3204223, +@Article{ faithfull.ea:coqoon:2018, author = {Faithfull, Alexander and Bengtson, Jesper and Tassi, Enrico and Tankink, Carst}, title = {Coqoon}, @@ -381,55 +367,12 @@ issn = {1433-2779}, pages = {125--137}, numpages = 13, - url = {https://doi.org/10.1007/s10009-017-0457-2}, doi = {10.1007/s10009-017-0457-2}, acmid = 3204223, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg} } -@InCollection{ brucker.wolff19:isadof-design-impl:2019, - abstract = {DOF is a novel framework for \emph{defining} ontologies - and \emph{enforcing} them during document development and - document evolution. A major goal of DOF is the integrated - development of formal certification documents (\eg, 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 Isabelle/HOL. \isadof is - integrated into Isabelle'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. - \isadof 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 collaboratively, while \emph{ensuring their - consistency}, and the impact of changes (in the formal and - the semi-formal content) is tracked automatically.}, - address = {Heidelberg}, - author = {Achim D. Brucker and Burkhart Wolff}, - booktitle = {International Conference on Software Engineering and - Formal Methods (SEFM)}, - doi = {10.1007/978-3-319-96812-4_3}, - keywords = {Isabelle, HOL, Ontologies, Certification}, - language = {USenglish}, - location = {Oslo, Norway}, - number = {TO APPEAR}, - pdf = {https://www.lri.fr/~wolff/papers/conf/2019-sefm-isa_dof-framework.pdf}, - publisher = {Springer-Verlag}, - series = {Lecture Notes in Computer Science}, - title = {{I}sabelle/{DOF}: {D}esign and {I}mplementation}, - year = 2019 -} - @InProceedings{ abrial:steam-boiler:1996, author = {Abrial, Jean-Raymond}, title = {Steam-Boiler Control Specification Problem}, @@ -481,7 +424,7 @@ the development, deployment and maintenanceactivities.} } -@Article{ Regular-Sets-AFP, +@Article{ kraus.ea:regular-sets-afp:2010, author = {Alexander Krauss and Tobias Nipkow}, title = {Regular Sets and Expressions}, journal = {Archive of Formal Proofs}, @@ -492,7 +435,7 @@ issn = {2150-914x} } -@Article{ Functional-Automata-AFP, +@Article{ nipkow.ea:functional-Automata-afp:2004, author = {Tobias Nipkow}, title = {Functional Automata}, journal = {Archive of Formal Proofs},