Editorial: comprehensive typo and grammar pass over all learn.adacore.com content

content/about.rst

@@ -7,15 +7,15 @@
 About learn.adacore.com
 ==========================
 
-Learn.adacore.com is an interactive learning platform designed to teach the Ada and SPARK programming languages. With courses featuring hands-on labs and easy to understand code snippets, you will have the opportunity to see, understand and experiment with the language capabilities.
+Learn.adacore.com is an interactive learning platform designed to teach the Ada and SPARK programming languages. With courses featuring hands-on labs and easy-to-understand code snippets, you will have the opportunity to see, understand and experiment with the language capabilities.
 
 .. rubric:: About Ada/SPARK
 
 
 The Ada programming language was designed from its inception to be used in applications where safety and security are of the utmost importance. Its feature set and programming paradigms, by design, allow software developers to develop applications more effectively and efficiently. It encourages a “think first, code later” principle which produces more readable, reliable, and maintainable software.
 
-The SPARK programming language is a formally verifiable subset of the Ada language which allows developers to mathematically prove program correctness through static means. This is accomplished by exploiting the strengths of the Ada syntax while eliminating the features of the language that introduce ambiguity and non-deterministic behavior. The language put together with a verification toolset and a design methodology ensures the development and deployment of low-defect software for high reliability applications.
+The SPARK programming language is a formally verifiable subset of the Ada language which allows developers to mathematically prove program correctness through static means. This is accomplished by exploiting the strengths of the Ada syntax while eliminating the features of the language that introduce ambiguity and non-deterministic behavior. The language put together with a verification toolset and a design methodology ensures the development and deployment of low-defect software for high-reliability applications.
 
 .. rubric:: About AdaCore
 
-Founded in 1994, AdaCore is the leading provider of commercial and open-source software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore is committed to being an active member of the software development community providing the GNAT Ada compiler and SPARK formal methods technologies as open-source projects to the world to advocate their use in the future of safe and reliable computing. Visit the AdaCore `website <https://www.adacore.com>`_ for more information.
+Founded in 1994, AdaCore is the leading provider of commercial and open-source software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore is committed to being an active member of the software development community, providing the GNAT Ada compiler and SPARK formal methods technologies as open-source projects to the world to advocate their use in the future of safe and reliable computing. Visit the AdaCore `website <https://www.adacore.com>`_ for more information.

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

@@ -162,7 +162,7 @@ maintainability, and to detect errors early in the software
 development process. This section will summarize several Ada features
 that help meet these goals.
 
-.. index:: single: Ada language; Modulatization
+.. index:: single: Ada language; Modularization
 .. index:: single: Ada language; Information hiding
 .. index:: single: Ada language; Packages
 .. index:: single: Ada language; Programming in the large
@@ -410,7 +410,7 @@ object.  To deallocate an allocated object, it is necessary to
 instantiate the generic procedure :ada:`Ada.Unchecked_Deallocation`;
 the result is the definition of procedure :ada:`Free`.  The sample
 code allocates an initialized heap object and subsequently frees its
-storage
+storage.
 
 As another example, here's a C code fragment that performs pointer
 arithmetic:
@@ -660,7 +660,7 @@ be specified informally by comments:
 
 They can also be captured more formally as `aspects` of the procedure
 specification (an aspect is a technical feature that specifies a
-property of program entity) if the SPARK subset of Ada is used, as
+property of a program entity) if the SPARK subset of Ada is used, as
 will be explained below.
 
 .. index:: single: Ada language; Interface / implementation separation
@@ -911,7 +911,7 @@ correctly on both little-endian and big-endian hardware.
     with
        Bit_Order            => System.Low_Order_First,
        Scalar_Storage_Order => System.Low_Order_First,
-          -- Scalar_Storage_Order is a GNAT-specifc aspect
+          -- Scalar_Storage_Order is a GNAT-specific aspect
        Size                 => 32, -- Bits
        Alignment            => 4;  -- Storage units
 
@@ -1226,7 +1226,7 @@ possible activities:
   raise the :ada:`Assertion_Error` exception. After testing and
   related verification activities achieve sufficient assurance that no
   violations will occur, the checking code can be removed (either by
-  :ada:`pragma Asserion_Policy(Ignore)` or by compiling without
+  :ada:`pragma Assertion_Policy(Ignore)` or by compiling without
   |gnata|).
 * **Enabling dynamic checks during testing, and keeping them in the
   final executable object code**. In this case, the software
@@ -1559,7 +1559,7 @@ Approach 1: Test cases are not specified in Ada specifications
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 A traditional approach can be followed by GNATtest |mdash| that is to
-say, tests cases are described outside of the Ada specification, but
+say, test cases are described outside of the Ada specification, but
 linked to a particular function. When working this way, GNATtest will
 generate one test per subprogram; for example :
 
@@ -1838,7 +1838,7 @@ implementation of one or several requirements, and a single test with
 all three conditions :ada:`True` will almost certainly fail to satisfy the
 requirement coverage criterion. Further, this single test is probably
 not sufficient to detect implementation errors: the purpose of testing
-is to detect errors and to show that the software satisifes its
+is to detect errors and to show that the software satisfies its
 requirements, not to achieve structural code coverage.  Structural
 coverage analysis is mainly a test completeness activity.
 
@@ -2541,7 +2541,7 @@ an exception would be raised.)  The type :ada:`Jet` is not
 substitutable for the type :ada:`Aircraft` on invocations of
 :ada:`Open_Doors`.
 
-The non-substitutabiity is reflected in the use of the specific aspect
+The non-substitutability is reflected in the use of the specific aspect
 :ada:`Pre` rather than the class-wide aspect :ada:`Pre'Class`. In a
 type hierarchy rooted at type :ada:`T` where :ada:`Pre'Class` is
 specified at each level for a subprogram :ada:`Proc`, the effective
@@ -2781,7 +2781,7 @@ than the precondition on :ada:`Open_Doors` for :ada:`Aircraft`. But
     * The postcondition for :ada:`Take_Off(Aircraft)` is strengthened
       by :ada:`Jet`
 
-Whether it is easier to demonstrate local versus global suitability
+Whether it is easier to demonstrate local versus global substitutability
 for a given class depends on the architecture and the ease of
 identification of actual dispatch destinations and
 substitutability. |do-332| allows the applicant to decide on whichever
@@ -2840,7 +2840,7 @@ be made by dispatching from this call. All objectives that apply to
 control and data coupling now apply to type derivation coupling, in
 particular the coverage objectives. Whether or not testing with all
 possible derivations in the system is used (i.e., pessimistic testing)
-depends of the strategy chosen for substitutability demonstration.
+depends on the strategy chosen for substitutability demonstration.
 
 .. index:: single: DO-332/ED-217: Object-Oriented Technology and
            Related Techniques; Memory management issues
@@ -3031,7 +3031,7 @@ several reasons:
   correspond to violations of preconditions, and such violations
   should not occur in verified code.
 * Since the normal control flow has been abandoned, the program may be
