Merge pull request #1295 from gusthoff/content/adacore-technologies-for-airborne-software/editorial/review/20251226

Editorial change: replace by `footbibliography`

Author: gusthoff

content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst

@@ -524,7 +524,7 @@ embedded systems; and Ada's low-level facilities, which allow the
 programmer to specify target-specific representations for data types
 (including the bit layout of fields in a record, and the values for
 enumeration elements). Further information on features that contribute
-to safe software may be found in :cite:p:`Barnes_Brosgol_2015`.
+to safe software may be found in :footcite:p:`Barnes_Brosgol_2015`.
 
 In summary, Ada's benefits stem from its expressive power, allowing
 the developer to specify the needed functionality or to constrain the
@@ -1076,7 +1076,7 @@ AdaCore tools and the Ada language.
 * A project using a C codebase can incrementally introduce Ada or
   SPARK. Ada has standard support for interfacing with C, SPARK can be
   combined with C (with checks at the interfaces)
-  :cite:p:`Kanig_Ochem_Comar_2016`, and AdaCore's :index:`GNAT Pro Common
+  :footcite:p:`Kanig_Ochem_Comar_2016`, and AdaCore's :index:`GNAT Pro Common
   Code Generator` compiles a SPARK-like subset of Ada into C (for use
   on processors lacking an Ada compiler). C projects can thus
   progressively adopt higher-tier languages without losing the
@@ -1470,7 +1470,7 @@ VxWorks 6 Cert, Lynx178, PikeOS) as well as bare metal configurations,
 for a wide range of processors (such as PowerPC and ARM).
 
 The Ada language helps reduce the risk of introducing errors during
-software development (see :cite:p:`Black_et_al_2011`). This is
+software development (see :footcite:p:`Black_et_al_2011`). This is
 achieved through a combination of specific programming constructs
 together with static and dynamic checks. As a result, Ada code
 standards tend to be shorter and simpler than C code standards, since
@@ -1976,7 +1976,7 @@ the outcome of the two tests is different.
 
 In the general case, the MC/DC criterion for a decision with n
 conditions requires n+1 tests, instead of 2\ :sup:`n`. For more
-information about MC/DC, see :cite:p:`Hayhurst_et_al_2001`.
+information about MC/DC, see :footcite:p:`Hayhurst_et_al_2001`.
 
 .. index:: GNATcoverage
 .. index:: single: Structural code coverage; GNATcoverage
@@ -3326,7 +3326,7 @@ requirements, and this may be appropriate for some critical kernel
 modules. (A description of how SPARK may be introduced into a project
 at various levels, depending on the system's assurance requirements,
 may be found in a booklet co-authored by AdaCore and Thales
-:cite:p:`AdaCore_Thales_2020`.) Since subprogram pre- and postcondition
+:footcite:p:`AdaCore_Thales_2020`.) Since subprogram pre- and postcondition
 contracts often express low-level requirements, some low-level
 requirements-based testing may be replaced by formal proofs as
 described in the |do-333| Formal Methods supplement to |do-178c|.
@@ -4162,3 +4162,10 @@ in this manner, completeness of verification is ensured.
 
 The only remaining activity is to check that the PDI instance value
 complies with the system configuration.
+
+
+.. only:: builder_html
+
+    .. rubric:: Bibliography
+
+.. footbibliography::

content/booklets/adacore-technologies-for-airborne-software/chapters/bibliography.rst

@@ -13,9 +13,9 @@ satisfy various objectives of the standards.  Many of the advantages
 of AdaCore's products stem from the software engineering support found
 in the Ada programming language, including features (such as
 contract-based programming) introduced in Ada\ |nbsp|\ 2012
-:cite:p:`ISO_IEC_2012`.  Other advantages draw directly from the
-formally analyzable SPARK subset of Ada :cite:p:`AdaCore_Altran_2020`,
-:cite:p:`Dross_2022`, :cite:p:`Chapman_et_al_2024`.  As a result, this
+:footcite:p:`ISO_IEC_2012`.  Other advantages draw directly from the
+formally analyzable SPARK subset of Ada :footcite:p:`AdaCore_Altran_2020`,
+:footcite:p:`Dross_2022`, :footcite:p:`Chapman_et_al_2024`.  As a result, this
 document identifies how Ada and SPARK contribute toward the
 development of reliable software. AdaCore personnel have played key
 roles in the design and implementation of both of these languages.
@@ -105,3 +105,10 @@ or technique is introduced, it's important to open a discussion with
 AdaCore and the designated authority to confirm its acceptability. The
 level of detail in the process description provided in the project
 plans and standard is a key factor in gaining acceptance.
+
+
+.. only:: builder_html
+
+    .. rubric:: Bibliography
+
+.. footbibliography::

content/booklets/adacore-technologies-for-airborne-software/chapters/introduction.rst

@@ -11,7 +11,7 @@ Overview
 "Every State has complete and exclusive sovereignty over the airspace
 above its territory." This general principle was codified in Article 1
 of the Convention on International Civil Aviation (the "Chicago
-Convention") in 1944 :cite:p:`ICAO_1944`. To control the airspace,
+Convention") in 1944 :footcite:p:`ICAO_1944`. To control the airspace,
 harmonized regulations have been formulated to ensure that the
 aircraft are airworthy.
 
@@ -28,7 +28,7 @@ Operating Performance Standards" (MOPS) and a set of recognized
 |do-254| for Complex Electronic Hardware.
 
 *DO-178C/ED-12C - Software Considerations in Airborne Systems and
-Equipment Certification* :cite:p:`RTCA_EUROCAE_2011` |mdash| was issued in
+Equipment Certification* :footcite:p:`RTCA_EUROCAE_2011` |mdash| was issued in
 December 2011, developed jointly by RTCA, Inc., and EUROCAE. It is the
 primary document by which certification authorities such as the FAA,
 EASA, and Transport Canada approve all commercial software-based
@@ -79,7 +79,7 @@ The |do-178c| document suite comprises:
   in other application domains.
 
 Details on how to use these standards in practice may be found in
-:cite:p:`Rierson_2013`.
+:footcite:p:`Rierson_2013`.
 
 .. index:: Design Assurance Level (DAL), Software level
 
@@ -237,8 +237,8 @@ target computer, the other objectives of EOC verification may be
 satisfied by formal analysis. This is a significant added
 value. However, employing formal analysis to replace tests is a new
 concept in the avionics domain, with somewhat limited experience in
-practice thus far (see :cite:p:`Moy_et_al_2013` for further
-information).  As noted in :cite:p:`Moy_2017`, a significant issue is
+practice thus far (see :footcite:p:`Moy_et_al_2013` for further
+information).  As noted in :footcite:p:`Moy_2017`, a significant issue is
 how to demonstrate that the compiler generates code that properly
 preserves the properties that have been formally demonstrated for the
 source code. Running the integration tests both with and without the
@@ -270,3 +270,10 @@ Certification credit for using formal proofs is summarized in
   :align: center
 
   SPARK contributions to verification objectives
+
+
+.. only:: builder_html
+
+    .. rubric:: Bibliography
+
+.. footbibliography::

content/booklets/adacore-technologies-for-airborne-software/chapters/standards.rst

@@ -30,8 +30,8 @@ for contract-based programming in the form of subprogram pre- and
 postconditions and type invariants) were added in the Ada 2012 version
 of the language standard, and a number of features to increase the
 language's expressiveness were introduced in Ada 2022 (see
-:cite:p:`ISO_IEC_2012`, :cite:p:`Barnes_Brosgol_2015`,
-:cite:p:`Barnes_2014`, :cite:p:`ISO_IEC_2022` for information about
+:footcite:p:`ISO_IEC_2012`, :footcite:p:`Barnes_Brosgol_2015`,
+:footcite:p:`Barnes_2014`, :footcite:p:`ISO_IEC_2022` for information about
 Ada).
 
 The name *Ada* is not an acronym; it was chosen in honor of Augusta
@@ -199,7 +199,7 @@ additional OOP features including Java-like interfaces and traditional
 Ada is methodologically neutral and does not impose a distributed
 overhead for OOP. If an application does not need OOP, then the OOP
 features do not have to be used, and there is no run-time penalty.
-See :cite:p:`Barnes_2014` or :cite:p:`AdaCore_2016` for more details.
+See :footcite:p:`Barnes_2014` or :footcite:p:`AdaCore_2016` for more details.
 
 .. index:: single: Ada language; Concurrent programming
 
@@ -264,7 +264,7 @@ With its emphasis on sound software engineering principles, Ada
 supports the development of high-integrity applications, including
 those that need to be certified against safety standards such
 |do-178c| for avionics, CENELEC EN 50716:2023 for rail systems, and
-security standards such as the Common Criteria :cite:p:`CCDB_2022`.
+security standards such as the Common Criteria :footcite:p:`CCDB_2022`.
 Key to Ada's support for high-assurance software is the language's
 memory safety; this is illustrated by a number of features, including:
 
@@ -358,7 +358,7 @@ cross-domain solutions.
 
 The SPARK language has been stable over the years, with periodic
 enhancements.  The 2014 version of SPARK represented a major revision
-(see :cite:p:`McCormick_Chapin_2015`), incorporating contract-based
+(see :footcite:p:`McCormick_Chapin_2015`), incorporating contract-based
 programming syntax from Ada 2012, and subsequent upgrades included
 support for pointers (access types) based on the Rust ownership model.
 
@@ -399,7 +399,7 @@ Ease of Adoption
 
 User experience has shown that the language and the SPARK Pro toolset
 do not require a steep learning curve. Training material such as
-AdaCore's online AdaLearn course for SPARK :cite:p:`Learn` can
+AdaCore's online AdaLearn course for SPARK :footcite:p:`Learn` can
 quickly bring developers up to speed; users are assumed to be experts
 in their own application domain such as avionics software and do not
 need to be familiar with formal methods or the proof technology
@@ -1122,3 +1122,10 @@ eliminating the need for manual input.
 GNATdashboard fits naturally into a continuous integration
 environment, providing users with metrics on code complexity, code
 coverage, conformance to coding standards, and more.
+
+
+.. only:: builder_html
+
+    .. rubric:: Bibliography
+
+.. footbibliography::

content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst

@@ -2,4 +2,4 @@
 title=AdaCore Technologies for Airborne Software
 author=Frédéric Pothon \\and Quentin Ochem
 version=2.1
-bibtex_file=references.bib
+bibtex_file=references.bib

content/booklets/adacore-technologies-for-airborne-software/conf.ini

@@ -158,4 +158,3 @@ booklet.
    AdaCore Tools and Technologies Overview <chapters/tools>
    Compliance with DO-178C / ED-12C Guidance: Analysis <chapters/analysis>
    Summary of contributions to DO-178C/ED-12C objectives <chapters/summary>
-   Bibliography <chapters/bibliography>

content/booklets/adacore-technologies-for-airborne-software/index.rst

@@ -235,10 +235,3 @@ Annex D References
 ~~~~~~~~~~~~~~~~~~
 
 * D.50 Structure Based Testing
-
-
-.. only:: builder_html
-
-    .. rubric:: Bibliography
-
-.. footbibliography::

content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst

@@ -149,7 +149,7 @@ and technologies:
 * Support tools and languages (sub-clause 6.7) |mdash| see
   :ref:`Railway_SW_tool-qualification` below.
 
-As shown in :cite:`Railway_SW_Boulanger_Schön_2007`, for software applications the
+As shown in :footcite:p:`Railway_SW_Boulanger_Schön_2007`, for software applications the
 assessment process involves demonstrating that the software application
 achieves its associated safety objectives.
 
@@ -340,7 +340,8 @@ referred to here as "tool qualification", and provides details on what
 needs to be performed and/or supplied.
 (The standard does not use a specific term for this process, but the
 "tool qualification" terminology from the airborne software standards
-|do-178c| :cite:`Railway_SW_RTCA_EUROCAE_2011a` and |do-330| :cite:`Railway_SW_RTCA_EUROCAE_2011b`
+|do-178c| :footcite:p:`Railway_SW_RTCA_EUROCAE_2011a` and |do-330|
+:footcite:p:`Railway_SW_RTCA_EUROCAE_2011b`
 is appropriate.)
 
 .. index:: Tool classes
@@ -388,7 +389,7 @@ standard by also specifying the lifecycle phase that is relevant for each
 sub-clause.
 The steps shown indicate the requirements to be met and reflect the additional
 effort needed as the tool level increases; for further information, please see
-:cite:`Railway_SW_Boulanger_2015`, Chapter 9.
+:footcite:p:`Railway_SW_Boulanger_2015`, Chapter 9.
 
 
 .. .. figure:: ../images/table1.png

content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst

@@ -13,11 +13,12 @@ and also a normative process based on certification standards.
 In Europe, these standards are issued and maintained by CENELEC
 (European Committee for Electrotechnical Standardization).
 This document explains the usage of AdaCore's technologies in conjunction
-with |en-50128|:2011 :cite:`Railway_SW_CENELEC_2011` |mdash|
+with |en-50128|:2011 :footcite:p:`Railway_SW_CENELEC_2011` |mdash|
 *Railway applications - Communication, signalling and processing systems
 - Software for railway control and protection systems* |mdash|
 as modified by amendments
-|en-50128|/A1 :cite:`Railway_SW_CENELEC_2020a` and |en-50128|/A2 :cite:`Railway_SW_CENELEC_2020b`.
+|en-50128|/A1 :footcite:p:`Railway_SW_CENELEC_2020a` and |en-50128|/A2
+:footcite:p:`Railway_SW_CENELEC_2020b`.
 (For ease of exposition, the 2011 edition of the standard, as modified
 by the A1 and A2 amendments, will simply be referred to as |en-50128|.)
 
@@ -31,19 +32,20 @@ standards:
 
 .. index:: EN 50126
 
-* |en-50126|-1 :cite:`Railway_SW_CENELEC_2017b`  |mdash|
+* |en-50126|-1 :footcite:p:`Railway_SW_CENELEC_2017b`  |mdash|
   *Railway applications - The specification and demonstration of reliability,
   availability, maintainability and safety (RAMS) - Part 1: Generic RAMS
-  process* (subsequently modified by |en-50126|-1/A1 :cite:`Railway_SW_CENELEC_2024`)
+  process* (subsequently modified by |en-50126|-1/A1
+  :footcite:p:`Railway_SW_CENELEC_2024`)
 
-* |en-50126|-2 :cite:`Railway_SW_CENELEC_2017c`  |mdash|
+* |en-50126|-2 :footcite:p:`Railway_SW_CENELEC_2017c`  |mdash|
   *Railway applications - The specification and demonstration of reliability,
   availability, maintainability and safety (RAMS): Part 2: systems approach
   to safety*
 
 .. index:: EN 50129
 
-* |en-50129| :cite:`Railway_SW_CENELEC_2018` |mdash|
+* |en-50129| :footcite:p:`Railway_SW_CENELEC_2018` |mdash|
   *Railway applications - Communication, signalling and processing systems -
   Safety related electronic systems for signalling*
 
@@ -61,8 +63,8 @@ relate to software's role in the safety of a railway system:
 
 .. index:: EN 50657
 
-* |en-50657|:2017 :cite:`Railway_SW_CENELEC_2017a` as modified by amendment
-  |en-50657|/A1 :cite:`Railway_SW_CENELEC_2023a` |mdash|
+* |en-50657|:2017 :footcite:p:`Railway_SW_CENELEC_2017a` as modified by amendment
+  |en-50657|/A1 :footcite:p:`Railway_SW_CENELEC_2023a` |mdash|
   *Railways applications - Rolling stock applications - Software on Board
   Rolling Stock*
 
@@ -75,7 +77,7 @@ relate to software's role in the safety of a railway system:
 
 .. index:: EN 50716
 
-* |en-50716|:2023 :cite:`Railway_SW_CENELEC_2023b` |mdash|
+* |en-50716|:2023 :footcite:p:`Railway_SW_CENELEC_2023b` |mdash|
   *Railway Applications - Requirements for software development*
 
   This standard is a successor to |en-50128| and |en-50657|,
@@ -149,12 +151,14 @@ processes defined by the CENELEC railway standards.
 AdaCore's technologies can be used at all Safety Integrity Levels, from
 Basic Integrity to |sil4|. At lower levels, the full Ada language is suitable,
 independent of platform. At higher levels, specific subsets will be needed,
-for example the :index:`Ravenscar Profile` (:cite:`Railway_SW_Burns_et_al_2004`,
-:cite:`Railway_SW_McCormick_Chapin_2015`) for concurrency support with analyzable
-semantics and a reduced footprint, or the :index:`Light Profile`
-:cite:`Railway_SW_AdaCore_Web_UG_Cross` for a subset with no run-time library
+for example the :index:`Ravenscar Profile`
+(:footcite:p:`Railway_SW_Burns_et_al_2004`,
+:footcite:p:`Railway_SW_McCormick_Chapin_2015`) for concurrency support with
+analyzable semantics and a reduced footprint, or the :index:`Light Profile`
+:footcite:p:`Railway_SW_AdaCore_Web_UG_Cross` for a subset with no run-time library
 requirements. At the highest level (|sil4|) the SPARK language
-(:cite:`Railway_SW_McCormick_Chapin_2015`, :cite:`Railway_SW_AdaCore_Altran_2020`) and its
+(:footcite:p:`Railway_SW_McCormick_Chapin_2015`,
+:footcite:p:`Railway_SW_AdaCore_Altran_2020`) and its
 verification toolsuite enable mathematical proof of properties including
 correct information flow, absence of run-time exceptions, and, for the most
 critical code, correctness of the implementation against a formally