| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Isabelle_C/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 6 kB |
|
Quelle README.thySprache: Isabelle |
|||||||||||||||
|
(****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) (* Authors: Frédéric Tuong, Burkhart Wolff *) theory README imports Main begin section ‹Isabelle/C› text ‹ /C contains a C99/C11/C18 front-end support for Isabelle. The front-end is actua two possibly interchangeable parsers (from two different projects): ▪ 🍋‹C11-FrontEnd›: 🪙‹https://hackage.haskell.org/package/language-c› ▪ 🪙‹https://gitlri.lri.fr/ftuong/isabelle_c/tree/C/C18-FrontEnd›: 🪙‹https://github.com/jhjourdan/C11parser› present, the recommended and default version is C11. section ‹Getting started› text ‹ A first installation step is: ▪ 🍋‹isabelle build -D› 🍋‹.› › text ‹ which should work out of the box. › text ‹ The following C examples or entry-points of documentation can be executed: ▪ 🍋‹isabelle jedit -d› 🍋‹.› 🍋‹C11-FrontEnd/examples/C0.thy› ▪ 🍋‹isabelle jedit -d› 🍋‹.› 🍋‹C11-FrontEnd/examples/C2.thy› ▪ 🍋‹isabelle jedit -d› 🍋‹.› 🍋‹C11-FrontEnd/examples/C1.thy› ▪ 🍋‹isabelle jedit -d› 🍋‹.› 🍋‹C11-FrontEnd/appendices/C_Appendices.thy› › text ‹ ▪ The example 🍋‹C11-FrontEnd/examples/C0.thy› is basically used to the faithfulness of the C11 parser implementation. ▪ The example 🍋‹C11-FrontEnd/examples/C2.thy› shows common cases of C and editing support in PIDE; it also contains annotation commands without any seman ▪ The example 🍋‹C11-FrontEnd/examples/C1.thy› is a show-case for markup and the use of bindings resulting from the static C environment. ▪ The example 🍋‹C11-FrontEnd/appendices/C_Appendices.thy› shows the use of /C documentation facilities. text ‹ AFP version of Isabelle/C does not include semantic back-ends (these are distri submissions or available via the web; see below). The structure of 🍋‹.› has designed to create a directory ‹C11-BackEnds› into which back-ends can be . The structure of 🍋‹.› is actually similar as 🪙‹https://gitlri.lri.fr/ftuong/isabelle_c›: see for example 🪙‹https://gitlri.lri.fr/ftuong/isabelle_c/tree/C/C11-BackEnds› where several -ends can be copied and tried. subsection ‹Isabelle/C/README› text ‹ 🍋‹README.md› is automatically generated from 🍋‹README.thy› 🪙‹https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/README.sh›. › text ‹ Note that this shell-script requires the prior installation of 🍋‹pandoc› (🪙‹https://github.com/jgm/pandoc›). › section ‹Authors› text ‹ ▪ Frédéric Tuong (🪙‹https://www.lri.fr/~ftuong›) ▪ Burkhart Wolff (🪙‹https://www.lri.fr/~wolff›) › section ‹License› text ‹ /C is licensed under a 3-clause BSD-style license (where certain files are in th compatible with the 3-clause BSD). more details: ▪ The generated files 🍋‹C11-FrontEnd/generated/c_ast.ML› and 🍋‹C11-FrontEnd/generated/c_grammar_fun.grm› are mixing several source code of different projects: ▪ In 3-clause BSD: the part representing the Haskell Language.C library. ▪ In 2-clause BSD: the C99 AST in HOL (before reflection to SML) adapted from th one in the L4.verified project. ▪ In 3-clause BSD: the HOL translation C11 to C99 from the Securify project. ▪ In 3-clause BSD: any other binding and translations of meta-models from the Ci project. ▪ In 3-clause BSD: the two combined generators generating 🍋‹C11-FrontEnd/generated/c_ast.ML› based on some modified version of Haskabelle and Citadelle. ▪ In 3-clause BSD: the Happy modified generator generating 🍋‹C11-FrontEnd/generated/c_grammar_fun.grm› ▪ In HPND: the ML-Yacc modified generator generating the two 🍋‹C11-FrontEnd/generated/c_grammar_fun.grm.sig› and 🍋‹C11-FrontEnd/generated/c_grammar_fun.grm.sml› (i.e., the ML-Yacc version of MLton). ▪ In HPND: the modified grammar library of ML-Yacc loaded in 🍋‹C11-FrontEnd/src/C_Parser_Language.thy›. ▪ In 3-clause BSD: the remaining files in 🍋‹C11-FrontEnd/src› constituting Isabelle/C core implementation. ▪ Most examples in 🍋‹C11-FrontEnd/examples› are in 3-clause BSD, some are used for quotation purposes to test the Isabelle/C lexer (hyperlinks around each their provenance). end
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-09) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09