Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
e6c6592143
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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>
|
||||
|
||||
|
|
|
|||
|
|
@ -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>
|
||||
|
|
|
|||
|
|
@ -3,33 +3,27 @@
|
|||
@STRING{s-lncs = "LNCS" }
|
||||
|
||||
@Misc{ w3c:ontologies:2015,
|
||||
author = {W3C},
|
||||
author = {W3C},
|
||||
title = {Ontologies},
|
||||
organisation = {W3c},
|
||||
url = {https://www.w3.org/standards/semanticweb/ontology},
|
||||
year = 2015
|
||||
}
|
||||
|
||||
@Misc{ doors,
|
||||
author = {IBM},
|
||||
@Misc{ ibm:doors:2019,
|
||||
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,39 +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,
|
||||
@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
|
||||
|
|
@ -326,43 +318,30 @@
|
|||
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},
|
||||
pages = {84--94},
|
||||
year = 2014,
|
||||
doi = {10.4204/EPTCS.167.10},
|
||||
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
|
||||
|
|
@ -372,10 +351,10 @@
|
|||
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,
|
||||
@Article{ faithfull.ea:coqoon:2018,
|
||||
author = {Faithfull, Alexander and Bengtson, Jesper and Tassi,
|
||||
Enrico and Tankink, Carst},
|
||||
title = {Coqoon},
|
||||
|
|
@ -388,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},
|
||||
|
|
@ -488,8 +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},
|
||||
|
|
@ -500,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},
|
||||
|
|
@ -521,7 +456,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 +487,5 @@
|
|||
@Book{ eijkhout:latex-cs:2012,
|
||||
author = {Victor Eijkhout},
|
||||
title = {The Computer Science of TeX and LaTeX},
|
||||
year = 2012,
|
||||
year = 2012
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue