Skip to content

Commit 4d6c567

Browse files
committed
Editorial change: replace by footbibliography
1 parent 0f1e73a commit 4d6c567

File tree

6 files changed

+47
-26
lines changed

6 files changed

+47
-26
lines changed

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

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -524,7 +524,7 @@ embedded systems; and Ada's low-level facilities, which allow the
524524
programmer to specify target-specific representations for data types
525525
(including the bit layout of fields in a record, and the values for
526526
enumeration elements). Further information on features that contribute
527-
to safe software may be found in :cite:p:`Barnes_Brosgol_2015`.
527+
to safe software may be found in :footcite:p:`Barnes_Brosgol_2015`.
528528

529529
In summary, Ada's benefits stem from its expressive power, allowing
530530
the developer to specify the needed functionality or to constrain the
@@ -1076,7 +1076,7 @@ AdaCore tools and the Ada language.
10761076
* A project using a C codebase can incrementally introduce Ada or
10771077
SPARK. Ada has standard support for interfacing with C, SPARK can be
10781078
combined with C (with checks at the interfaces)
1079-
:cite:p:`Kanig_Ochem_Comar_2016`, and AdaCore's :index:`GNAT Pro Common
1079+
:footcite:p:`Kanig_Ochem_Comar_2016`, and AdaCore's :index:`GNAT Pro Common
10801080
Code Generator` compiles a SPARK-like subset of Ada into C (for use
10811081
on processors lacking an Ada compiler). C projects can thus
10821082
progressively adopt higher-tier languages without losing the
@@ -1470,7 +1470,7 @@ VxWorks 6 Cert, Lynx178, PikeOS) as well as bare metal configurations,
14701470
for a wide range of processors (such as PowerPC and ARM).
14711471

14721472
The Ada language helps reduce the risk of introducing errors during
1473-
software development (see :cite:p:`Black_et_al_2011`). This is
1473+
software development (see :footcite:p:`Black_et_al_2011`). This is
14741474
achieved through a combination of specific programming constructs
14751475
together with static and dynamic checks. As a result, Ada code
14761476
standards tend to be shorter and simpler than C code standards, since
@@ -1976,7 +1976,7 @@ the outcome of the two tests is different.
19761976

19771977
In the general case, the MC/DC criterion for a decision with n
19781978
conditions requires n+1 tests, instead of 2\ :sup:`n`. For more
1979-
information about MC/DC, see :cite:p:`Hayhurst_et_al_2001`.
1979+
information about MC/DC, see :footcite:p:`Hayhurst_et_al_2001`.
19801980

19811981
.. index:: GNATcoverage
19821982
.. index:: single: Structural code coverage; GNATcoverage
@@ -3326,7 +3326,7 @@ requirements, and this may be appropriate for some critical kernel
33263326
modules. (A description of how SPARK may be introduced into a project
33273327
at various levels, depending on the system's assurance requirements,
33283328
may be found in a booklet co-authored by AdaCore and Thales
3329-
:cite:p:`AdaCore_Thales_2020`.) Since subprogram pre- and postcondition
3329+
:footcite:p:`AdaCore_Thales_2020`.) Since subprogram pre- and postcondition
33303330
contracts often express low-level requirements, some low-level
33313331
requirements-based testing may be replaced by formal proofs as
33323332
described in the |do-333| Formal Methods supplement to |do-178c|.
@@ -4162,3 +4162,10 @@ in this manner, completeness of verification is ensured.
41624162

41634163
The only remaining activity is to check that the PDI instance value
41644164
complies with the system configuration.
4165+
4166+
4167+
.. only:: builder_html
4168+
4169+
.. rubric:: Bibliography
4170+
4171+
.. footbibliography::

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

Lines changed: 0 additions & 6 deletions
This file was deleted.

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

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ satisfy various objectives of the standards. Many of the advantages
1313
of AdaCore's products stem from the software engineering support found
1414
in the Ada programming language, including features (such as
1515
contract-based programming) introduced in Ada\ |nbsp|\ 2012
16-
:cite:p:`ISO_IEC_2012`. Other advantages draw directly from the
17-
formally analyzable SPARK subset of Ada :cite:p:`AdaCore_Altran_2020`,
18-
:cite:p:`Dross_2022`, :cite:p:`Chapman_et_al_2024`. As a result, this
16+
:footcite:p:`ISO_IEC_2012`. Other advantages draw directly from the
17+
formally analyzable SPARK subset of Ada :footcite:p:`AdaCore_Altran_2020`,
18+
:footcite:p:`Dross_2022`, :footcite:p:`Chapman_et_al_2024`. As a result, this
1919
document identifies how Ada and SPARK contribute toward the
2020
development of reliable software. AdaCore personnel have played key
2121
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
105105
AdaCore and the designated authority to confirm its acceptability. The
106106
level of detail in the process description provided in the project
107107
plans and standard is a key factor in gaining acceptance.
108+
109+
110+
.. only:: builder_html
111+
112+
.. rubric:: Bibliography
113+
114+
.. footbibliography::

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

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ Overview
1111
"Every State has complete and exclusive sovereignty over the airspace
1212
above its territory." This general principle was codified in Article 1
1313
of the Convention on International Civil Aviation (the "Chicago
14-
Convention") in 1944 :cite:p:`ICAO_1944`. To control the airspace,
14+
Convention") in 1944 :footcite:p:`ICAO_1944`. To control the airspace,
1515
harmonized regulations have been formulated to ensure that the
1616
aircraft are airworthy.
1717

@@ -28,7 +28,7 @@ Operating Performance Standards" (MOPS) and a set of recognized
2828
|do-254| for Complex Electronic Hardware.
2929

3030
*DO-178C/ED-12C - Software Considerations in Airborne Systems and
31-
Equipment Certification* :cite:p:`RTCA_EUROCAE_2011` |mdash| was issued in
31+
Equipment Certification* :footcite:p:`RTCA_EUROCAE_2011` |mdash| was issued in
3232
December 2011, developed jointly by RTCA, Inc., and EUROCAE. It is the
3333
primary document by which certification authorities such as the FAA,
3434
EASA, and Transport Canada approve all commercial software-based
@@ -79,7 +79,7 @@ The |do-178c| document suite comprises:
7979
in other application domains.
8080

8181
Details on how to use these standards in practice may be found in
82-
:cite:p:`Rierson_2013`.
82+
:footcite:p:`Rierson_2013`.
8383

8484
.. index:: Design Assurance Level (DAL), Software level
8585

@@ -237,8 +237,8 @@ target computer, the other objectives of EOC verification may be
237237
satisfied by formal analysis. This is a significant added
238238
value. However, employing formal analysis to replace tests is a new
239239
concept in the avionics domain, with somewhat limited experience in
240-
practice thus far (see :cite:p:`Moy_et_al_2013` for further
241-
information). As noted in :cite:p:`Moy_2017`, a significant issue is
240+
practice thus far (see :footcite:p:`Moy_et_al_2013` for further
241+
information). As noted in :footcite:p:`Moy_2017`, a significant issue is
242242
how to demonstrate that the compiler generates code that properly
243243
preserves the properties that have been formally demonstrated for the
244244
source code. Running the integration tests both with and without the
@@ -270,3 +270,10 @@ Certification credit for using formal proofs is summarized in
270270
:align: center
271271

272272
SPARK contributions to verification objectives
273+
274+
275+
.. only:: builder_html
276+
277+
.. rubric:: Bibliography
278+
279+
.. footbibliography::

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

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,8 @@ for contract-based programming in the form of subprogram pre- and
3030
postconditions and type invariants) were added in the Ada 2012 version
3131
of the language standard, and a number of features to increase the
3232
language's expressiveness were introduced in Ada 2022 (see
33-
:cite:p:`ISO_IEC_2012`, :cite:p:`Barnes_Brosgol_2015`,
34-
:cite:p:`Barnes_2014`, :cite:p:`ISO_IEC_2022` for information about
33+
:footcite:p:`ISO_IEC_2012`, :footcite:p:`Barnes_Brosgol_2015`,
34+
:footcite:p:`Barnes_2014`, :footcite:p:`ISO_IEC_2022` for information about
3535
Ada).
3636

3737
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
199199
Ada is methodologically neutral and does not impose a distributed
200200
overhead for OOP. If an application does not need OOP, then the OOP
201201
features do not have to be used, and there is no run-time penalty.
202-
See :cite:p:`Barnes_2014` or :cite:p:`AdaCore_2016` for more details.
202+
See :footcite:p:`Barnes_2014` or :footcite:p:`AdaCore_2016` for more details.
203203

204204
.. index:: single: Ada language; Concurrent programming
205205

@@ -264,7 +264,7 @@ With its emphasis on sound software engineering principles, Ada
264264
supports the development of high-integrity applications, including
265265
those that need to be certified against safety standards such
266266
|do-178c| for avionics, CENELEC EN 50716:2023 for rail systems, and
267-
security standards such as the Common Criteria :cite:p:`CCDB_2022`.
267+
security standards such as the Common Criteria :footcite:p:`CCDB_2022`.
268268
Key to Ada's support for high-assurance software is the language's
269269
memory safety; this is illustrated by a number of features, including:
270270

@@ -358,7 +358,7 @@ cross-domain solutions.
358358

359359
The SPARK language has been stable over the years, with periodic
360360
enhancements. The 2014 version of SPARK represented a major revision
361-
(see :cite:p:`McCormick_Chapin_2015`), incorporating contract-based
361+
(see :footcite:p:`McCormick_Chapin_2015`), incorporating contract-based
362362
programming syntax from Ada 2012, and subsequent upgrades included
363363
support for pointers (access types) based on the Rust ownership model.
364364

@@ -399,7 +399,7 @@ Ease of Adoption
399399

400400
User experience has shown that the language and the SPARK Pro toolset
401401
do not require a steep learning curve. Training material such as
402-
AdaCore's online AdaLearn course for SPARK :cite:p:`Learn` can
402+
AdaCore's online AdaLearn course for SPARK :footcite:p:`Learn` can
403403
quickly bring developers up to speed; users are assumed to be experts
404404
in their own application domain such as avionics software and do not
405405
need to be familiar with formal methods or the proof technology
@@ -1122,3 +1122,10 @@ eliminating the need for manual input.
11221122
GNATdashboard fits naturally into a continuous integration
11231123
environment, providing users with metrics on code complexity, code
11241124
coverage, conformance to coding standards, and more.
1125+
1126+
1127+
.. only:: builder_html
1128+
1129+
.. rubric:: Bibliography
1130+
1131+
.. footbibliography::

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -158,4 +158,3 @@ booklet.
158158
AdaCore Tools and Technologies Overview <chapters/tools>
159159
Compliance with DO-178C / ED-12C Guidance: Analysis <chapters/analysis>
160160
Summary of contributions to DO-178C/ED-12C objectives <chapters/summary>
161-
Bibliography <chapters/bibliography>

0 commit comments

Comments
 (0)