-  in an instable state (for example with aggregate data structures not
+  in an unstable state (for example with aggregate data structures not
   fully updated) and writing an appropriate handler can be difficult.
 
 |do-332| specifies that exception handling needs to be taken into
@@ -3881,7 +3881,7 @@ check the contents of a flash zone:
 
 .. index:: DO-333/ED-216: Formal Methods
 
-The Low-Level Requirments comprise a textual description and a set of
+The Low-Level Requirements comprise a textual description and a set of
 formal properties.  The textual description appears in |do-333| and is
 not repeated here.  The formal properties of the :ada:`A1F2_TestZone`
 procedure are of three kinds:
@@ -4062,7 +4062,7 @@ correctness of the overall system."
   and discrepancies explained
 * Table FM.A-6, Objective 3: Executable object code complies with
   low-level requirements
-* Table FM.A-6, Objective 4: Executable object code is tobust with
+* Table FM.A-6, Objective 4: Executable object code is robust with
   low-level requirements
 * Table FM.A-7, Objective FM 4: Coverage of low-level requirements is
   achieved

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

@@ -6,7 +6,7 @@ Introduction
 This document explains how to use AdaCore's technologies |mdash| the
 company's tools, run-time libraries, and associated services |mdash|
 in conjunction with the safety-related standards for airborne
-software: |do-178c| and and its technology supplements and tool
+software: |do-178c| and its technology supplements and tool
 qualification considerations. It describes how AdaCore's technologies
 fit into a project's software life cycle processes, and how they can
 satisfy various objectives of the standards.  Many of the advantages
@@ -100,7 +100,7 @@ objectives for one project (determined by the development standards,
 the input complexity, the target computer and system environment) but
 not necessarily on another project. The effort and amount of
 justification to gain approval may also differ from one auditor to
-another, depending of their background. Whenever a new tool, method,
+another, depending on their background. Whenever a new tool, method,
 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

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

@@ -125,7 +125,7 @@ but might fail to detect an error) to TQL-1 (the highest, applicable
 to software tools that can insert an error in software at level A).
 
 A tool is only qualified in the context of a specific project, for a
-specific certification credit, expressed in term of objectives and
+specific certification credit, expressed in terms of objectives and
 activities. Achieving qualification for a tool on a specific project
 does of course greatly increase the likelihood of being able to
 qualify the tool on another project. However, a different project may
@@ -172,7 +172,7 @@ do not relate directly to the issues addressed in this supplement.
 Object-Oriented Technology and Related Techniques Supplement: DO-332/ED-217
 ------------------------------------------------------------------------------
 
-Although |do-332| is often referred as the "object oriented
+Although |do-332| is often referred to as the "object oriented
 supplement", the "related techniques" mentioned in the title are
 equally relevant and are addressed in detail. They may be used in
 conjunction with Object-Oriented Technology (OOT) but are not

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

@@ -99,7 +99,7 @@ solutions can reduce the effort in meeting some of these objectives.
    Objective, Summary, Activities, "Use case #1a", "Use case #1b (OOT)", "Use case #2"
    1, "The activities of the software life cycle processes are defined", All, "This document describes possible methods and tools that may be used. When an AdaCore solution is adopted, it should be documented in the  plans.", Same as #1a, Same as #1a
    2, "The software life cycle(s), including the inter-relationships between the processes, their sequencing, and transition criteria, is defined.", All, "A variety of software life cycles may be defined (such as V cycle, Incremental, Iterative, and Agile). AdaCore solutions do not require any specific software life cycle.", Same as #1a, Same as #1a
-   3, "Software life cycle environment is selected and defined", "4.4.1.a, 4.4.1.f, 4.4.2.b, 4.4.3.a, 4.4.3.b", "When an AdaCore solution is used, the plans should identify and escribe the associated tools. In particular, see :ref:`Airborn_SW_Sustained_Branches` and :ref:`Airborn_SW_Compiling_with_the_GNAT_Pro_compiler`", Same as #1a, Same as #1a
+   3, "Software life cycle environment is selected and defined", "4.4.1.a, 4.4.1.f, 4.4.2.b, 4.4.3.a, 4.4.3.b", "When an AdaCore solution is used, the plans should identify and describe the associated tools. In particular, see :ref:`Airborn_SW_Sustained_Branches` and :ref:`Airborn_SW_Compiling_with_the_GNAT_Pro_compiler`", Same as #1a, Same as #1a
    4, "Additional considerations are addressed", "4.2.j, 4.2.k", "The need for tool qualification is addressed throughout this document.", "Same as #1a", "Same as #1a"
    5, "Software development standards are defined.", "4.2.b, 4.5.b, 4.5.c, 4.5.d", "This document describes possible languages, methods and tools that may be used during the design and coding processes. When any of them are used, design and code standards must be developed accordingly. A Code Standard can be defined through :ref:`Airborn_SW_GNATcheck`", "Same as #1a", "Same as #1a"
    6, "Software plans comply with this document.", All, "This objective is satisfied through the review and analysis of the plans and standards.", "Same as #1a", "Same as #1a"

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

