Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Normalized BibTeX keys.

This commit is contained in:
Achim D. Brucker 2019-08-17 10:02:13 +01:00
parent c92376871c
commit 4692201cb0
6 changed files with 20 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
View File

@ -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>\<open>traceability\<close> 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.

10
examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
View File

@ -137,9 +137,9 @@ text\<open>
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+\<Open> ... \<Close> + barriers, while \dof actually only requires a two-level
@ -158,8 +158,8 @@ text\<open>
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>\<open>continuous build, continuous check\<close> 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

4
examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
View File

@ -115,8 +115,8 @@ text\<open>
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>\<open>write permissions for the Isabelle system directory\<close> and registers \isadof as Isabelle component.

4
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -257,12 +257,12 @@ text\<open>
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|\<forall> x. P(x) \<and> Q x = C| (formulas). For details, see~@{cite "nipkowMain19"}.
\inlineisar|\<forall> x. P(x) \<and> Q x = C| (formulas). For details, see~@{cite "nipkow:whats:2019"}.
\<close>
text\<open>
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.
\<close>

2
examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
View File

@ -228,7 +228,7 @@ text\<open>
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}.
\<close>
section\<open>The \LaTeX-Core of \isadof\<close>

75
examples/technical_report/Isabelle_DOF-Manual/document/root.bib
View File

@ -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},