@@ -34,10 +34,10 @@ Additional features (including support for contract-based programming
3434in the form of subprogram pre- and postconditions and type invariants)
3535were added in the Ada 2012 version of the language standard, and a
3636number of features to increase the language's expressiveness were
37- introduced in Ada 2022 (see :cite : `Railway_SW_ISO_IEC_2016 `,
38- :cite : `Railway_SW_Barnes_Brosgol_2015 `,
39- :cite : `Railway_SW_Barnes_2014 `,
40- :cite : `Railway_SW_ISO_IEC_2022 ` for information about Ada).
37+ introduced in Ada 2022 (see :footcite:p : `Railway_SW_ISO_IEC_2016 `,
38+ :footcite:p : `Railway_SW_Barnes_Brosgol_2015 `,
39+ :footcite:p : `Railway_SW_Barnes_2014 `,
40+ :footcite:p : `Railway_SW_ISO_IEC_2022 ` for information about Ada).
4141
4242.. index :: Lovelace (Augusta Ada), Babbage (Charles), Byron (Lord George)
4343
@@ -209,7 +209,8 @@ traditional :ada:`obj.op(...)` operation invocation notation.
209209Ada is methodologically neutral and does not impose a distributed overhead for
210210OOP. If an application does not need OOP, then the OOP features do not have
211211to be used, and there is no run-time penalty.
212- See :cite: `Railway_SW_Barnes_2014 ` or :cite: `Railway_SW_AdaCore_2016 ` for more details..
212+ See :footcite:p: `Railway_SW_Barnes_2014 ` or
213+ :footcite:p: `Railway_SW_AdaCore_2016 ` for more details.
213214
214215.. index :: single: Ada language; Concurrent programming
215216
@@ -276,8 +277,9 @@ High-Integrity Systems
276277With its emphasis on sound software engineering principles, Ada supports the
277278development of high-integrity applications, including those that need to be
278279certified against safety standards such |en-50128 | for rail systems,
279- |do-178c | :cite: `Railway_SW_RTCA_EUROCAE_2011a ` for avionics, and security standards
280- such as the Common Criteria :cite: `Railway_SW_CCDB_2022 `.
280+ |do-178c | :footcite:p: `Railway_SW_RTCA_EUROCAE_2011a `
281+ for avionics, and security standards
282+ such as the Common Criteria :footcite:p: `Railway_SW_CCDB_2022 `.
281283Key to Ada's support for high-assurance software is the language's
282284memory safety; this is illustrated by a number of features, including:
283285
@@ -379,7 +381,8 @@ software, and cross-domain solutions.
379381
380382The SPARK language has been stable over the years, with periodic
381383enhancements. The 2014 version of SPARK represented a major revision
382- :cite: `Railway_SW_McCormick_Chapin_2015 `, :cite: `Railway_SW_AdaCore_Altran_2020 `),
384+ :footcite:p: `Railway_SW_McCormick_Chapin_2015 `,
385+ :footcite:p: `Railway_SW_AdaCore_Altran_2020 `),
383386incorporating contract-based programming
384387syntax from Ada 2012, and subsequent upgrades included support for pointers
385388(access types) based on the Rust ownership model.
@@ -421,7 +424,8 @@ Ease of Adoption
421424
422425User experience has shown that the language and the SPARK Pro toolset do not
423426require a steep learning curve. Training material such as AdaCore's online
424- AdaLearn course for SPARK :cite: `Railway_SW_AdaCore_AdaLearn ` can quickly bring
427+ AdaLearn course for SPARK
428+ :footcite:p: `Railway_SW_AdaCore_AdaLearn ` can quickly bring
425429developers up to speed; users are assumed to be experts in their own
426430application domain such as railway software and do not need to be familiar
427431with formal methods or the proof technology implemented by the toolset.
@@ -519,13 +523,14 @@ Language and Tool Support
519523GNAT Pro Assurance for Ada supports all versions of the Ada
520524language standard as well as multiple versions of C (C89, C99, and C11).
521525It provides an Integrated Development Environment
522- (see :ref: `Railway_SW_Integrated_Development_Environments `), a comprehensive toolsuite
526+ (see :ref: `Railway_SW_Integrated_Development_Environments `),
527+ a comprehensive toolsuite
523528including a visual debugger, and an extensive set of libraries and bindings.
524529Details on the GNAT Pro for Ada toolchain may be found in
525- :cite : `Railway_SW_AdaCore_Web_UG_Native `.
530+ :footcite:p : `Railway_SW_AdaCore_Web_UG_Native `.
526531AdaCore's GNAT project facility, based on a multi-language builder for
527532systems organized into subsystems and libraries, is documented in
528- :cite : `Railway_SW_AdaCore_Web_GPR `.
533+ :footcite:p : `Railway_SW_AdaCore_Web_GPR `.
529534
530535.. index :: single: GNAT Pro Assurance; Configurable Run-Time Libraries
531536
@@ -540,7 +545,7 @@ Configurable Run-Time Libraries
540545
541546Two specific GNAT-defined run-time libraries have been designed with
542547certification in mind and are known as the Certifiable Profiles
543- (see :cite : `Railway_SW_AdaCore_Web_UG_Cross `):
548+ (see :footcite:p : `Railway_SW_AdaCore_Web_UG_Cross `):
544549
545550* *Light Profile *
546551
@@ -823,9 +828,11 @@ GNATcheck provides:
823828* Style checks that allow developers to control indentation, casing,
824829 comment style, and nesting level.
825830
826- AdaCore's :index: `GNATformat ` tool :cite: `Railway_SW_AdaCore_Web_GNATformat `, which
831+ AdaCore's :index: `GNATformat ` tool
832+ :footcite:p: `Railway_SW_AdaCore_Web_GNATformat `, which
827833formats Ada source code according to the GNAT coding style
828- :cite: `Railway_SW_AdaCore_Coding_Style `, can help avoid having code that violates
834+ :footcite:p: `Railway_SW_AdaCore_Coding_Style `,
835+ can help avoid having code that violates
829836GNATcheck rules. GNATformat is included in the GNAT Pro for Ada toolchain.
830837
831838GNATcheck comes with a query language (LKQL, for Language Kit Query Language)
@@ -869,7 +876,8 @@ Principle) that can be used to demonstrate consistency of class hierarchies.
869876Testing a private subprogram is outside the scope of GNATtest but can be
870877implemented by defining the relevant testing code in a private child of the
871878package that declares the private subprogram.
872- Additionally, hybrid verification can help (see :ref: `Railway_SW_Hybrid_Verification `):
879+ Additionally, hybrid verification can help (see
880+ :ref: `Railway_SW_Hybrid_Verification `):
873881augmenting testing with the use of SPARK to formally prove relevant properties
874882of the private subprogram.
875883
@@ -1005,7 +1013,8 @@ Critical fixes to GNAT Pro for Rust are upstreamed to the Rust community,
10051013and critical fixes made by the community to upstream Rust tools are backported
10061014as needed to the GNAT Pro for Rust code base.
10071015Additionally, the Assurance edition of GNAT Pro for Rust includes the
1008- "sustained branch" service (see :ref: `Railway_SW_Sustained_Branches `) that strikes the
1016+ "sustained branch" service (see :ref: `Railway_SW_Sustained_Branches `) that
1017+ strikes the
10091018balance between tool stability and project flexibility.
10101019
10111020.. index :: Integrated Development Environments (IDEs)
0 commit comments