@@ -117,7 +117,7 @@ contracts the developer can formalize the intended behavior of the
 application, and can verify this behavior by testing, static analysis
 or formal proof.
 
-Here's a skeletal example that illustrates contact-based programming;
+Here's a skeletal example that illustrates contract-based programming;
 a :ada:`Table` object is a fixed-length container for distinct
 :ada:`Float` values.
 
@@ -278,7 +278,7 @@ memory safety; this is illustrated by a number of features, including:
 
   A run-time check guarantees that an array index is within the bounds
   of the array.  This prevents buffer overflow vulnerabilities that
-  are common in C and C++.  In many cases a a compiler optimization
+  are common in C and C++.  In many cases a compiler optimization
   can detect statically that the index is within bounds and thus
   eliminate any run-time code for the check.
 
@@ -290,7 +290,7 @@ memory safety; this is illustrated by a number of features, including:
 
 * Prevention of dangling references
 
-  A scope accessibility checks ensures that a pointer cannot reference
+  A scope accessibility check ensures that a pointer cannot reference
   an object on the stack after exit/return from the scope (block or
   subprogram) in which the object is declared. Such checks are
   generally static, with no run-time overhead.
@@ -772,7 +772,7 @@ standard as a set of rules, for example a subset of permitted language
 features. It verifies a program's conformance with the resulting rules
 and thereby facilitates demonstration of a system's compliance with
 Table A-5, Objective 4 of |do-178c| ("Source Code conforms to
-standards"). GNATcheck providess:
+standards"). GNATcheck provides:
 
 * An integrated `Ada Restrictions` mechanism for banning specific
   features from an application. This can be used to restrict features
@@ -799,7 +799,7 @@ standards"). GNATcheck providess:
 AdaCore's :index:`GNATformat` tool, which formats Ada source code
 according to the `GNAT coding style
 <https://gcc.gnu.org/onlinedocs/gnat-style.pdf>`_, can help avoid
-having code that violates GNATcheck rules
+having code that violates GNATcheck rules.
 
 GNATcheck comes with a query language (called LKQL) that lets
 developers define their own checks for any in-house rules that need to

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

@@ -10,7 +10,7 @@ EN 50128 governs software used in railway control and protection applications,
 i.e., systems that ensure the safe and efficient movement of trains.
 Examples include:
 
-* *Automatic Train Protection (ATP)*, which ensure automatic braking to avoid
+* *Automatic Train Protection (ATP)*, which ensures automatic braking to avoid
   collisions or overspeed;
 
 * *Interlocking Systems*, which prevent conflicting train movements through
@@ -22,10 +22,10 @@ Examples include:
 * *Level Crossing Protection*, which manages gates and warnings at road-rail
   intersections; and
 
-* *Centralized Traffic Control (CTC)*, which oversee train routing and
+* *Centralized Traffic Control (CTC)*, which oversees train routing and
   dispatch across large regions.
 
-The goal of the standard is to provide confidence that that the software
+The goal of the standard is to provide confidence that the software
 functions reliably and safely relative to its SIL. To this end it
 specifies requirements in areas including the following:
 
@@ -168,7 +168,7 @@ Clause 7, *Generic software development*, has the following sub-clauses:
 * Component design (sub-clause 7.4);
 * Component implementation and testing (sub-clause 7.5);
 * Integration (sub-clause 7.6); and
-* Overall Software Testing / Final Validation (sub-class 7.7).
+* Overall Software Testing / Final Validation (sub-clause 7.7).
 
 .. index:: single: EN 50128; Clause 8 (Development of application data or algorithms)
 

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

@@ -239,7 +239,7 @@ The following technologies will be presented:
 
   - GNAT Studio |mdash| a robust, flexible, and extensible IDE
   - VS Code support |mdash| extensions for Ada and SPARK
-  - GNATbench |mdash| an Ada-knowlegeable Eclipse plug-in
+  - GNATbench |mdash| an Ada-knowledgeable Eclipse plug-in
   - GNATdashboard |mdash| a metric integration and management platform
 
 .. _Railway_SW_fig2: