8. Software Unit Verification Checklists

This section provides two verification checklists that are to be used to provide evidence of correct execution of this process for each software unit. The two verification checklists are:

The Verification Checklist for Software Unit Requirements is expected to be incorporated (e.g., by reference) into the corresponding Verification Specification for those software unit requirements (see ISO 26262-6:2018, 6.4.7). The development of that Verification Specification is out of the scope of this process. This process only covers software requirements specification at all because this process introduces the practice of incorporating software unit requirements into the public parts of external ADS files for purposes of enabling formal specification and verification of software unit requirements.

Note: An organization may consider the software unit requirements to be part of the software architectural design, in which case the software architectural design Verification Specification would be the particular Verification Specification that would need to incorporate the Verification Checklist for Software Unit Requirements.

The Verification Checklist for Software Unit Design and Implementation is expected to be incorporated by reference into the Software Unit Verification Specification work product described in this process.

Note: Each checklist question must be usable by:

• reviewers on the software unit development team,

• confirmation reviewers, and

• assessors.

Separate checklists are not provided for each of these stakeholders because the same checklist questions apply to all three of these roles. Where expectations are different for the different roles, the checklist row calls out the specific differences in the roles in answering the checklist question.

If multiple reviewers are completing checklists for the same software interface or software unit, reviewers cannot share a checklist among one another; each review must complete a checklist separately. Except where specified otherwise, any non-zero number of reviewers is sufficient as long as no fragment of the software interface or software unit was authored by all the reviewers (every fragment must have at least one reviewer who is not the author, as is required by local peer reviews).

It is the intent of this process that confirmation reviewers and assessors use the same checklist as reviewers. Other checklists that were not developed with formal verification in mind are likely to underemphasize areas that are of primary concern where formal verification is used and are likely to overemphasize areas that are of lesser concern where formal verification is used.

Checklist items are color-coded according to what situations they apply to:

• Checklist items with a light-green background apply to every software interface and software unit developed according to this process.

• Checklist items with a light-blue background apply to every software interface and software unit developed according to this process except for SPARK Platinum software interfaces and clean SPARK Platinum software units (see the Terminology section).

• Checklist items with a light-red background apply to any software unit developed according to this process that does not enable SPARK_Mode throughout the entirety of the unit or that skips proof for part or all of the unit.

• Checklist rows with a gray background identify activities for which no manual verification of compliance is needed.

Checklist item numbers are suffixed with either (A) indicating that it is expected to be automatable through other processes and tools or (M) indicating that manual verification is inherently required.

In order to complete these checklists, the reviewer needs access to:

• The software unit requirements.

• The software unit files (e.g., GPR, ADC, ADS, and ADB files).

• The precise commands executed per this process and the corresponding console output, exit statuses, and output file contents recorded in the Software Unit Verification Report.

8.1. Verification Checklist for Software Unit Requirements

The Verification Checklist for Software Unit Requirements consists of the following parts:

• Per-software-unit checklist

• Per-software-interface checklist

8.1.1. Per-Software-Unit Checklist

Complete this once per Ada software unit.

Checklist item 1.1.1 (automatable)

Identify_External_Packages

Up to and including SPARK Platinum

For each software interface provided or used by the Ada software unit (as determined by the software architectural design), does the software interface specification clearly indicate whether or not the software interface is expected to be specified per this process (in the form of ADS files)?

Rationale: To start off, we need to identify which software interface specifications to verify with this process.

Checklist item 1.1.2 (automatable)

Identify_External_Packages .. Verify_Requirement_Necessity

Up to and including SPARK Platinum

For each software interface identified in checklist question 1 as being specified per this process (in the form of ADS files), did the developers complete an instance of the per-software-interface checklist in the next section, where that instance covers the software interface?

Note: Multiple software interfaces can be covered by the same completed per-software-interface checklist.

Rationale: The developers must complete the checklist for each software interface.

8.1.2. Per-Software-Interface Checklist

Every software interface identified in checklist question 1 in the per-software-unit checklist must be covered by exactly one of the following per-software-interface checklists. It is acceptable to cover multiple software interfaces with the same per-software-interface checklist as long as each person completing the checklist gives full consideration to all the software interfaces within the scope of the checklist.

Checklist question 1 in this checklist asks for what software interfaces are covered by the particular checklist. Every subsequent question in this checklist must only be answered “Yes” if the answer is “Yes” for each and every software interface identified in the answer to checklist question 1.

Checklist item 1.1.3 (automatable)

Identify_External_Packages

Up to and including SPARK Platinum

Is this instance of this checklist clearly associated with the set of software interfaces to be verified using this checklist?

Checklist item 1.1.4 (automatable)

Identify_External_Packages

Up to and including SPARK Platinum

Does the software interface specification clearly indicate all the non-nested packages whose package specifications will specify the software interface?

Checklist item 1.1.5 (automatable)

Identify_External_Packages

Up to and including SPARK Platinum

For each non-nested package identified in response to checklist question 1.1.4, does the software interface specification clearly indicate:

• Whether the package specification to be specified in an ADS file…

  • must be implemented, or

  • consists of public specification only.

• For each of the packages to be implemented:

  • Whether the package specification is allowed to have a private part.

  • Whether the package is to be implemented by

    • (typically) each provider of the software interface, or

    • (rarely) each user of the software interface?

Checklist item 1.1.6 (automatable)

Identify_External_Packages

Up to and including SPARK Platinum

For each child package that must be implemented by the provider or user software unit(s), is each proper ancestor of that package (the parent package and their recursive parents, if any) that is allowed to have a private part either

• to be implemented by the same software unit, or

• not to be implemented by any software unit?

Checklist item 1.2.1 (automatable)

Create_External_ADS

Up to and including SPARK Platinum

For each non-nested package identified in response to checklist question 1.1.4, is there a corresponding ADS file named according to the naming convention specified in the Create External ADS step?

Checklist item 1.2.2 (automatable)

Create_External_ADS

Up to and including SPARK Platinum

For each non-nested package identified in response to checklist question 1.1.4, if the package specification has a private part, then does the software interface specification allow the package specification to have a private part?

Checklist item 1.3.1

Declare_SPARK_Package

N/A - Fully automated

During the Compile Project step, the compiler will verify that the correct package is declared in each external ADS file.

Checklist item 1.4.1

Identify_Dependencies

N/A - Fully automated

During the Compile Project step, the compiler will verify that all necessary dependencies are with’d by each external ADS file.

Checklist item 1.5.1 (automatable/manual)

Declare_Types_States_And_Subprograms

Up to and including SPARK Platinum

Is each type, constant, variable, and subprogram declaration in the public part of each external ADS file necessary, i.e., does each such declaration satisfy at least one of the following conditions?

• The declared entity is intended to be referenced directly by providers and/or users of the interface.

• The declared entity is referenced by another declaration within the public part of an external ADS file of the interface, where the latter declaration is recursively necessary by these criteria.

Note: Automation could be used to support this, by identifying declarations that are not referenced by the interface or the software units. Review could then be focused on evaluating whether those declarations are necessary.

Checklist item 1.6.1

Capture_Requirements

N/A - Fully automated

During the Verify Requirement Correctness, Completeness and Adherence to Ada/SPARK Guidelines step and during unit design and implementation, the completeness of the captured requirements is verified.

Checklist item 1.6.2 (manual)

Capture_Requirements

Up to and including SPARK Platinum

Is each formal requirement preceded by a comment that explains the requirement in natural language?

Note: Multiple formal requirements can be preceded by a single comment that explains them all.

Checklist item 1.6.3 (automatable)

Capture_Requirements

Up to and including SPARK Platinum

Does each declaration in an external ADS file have the Ghost aspect if the declaration is only used in formal requirements?

Checklist item 1.6.4 (manual)

Capture_Requirements

Up to and including SPARK Gold

Is each ASIL C and ASIL D non-formal requirement in the software interface specification expressed in some form of semi-formal notation (e.g., EARS)?

Checklist item 1.6.5 (manual)

Capture_Requirements

Up to and including SPARK Gold

Is each non-formal requirement in the software interface specification unambiguous (that is, lending itself to a single interpretation) and free from internal contradictions?

Checklist item 1.6.6 (manual)

Capture_Requirements

Up to and including SPARK Gold

Is each non-formal requirement in the software interface specification implementation free (see the Terminology section)?

Checklist item 1.6.7 (manual)

Capture_Requirements

Up to and including SPARK Gold

Is each non-formal safety requirement in the software interface specification atomic, to the extent that this is reasonably possible without interfering with compliance with other items in this checklist?

Checklist item 1.7.1 (automatable)

Assign_Requirement_Unique_IDs

Up to and including SPARK Platinum

Does each of the following requirements in the public parts of the interface’s ADS files have its own unique ID as described in the Traceability Model section?

• Non-formal type/subprogram/package contracts

• Formal type contracts

  • Scalar constraints

    • range constraints

    • digits constraints

    • delta constraints

  • Composite constraints

    • Index constraints

    • Discriminant constraints

  • Null exclusions

  • Type predicates

  • Default initial conditions

• Formal subprogram-only contracts

  • Top-level and’ed conditions of:

    • Preconditions

      • Pre aspects

      • Pre’Class aspects

    • Postconditions

      • Post aspects

      • Post’Class aspects

      • Refined_Post aspects

    • Cases of Contract_Cases aspects

    • Global aspects

    • Depends aspects (or each dependency_clause thereof, at the developers’ discretion)

    • No_Return aspects

  • Formal subprogram/package contracts

    • Forward_Progress user aspects

    • Always_Terminates aspects

    • Local_Restrictions (No_Secondary_Stack, No_Heap_Allocations) aspects

Checklist item 1.7.2 (automatable/manual)

Assign_Requirement_Unique_IDs

Up to and including SPARK Platinum

For each requirement in the software interface specification that has a unique ID, does the requirement trace to all the non-unit-level work product fragments (if any) that directly motivate the requirement?

Note: Automation of this checklist item would require formalization of all non-unit-level work products capable of motivating requirements in the software interface specification.

Checklist item 1.8.1

Verify_Formal_Requirement_Consistency

N/A - Fully automated

During the Compile Project and Verify Project steps, the commands specified in this step will be re-executed, but with more strict criteria for passing verification than what is required by the Verify Formal Requirement Consistency step.

Checklist item 1.9.1 (manual)

Verify_Non_Formal_Requirement_Consistency

Up to and including SPARK Gold

Does each of the non-formal requirements in the software interface specification have both of the following properties?

• Consistent with all other requirements (formal and non-formal) in the software interface specification

• Does not duplicate content from any other requirements (formal and non-formal) in the software interface specification

Checklist item 1.10.1 (manual)

Verify_Requirement_Correctness_And_Completeness

Up to and including SPARK Platinum

Is the entirety of the software interface specification out-of-context comprehensible (see the Terminology section)?

Checklist item 1.10.2 (manual)

Verify_Requirement_Correctness_And_Completeness

Up to and including SPARK Platinum

Does the entirety of the public parts of the ADS files fully observe the fragments of the Ada/SPARK Guidelines identified therein as manually enforced?

Checklist item 1.10.3 (automatable/manual)

Verify_Requirement_Correctness_And_Completeness

Up to and including SPARK Platinum

Are the requirements in the software interface correct and complete with respect to the non-unit-level work products, and is this completeness supported by traceability? (Does each non-unit-level work product fragment that constrains the software interface trace to requirements in the software interface that are correct and complete with respect to that non-unit-level work product fragment?)

Note: Automation of this checklist item would require formalization of all non-unit-level work products capable of motivating requirements in the software interface specification.

Checklist item 1.11.1 (automatable)

Verify_Requirement_Necessity

Up to and including SPARK Platinum

For each requirement in the software interface specification that has a unique ID, is at least one of the following true?

1. The requirement traces to at least one work product fragment that motivates the requirement.

2. The requirement is a formal requirement on a package, subprogram, or type that is leveraged by a proven subprogram.

Note: It is typically necessary to defer this checklist question until after the completion of the software unit designs of the software units that provide or use this software interface. For example, the Document Design Solutions For Non-Formally-Verified Unit Specification Fragments step of this process can create trace links from requirements to unit design decisions that motivate those requirements.

Checklist item 1.12.1 (manual)

(All)

Up to and including SPARK Platinum

What is the PASS/FAIL outcome of software interface verification?

Note: Only enter PASS if the answers to all earlier questions is “Yes”.

8.2. Verification Checklists for Software Unit Design and Implementation

Complete each of the checklists in this section once per Ada software unit developed according to this process.

8.2.1. Verification Checklist for Software Unit Design

Complete this once per Ada software unit.

Checklist item 2.1.1 (automatable)

Identify_Activity_Scope

Up to and including SPARK Platinum

Does the software unit have a corresponding Software Unit Verification Plan work product that states that the software unit is verified according to this process and that the verification plan for the software unit includes everything stated in this process concerning verification planning?

Checklist item 2.1.2 (automatable)

Identify_Activity_Scope

Up to and including SPARK Platinum

Consult the software architectural design’s list of software interfaces to be provided/used by the software unit, and consult the corresponding software interface specifications. Does the Software Unit Verification Plan correctly identify the set of external non-nested packages that the software unit must implement, and the corresponding ADS file name for each such package per the GNAT default file naming scheme?

Checklist item 2.1.3 (automatable)

Identify_Activity_Scope

Up to and including SPARK Platinum

If the software unit has a corresponding Software Unit Verification Specification work product, does that Software Unit Verification Specification include the software unit within its scope, reference the software unit’s Software Unit Verification Plan, and state that the verification specification for the software unit includes everything stated in this process concerning verification specification?

Checklist item 2.1.4 (manual)

Identify_Activity_Scope

Up to and including SPARK Platinum

If the software unit interacts with third-party safety-related software components, are all applicable constraints from third-party-supplied safety manuals captured as unit requirements?

Checklist item 2.1.5 (manual)

Identify_Activity_Scope

Up to and including SPARK Platinum

If the software unit interacts with hardware, are all applicable constraints from hardware/software interface specifications captured as unit requirements?

Checklist item 2.1.6 (manual)

Identify_Activity_Scope

Up to and including SPARK Platinum

If the software unit is safety-related, are the safety measures resulting from safety-oriented analyses captured as unit requirements?

Checklist item 2.2.1 (automatable)

Create_Project_File

Up to and including SPARK Platinum

Is the set of unit GPR files, and the GPR files they directly or indirectly depend on via project with keywords, clearly identifiable for the software unit?

Checklist item 2.2.2 (automatable)

Create_Project_File

Up to and including SPARK Platinum

Does each unit GPR file (combined with any other GPR files recursively included via with keywords) do all the following?

• Set attributes Runtime ("Ada"), Target, and Builder'Global_Configuration_Pragmas, with values that satisfy the restrictions specified by the Create Project File step

• Refrain from including a Naming package

Checklist item 2.2.3 (automatable)

Create_Project_File

Up to and including SPARK Platinum

Does each unit GPR file (combined with any other GPR files recursively included via with keywords) include a Compiler package that specifies switches that comply with all the following?

• The Requirements Concerning Compiler Warning Switches section

• The Requirements Concerning Non-Warning-Related Compiler Switches section

• Any restrictions in the Ada/SPARK Guidelines concerning style checking switches

Checklist item 2.2.4 (automatable)

Create_Project_File

Up to and including SPARK Platinum

Does each unit GPR file (combined with any other GPR files recursively included via with keywords) with a Prove package refrain from specifying any GNATprove switches prohibited by the Requirements Concerning GNATprove Switches section?

Checklist item 2.2.5 (automatable)

Create_Project_File

Up to and including SPARK Platinum

Does each unit GPR file (combined with any other GPR files recursively included via with keywords) with a Check package refrain from specifying any GNATcheck switches prohibited by the Requirements Concerning GNATcheck Switches and Rules section?

Checklist item 2.2.6 (automatable)

Create_Project_File

Up to and including SPARK Platinum

Does each unit GPR file (combined with any other GPR files recursively included via with keywords) avoid all non-safety-qualified tool switches in the Compiler, Prove, and Check packages?

Checklist item 2.3.1 (automatable)

Create_Configuration_Pragmas

Up to and including SPARK Platinum

For each unit GPR file (combined with any other GPR files recursively included via with keywords), does the ADC file specified by the Builder’Global_Configuration_Pragmas attribute contain the exact definition of the Forward_Progress user aspect specified in the Create Configuration Pragmas step?

(Note: There is a bug relating to this in the 24.1 tools that is fixed in the 24.2 tools; this rule does not apply in this case.)

Checklist item 2.4.1 (automatable)

Identify_Internal_Packages

Up to and including SPARK Platinum

Does the Software Unit Verification Plan clearly identify what internal non-nested packages are part of the software unit, and the corresponding ADS file name for each such package per the GNAT default file naming scheme?

Checklist item 2.4.2 (automatable)

Identify_Internal_Packages

Up to and including SPARK Platinum

For each external interface package that is an ancestor of any internal package identified as part of the software unit, if the external interface package is not implemented by the software unit, is it part of a software interface specification that forbids the external interface package from having a private part?

Checklist item 2.5.1 (automatable)

Create_Internal_ADS

Up to and including SPARK Platinum

For each internal package identified in the Software Unit Verification Plan, is the corresponding internal ADS file included in at least one of the unit GPR files (whether it is included directly or via the containing directory)?

Checklist item 2.6.1 (automatable/manual)

Declare_Internal_Types_States_And_Subprograms

Up to and including SPARK Gold

For each software interface the software unit provides or uses, for each code fragment of the software interface specification that is not part of an ADS file but expresses a responsibility of the software unit, does the software unit design include one or more equivalent Ada declarations?

Note: For software units that do not provide any non-ADS software interfaces, this checklist item can be satisfied with automation. For other software units, manual verification is required.

Checklist item 2.6.2

Declare_Internal_Types_States_And_Subprograms

N/A - Fully automated

During the Write Tests step, the sufficiency of the unit design to justify all the unit test cases is verified.

Checklist item 2.7.1

Capture_Unit_Design_Constraints

N/A - Fully automated

During the Inspect Unit Design step, the sufficiency of the unit design constraints and documentation fragments to satisfy all non-formally-verified unit specification fragments is verified.

Checklist item 2.7.2 (manual)

Capture_Unit_Design_Constraints

Up to and including SPARK Gold

Does each non-formally-verified unit design constraint have its own unique ID as described in the Traceability Model section?

Note: It is also acceptable to assign unique IDs to all unit design constraints, whether formally-verified or not.

Checklist item 2.7.3 (manual)

Capture_Unit_Design_Constraints

Up to and including SPARK Gold

For each formally-verified unit design constraint that supports one or more non-formally-verified unit specification fragments, does the formally-verified unit design constraint have its own unique ID as described in the Traceability Model section?

Note: It is also acceptable to assign unique IDs to all unit design constraints, whether formally-verified or not.

Checklist item 2.8.1 (manual)

Document_Design_Solutions

Up to and including SPARK Gold

Does each design documentation fragment in an ADS or ADB file have its own unique ID as described in the Traceability Model section?

Checklist item 2.8.2 (manual)

Document_Design_Solutions

Up to and including SPARK Gold

Is each design documentation fragment not in an ADS or ADB file documented in accordance with the Ada/SPARK Process Binding?

Checklist item 2.8.3 (manual)

Document_Design_Solutions

Up to and including SPARK Gold

If the cleanliness-adjusted ASIL of the software unit is ASIL C or ASIL D, for each design documentation fragment that describes control flow or data flow between more than three entities, is the control flow or data flow specified using semi-formal or formal notation with the methods and syntax required by the Ada/SPARK Process Binding?

Checklist item 2.8.4 (manual)

Capture_Unit_Design_Constraints, Document_Design_Solutions

Up to and including SPARK Gold

Does each software unit design fragment trace to each non-formally-verified software unit specification fragment it directly supports?

Checklist item 2.8.5 (manual)

Document_Design_Solutions

Up to and including SPARK Gold

Does each software unit design documentation fragment trace (e.g., by name) to each subprogram it directly depends on?

Checklist item 2.8.6

Document_Design_Solutions

N/A - Fully automated

During the Inspect Unit Design step, the sufficiency of the unit design constraints and documentation fragments to satisfy all non-formally-verified unit specification fragments is verified.

Checklist item 2.9.1 (manual)

Inspect_Unit_Design

Up to and including SPARK Gold

Is the unit design (including internal types, states, and subprograms, unit design constraints, and design documentation fragments) free of contradictions with all the non-formally-verified unit requirements?

Note: This verifies that the unit design is correct with respect to the non-formally-verified unit requirements. No analogous inspection is required for formally-verified unit requirements, because in the Verify Project step, GNATprove will be used to verify the unit design is correct with respect to the formally-verified unit requirements.

Checklist item 2.9.2 (manual)

Inspect_Unit_Design

Up to and including SPARK Gold

For each non-formally-verified unit specification fragment, is the set of supporting unit design fragments and/or unit requirements (as determined via trace links) sufficiently comprehensive that a test developer can determine the PASS/FAIL criteria for each test case without consulting the implementation, considering the structural coverage obligations associated with the cleanliness-adjusted ASIL of the unit?

Note: This verifies that the unit design is complete with respect to the non-formally-verified requirements. No analogous inspection is required for formally-verified unit requirements, because in the Verify Project step, GNATprove will be used to verify the unit design is complete with respect to the formally-verified unit requirements.

Checklist item 2.9.3 (manual)

Inspect_Unit_Design

Up to and including SPARK Gold

Is each non-formally-verified unit design constraint and documentation fragment consistent with the rest of the unit design?

Note: No analogous inspection of internal consistency is required between two formally-verified unit design constraints, because in the Verify Project step, GNATprove will be used to verify that all the formally-verified unit design constraints are consistent with one another.

Checklist item 2.9.4 (manual)

Inspect_Unit_Design

Up to and including SPARK Gold

Is each unit design constraint and each unit design documentation fragment necessary to support the unit requirements or the rest of the unit design?

Checklist item 2.9.5 (manual)

Inspect_Unit_Design

Up to and including SPARK Platinum

Does the entirety of the unit design fully observe the fragments of the Ada/SPARK Guidelines identified therein as manually enforced?

Checklist item 2.9.6 (manual)

Inspect_Unit_Design

Up to and including SPARK Platinum

Is the unit design in-context-comprehensible (see the Terminology section)?

Checklist item 2.9.7 (manual)

Inspect_Unit_Design

Up to and including SPARK Gold

If the cleanliness-adjusted ASIL of the unit is ASIL C or ASIL D, for each design documentation fragment that describes control flow or data flow between more than three entities, was control flow and data flow analysis performed in accordance with the Ada/SPARK Process Binding and did the analysis yield a passing result?

Checklist item 2.9.8 (manual)

Inspect_Unit_Design

Up to and including SPARK Platinum

For each with clause in the unit’s internal ADS files, is the referenced package either an internal package of the unit or an external package of a software interface that per the software architectural design is provided/used by the software unit?

Checklist item 2.9.9 (manual)

Inspect_Unit_Design

Up to and including SPARK Gold

If the unit supports different states, do the unit requirements, unit design constraints, and unit design documentation fragments collectively specify those states and the state transitions?

Checklist item 2.9.10 (manual)

Inspect_Unit_Design

Up to and including SPARK Gold

Do the unit requirements, unit design constraints, and unit design documentation fragments collectively specify the error handling responsibilities of the unit?

Checklist item 2.9.11 (manual)

Inspect_Unit_Design

Up to and including SPARK Gold

Do the unit requirements, unit design constraints, and unit design documentation fragments collectively specify the timing and concurrency-related responsibilities of the unit?

Checklist item 2.10.1

Verify_Unit_Design

N/A - Fully automated

During the Verify Project step, GNATprove will be re-executed, but with more strict criteria for passing verification than what is required by the Verify Unit Design step.

Checklist item 2.11.1 (manual)

(All)

Up to and including SPARK Platinum

What is the PASS/FAIL outcome of unit design verification?

Note: Only enter PASS if the answers to all earlier questions is “Yes”.

8.2.2. Verification Checklist for Software Unit Implementation and Verification

Complete this once per Ada software unit.

Checklist item 3.1.1 (automatable)

Create_ADB

Up to and including SPARK Platinum

For each non-nested package implemented by the unit, does the Software Unit Verification Plan correctly indicate whether the package requires a package body and, if so, the corresponding ADB file name per the GNAT default file naming scheme?

Checklist item 3.1.2 (automatable)

Create_ADB

Up to and including SPARK Platinum

For each non-nested package implemented by the unit which requires a package body, is the corresponding ADB file included in at least one of the unit GPR files (whether it is included directly or via the containing directory)?

Checklist item 3.2.1

Define_SPARK_Package

N/A - Fully automated

During the Compile Project step, the compiler will verify that the correct package body is declared in each ADB file.

Checklist item 3.3.1

Implement_SPARK_Package

N/A - Fully automated

During the Compile Project step, the compiler will verify that each ADB file completes all the declarations left incomplete by the corresponding ADS file, and you will verify that the project compiles without errors or warnings.

Checklist item 3.3.2

Implement_SPARK_Package

N/A - Fully automated

During the Verify Project step, GNATprove will formally verify the project.

Checklist item 3.3.3

Implement_SPARK_Package

N/A - Fully automated

During the Review Deactivated SPARK step, reviewers will verify compliance with all the requirements of the Non-SPARK Ada subsection.

Checklist item 3.3.4

Implement_SPARK_Package

N/A - Fully automated

During the Review Diagnostic Justifications step, reviewers will verify the compliance with all the requirements of the Diagnostic Justifications subsection.

Checklist item 3.4.1 (automatable)

Compile_Project

Up to and including SPARK Platinum

Was the software unit compiled using the gprbuild command specified in the Compile Project step?

Checklist item 3.4.2 (automatable)

Compile_Project

Up to and including SPARK Platinum

Did the software unit compile without errors, warnings, or style messages? (Alternatively, did gprbuild exit with a zero exit status?)

Checklist item 4.1.1 (automatable)

Develop_Unit_Verification_Plan

Up to and including SPARK Platinum

Does the Software Unit Verification Plan indicate (whether directly or indirectly) the versions of the ADS and ADB files that are being verified as suitable for release?

Note: The ADS and ADB files to be verified were already recorded in the Identify Activity Scope, Identify Internal Packages, and Create ADB steps.

Checklist item 4.1.2 (manual)

Develop_Unit_Verification_Plan

Up to and including SPARK Platinum

Does the Software Unit Verification Plan specify the objectives of verification, and do these objectives include the four objectives from ISO 26262-6:2018, 9.1 (duplicated below for the reviewer’s convenience)?

1. to provide evidence that the software unit design satisfies the allocated software requirements and is suitable for the implementation;

2. to verify that the defined safety measures resulting from safety-oriented analyses in accordance with 7.4.10 and 7.4.11 are properly implemented;

3. to provide evidence that the implemented software unit complies with the unit design and fulfills the allocated software requirements with the required ASIL; and

4. to provide sufficient evidence that the software unit contains neither undesired functionalities nor undesired properties regarding functional safety.

Checklist item 4.1.3 (manual)

Develop_Unit_Verification_Plan

Up to and including SPARK Platinum

Does the Software Unit Verification Plan indicate that the verification methods, the verification pass/fail criteria, the verification environment, and some of the verification tools are defined in this document (the SPARK-Based ISO 26262 Safety Process for Vehicle Software), including the particular version of this document that was used?

Checklist item 4.1.4 (manual)

Develop_Unit_Verification_Plan

Up to and including SPARK Platinum

Does the Software Unit Verification Plan identify the tools and equipment that will be used to automate verification checklist rows marked automatable (A), for those rows (if any) that will be automated?

Note: This process does not require the automation of verification checklist rows marked automatable (A).

Checklist item 4.1.5 (manual)

Develop_Unit_Verification_Plan

Up to and including SPARK Platinum

Does the Software Unit Verification Plan identify the resources (person-days of people with various skills, time slots on shared equipment…) required for verification, and to the best of the knowledge of the reviewer, are those resources sufficient to complete all the verification activities specified in the Software Unit Verification Plan?

Checklist item 4.1.6 (manual)

Develop_Unit_Verification_Plan

Up to and including SPARK Platinum

Does the Software Unit Verification Plan identify the actions to be taken if anomalies are detected during verification and the incremental re-verification required after changes to the software unit design and/or implementation?

Checklist item 4.2.1 (automatable)

Verify_Project

Up to and including SPARK Platinum

Was GNATprove invoked with the gnatprove command line described in the Verify Project step?

Checklist item 4.2.2 (automatable)

Verify_Project

Up to and including SPARK Platinum

Did GNATprove report zero warnings, zero errors, and zero high/medium/low check messages? (Alternatively, did gnatprove exit with a zero exit status?)

Checklist item 4.2.3 (automatable)

Verify_Project

Up to and including SPARK Platinum

Do the switches on the gnatprove command line refrain from using any switches prohibited by the Requirements Concerning GNATprove Switches section?

Checklist item 4.2.4 (automatable)

Verify_Project

Up to and including SPARK Platinum

Does the combination of switches in the Prove package in the unit GPR file and the switches on the gnatprove command line collectively include all the switches required by the Requirements Concerning GNATprove Switches section?

Checklist item 4.3.1 (automatable)

Automated_Check_Against_Coding_Std

Up to and including SPARK Platinum

Was GNATcheck invoked with the gnatcheck command line described in the Automated Check Against Coding Standard and Safety Manual step?

Checklist item 4.3.2 (automatable)

Automated_Check_Against_Coding_Std

Up to and including SPARK Platinum

Do the switches on the gnatcheck command line refrain from using any switches prohibited by the Requirements Concerning GNATcheck Switches and Rules section?

Checklist item 4.3.3 (automatable)

Automated_Check_Against_Coding_Std

Up to and including SPARK Platinum

Does the combination of switches in the Check package in the unit GPR file and the switches on the gnatcheck command line collectively include all the switches and enable all the rules required by the Requirements Concerning GNATcheck Switches and Rules section?

Checklist item 4.3.4 (automatable)

Automated_Check_Against_Coding_Std

Up to and including SPARK Platinum

Does the combination of switches in the Check package in the unit GPR file and the switches on the gnatcheck command line collectively enable all the rules required by the Ada/SPARK Guidelines?

Checklist item 4.3.5 (automatable)

Automated_Check_Against_Coding_Std

Up to and including SPARK Platinum

Was GNATkp invoked with the gnatkp command line described in the Automated Check Against Coding Standard and Safety Manual step and with the --kp-version switch set to the correct GNAT tools version?

Checklist item 4.4.1 (automatable)

Fix_Coding_Std_Issues

Up to and including SPARK Platinum

Did GNATcheck and GNATkp collectively report no warnings, no coding standard violations, and no safety manual violations?

Checklist item 4.5.1 (manual)

Static_Analysis_Unit

Interfaces and units containing Ada

Does the CodePeer command line enable medium/high messages for all non-proven code in the software unit?

Checklist item 4.5.2 (automatable)

Static_Analysis_Unit

Interfaces and units containing Ada

Did CodePeer output zero diagnostics?

Checklist item 4.6.1 (automatable)

Check_Stack_Usage_Unit

Up to and including SPARK Platinum

Was GNATstack invoked using the gnatstack command line specified in the Check Stack Usage (Unit) step?

Checklist item 4.6.2 (automatable)

Check_Stack_Usage_Unit

Up to and including SPARK Platinum

For each subprogram whose stack frame size is greater than five times the median subprogram stack frame size, does the software unit design identify the subprogram by name as potentially requiring a large amount of stack space, does the software unit design specify a numerical upper bound for the subprogram’s stack frame size, and is the subprogram’s actual stack frame size less than or equal to that threshold?

Checklist item 4.6.3 (automatable)

Check_Stack_Usage_Unit

Up to and including SPARK Platinum

For each subprogram whose stack frame size is variable, does the software unit design identify the subprogram by name as potentially requiring a variable-length stack frame?

Checklist item 4.7.1 (manual)

Review_Diagnostic_Justifications

Up to and including SPARK Gold

Was the Diagnostic Justifications Verification Worksheet completed with a global peer review, and were zero issues identified in it?

Checklist item 4.8.1 (manual)

Review_Deactivated_SPARK

Interfaces and units containing Ada

Was the Non-Proven Ada Worksheet completed, and were zero issues identified in it?

Checklist item 4.9.1 (manual)

Manual_Check_Against_Safety_Manuals

Up to and including SPARK Platinum

Review all the safety manuals identified in the Manual Check Against Safety Manuals step. For each usage constraint in each of the safety manuals, if the usage constraint is not checked by gnatkp and not checked by GNATcheck rule Ada_2022_Outside_Of_Contracts, does the software unit and the usage of the GNAT tools for this process comply with the usage constraint?

Checklist item 4.10.1 (manual)

Inspect_Implementation

Up to and including SPARK Platinum

Was the Code Inspection Worksheet completed, and were zero issues identified in it?

Checklist item 4.11.1 (automatable)

Write_Tests

Up to and including SPARK Platinum

Does each test case in an ADS or ADB file have its own unique ID as described in the Traceability Model section?

Checklist item 4.11.2 (manual)

Write_Tests

Up to and including SPARK Gold

Aside from test cases that merely instantiate generic test cases, does each test case trace to one or more unit specification fragments that collectively justify all the PASS/FAIL criteria of the test case?

Rationale: Aside from test cases that merely instantiate generic test cases, test cases must not be derived from unit implementation.

Checklist item 4.11.3 (manual)

Write_Tests

Up to and including SPARK Gold

Does each test case include documentation of the equivalence classes and boundary values covered by the test case?

Checklist item 4.11.4 (automatable)

Write_Tests

Up to and including SPARK Gold

Are test cases for generic packages and subprograms themselves generic, and do the generic test cases have the exact same sequence of generic formal parameters as the generic packages and subprograms they test?

Checklist item 4.11.5 (automatable)

Write_Tests

Up to and including SPARK Gold

Do the test cases collectively instantiate all the generic test cases for the software unit?

Checklist item 4.11.6 (automatable)

Write_Tests

Up to and including SPARK Platinum

Do the test cases collectively instantiate and invoke all the generic test cases corresponding to generic packages and subprogram instantiations in the software unit, with the same generic actual parameters?

Checklist item 4.11.7 (automatable)

Write_Tests

Interfaces and units containing Ada

For each generic instantiation in the software unit, if any part of the generic package or subprogram uses a higher level of SPARK than the instantiation site in the software unit, is there a SPARK_Mode => On non-proof-skipping test case that instantiates the generic package or subprogram with the same generic actual parameters, and does the test case documentation clearly indicate that this test case must be proven during verification?

Checklist item 4.12.1 (manual)

Review_Tests

Up to and including SPARK Gold

Does each non-formally-verified unit requirement, each non-formally-verified unit design constraint, and each non-formally-verified unit design documentation fragment trace to test cases that collectively verify all the specified properties and behaviors and collectively cover all the equivalence classes and boundary values evident from the specification?

Checklist item 4.12.2 (manual)

Review_Tests

Up to and including SPARK Gold

Does each diagnostic justification and each uniquely-identified check suppression trace to test cases that collectively verify that the diagnostic justification or check suppression is correct (not masking a bug) and collectively cover all the equivalence classes and boundary values evident in the supplied justification?

Checklist item 4.12.3

Review_Tests

N/A - Fully automated

The other bullets of Review Tests are covered by the checklist items for Write Tests.

Checklist item 4.13.1 (automatable)

Formally_Verify_Test_Cases

Up to and including SPARK Gold

If any test cases are documented as requiring proof, then was GNATprove GNATprove invoked with the gnatprove command line described in the Formally Verify Test Cases step?

Checklist item 4.13.2 (automatable)

Formally_Verify_Test_Cases

Up to and including SPARK Gold

Did GNATprove report zero warnings, zero errors, and zero high/medium/low check messages? (Alternatively, did gnatprove exit with a zero exit status?)

Checklist item 4.13.3 (automatable)

Formally_Verify_Test_Cases

Up to and including SPARK Gold

Do the switches on the gnatprove command line refrain from using any switches prohibited by the Requirements Concerning GNATprove Switches section?

Checklist item 4.13.4 (automatable)

Formally_Verify_Test_Cases

Up to and including SPARK Gold

Does the combination of switches in the Prove package in the test GPR file and the switches on the gnatprove command line collectively include all the switches required by the Requirements Concerning GNATprove Switches section?

Checklist item 4.14.1 (automatable)

Unit_Test_Run_And_Coverage

Up to and including SPARK Platinum

Were all the unit tests run, and did all the unit tests pass?

Checklist item 4.14.2 (automatable)

Unit_Test_Run_And_Coverage

Up to and including SPARK Gold

If the cleanliness-adjusted ASIL of the unit is not QM, was a tool such as GNATcoverage used to measure the structural coverage of the software unit achieved by the passing unit tests, using the metric corresponding to the cleanliness-adjusted ASIL of the software unit?

• MC/DC coverage for ASIL D

• Decision coverage for ASILs B and C

• Statement coverage for ASIL A

Checklist item 4.15.1 (automatable)

Handle_Coverage_Deviations

Up to and including SPARK Gold

If the cleanliness-adjusted ASIL of the unit is not QM, is each coverage gap identified in the Unit Test Run And Coverage step justified by one of the three justification methods listed in the Handle Coverage Deviations step?

Checklist item 4.16.1 (automatable)

Verify_Dynamic_Assumptions

Up to and including SPARK Platinum

Was the software unit rebuilt with the GPR and ADC file modifications specified in the Verify Dynamic Assumptions step?

Checklist item 4.16.2 (automatable)

Verify_Dynamic_Assumptions

Up to and including SPARK Platinum

Were all the rebuilt unit tests run, and did all the rebuilt unit tests pass, without exceptions being raised during test execution?

Checklist item 4.17.1 (automatable)

Develop_Verification_Report

Up to and including SPARK Platinum

Does the Software Unit Verification Report refer to the Software Unit Verification Plan and Software Unit Verification Specification (or to this process)?

Checklist item 4.17.2 (automatable)

Develop_Verification_Report

Up to and including SPARK Platinum

Does the Software Unit Verification Report identify the specific versions of the files of the software unit that were verified?

Checklist item 4.17.3 (automatable)

Develop_Verification_Report

Up to and including SPARK Platinum

What is the PASS/FAIL outcome of unit verification?

Note: Only enter PASS if the answers to all earlier questions is “Yes”.

8.2.3. Diagnostic Justifications Verification Worksheet

Complete this worksheet if required by the Verification Checklist for Software Unit Implementation and Verification.

This worksheet includes checklist questions related to:

• Non-formally-verified assumptions (a.k.a. GNATprove indirect justifications):

  • pragma Assume (condition, justification);
    

• GNATprove warning suppressions:

  • pragma Warnings (GNATprove, Off, warning,
                     Reason => justification);
    ...
    pragma Warnings (GNATprove, On, warning);
    

  • pragma Warnings (Off, warning, Reason => justification);
    ...
    pragma Warnings (On, warning);
    

• GNATprove direct justifications (a.k.a. GNATprove check message direct justifications):

  • pragma Annotate (GNATprove, False_Positive,
                     check_message,
                     justification);
    

  • pragma Annotate (GNATprove, Intentional,
                     check_message,
                     justification);
    

• GNATcheck rule exemptions:

  • pragma Annotate (GNATcheck, Exempt_On,
                     rule_name,
                     justification);
    ...
    pragma Annotate (GNATcheck, Exempt_Off, rule_name);
    

Worklist item 1.1 (Non-formally-verified assumptions)

Applies to: Up to and including SPARK Gold

Is each pragma Assume’s condition parameter a minimal Boolean expression (does it refrain from expressing properties that have already been proven or which are not needed for any proof)?

Worklist item 1.2 (Non-formally-verified assumptions)

Applies to: Up to and including SPARK Gold

Does each pragma Assume include a justification parameter whose value is a string that provides a justification for why the assumption is valid (why the condition will always be true)?

Note: The justification may also be used to explain challenges that may have led to GNATprove being unable to prove the condition, but this is not required.

Worklist item 1.3 (Non-formally-verified assumptions)

Applies to: Up to and including SPARK Gold

Does each pragma Assume have its own unique ID as described in the Traceability Model section?

Worklist item 2.1 (GNATprove warning suppressions)

Applies to: Up to and including SPARK Gold

Is each GNATprove warning suppression expressed with two pragma Warnings lines with identical warning values, the first with Off and the second with On, that bracket the region of code for which the warning is to be suppressed?

Worklist item 2.2 (GNATprove warning suppressions)

Applies to: Up to and including SPARK Gold

Is each bracketed region of code minimal (is the first pragma Warnings line immediately before the code that causes the warning, and is the second pragma Warnings line immediately after the code that causes the warning)?

Worklist item 2.3 (GNATprove warning suppressions)

Applies to: Up to and including SPARK Gold

Does each pragma Warnings include a warning value long enough to avoid inadvertently suppressing other warnings?

Worklist item 2.4 (GNATprove warning suppressions)

Applies to: Up to and including SPARK Gold

Does the first pragma Warnings line of each pair include a Reason => justification parameter where the justification is a string that provides a justification for why the warning does not mask a bug?

Note: The justification may also be used to explain why the warning occurs, but this is not required.

Worklist item 2.5 (GNATprove warning suppressions)

Applies to: Up to and including SPARK Gold

Does the first pragma Warnings line of each pair have its own unique ID as described in the Traceability Model section?

Worklist item 2.6 (GNATprove warning suppressions)

Applies to: Up to and including SPARK Gold

For each GNATprove warning suppression that suppresses “assumed Always_Terminates” warnings, does the supplied justification explain why the code does not violate GNATprove assumption [PARTIAL_TERMINATION]?

Worklist item 2.7 (GNATprove warning suppressions)

Applies to: Up to and including SPARK Gold

For each GNATprove warning suppression that suppresses “assumed Global null” warnings, does the supplied justification explain why the code does not violate GNATprove assumption [PARTIAL_GLOBAL]?

Worklist item 2.8 (GNATprove warning suppressions)

Applies to: Up to and including SPARK Gold

For each GNATprove warning suppression that suppresses “imprecisely supported address specification” warnings, does the supplied justification explain why the code does not violate GNATprove assumptions [SPARK_EXTERNAL], [SPARK_ALIASING_ADDRESS], and [SPARK_EXTERNAL_VALID]?

Worklist item 3.1 (GNATprove direct justifications)

Applies to: Up to and including SPARK Gold

Does each GNATprove direct justification include a check_message value long enough to avoid inadvertently suppressing other check messages?

Worklist item 3.2 (GNATprove direct justifications)

Applies to: Up to and including SPARK Gold

Does each False_Positive GNATprove direct justification include a justification parameter that is a string that provides a justification for why the error condition identified by the check message will never actually occur?

Note: The justification may also be used to explain why the check message occurs, but this is not required.

Worklist item 3.3 (GNATprove direct justifications)

Applies to: Up to and including SPARK Gold

Does each Intentional GNATprove direct justification include a justification parameter that is a string that provides a justification for why the check message does not mask a bug?

Note: The justification may also be used to explain why the check message occurs, but this is not required.

Worklist item 3.4 (GNATprove direct justifications)

Applies to: Up to and including SPARK Gold

Does each GNATprove direct justification have its own unique ID as described in the Traceability Model section?

Worklist item 4.1 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

Is each GNATcheck rule exemption expressed with two pragma Annotate lines with identical rule_name values, the first with Exempt_On and the second with Exempt_Off, that bracket the region of code for which the rule is to be suppressed?

Worklist item 4.2 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

Is each bracketed region of code minimal (is the first pragma Annotate line immediately before the code that violates the rule, and is the second pragma Annotate line immediately after the code that violates the rule)?

Worklist item 4.3 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

Does the first pragma Annotate line of each pair include a justification parameter where the justification is a string that provides a justification for why the rule violation does not mask a bug and why the code needs to violate the rule?

Worklist item 4.4 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

Does the first pragma Annotate line of each pair have its own unique ID as described in the Traceability Model section?

Worklist item 4.5 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Forbidden_Attributes:Initialized rule in SPARK code, does the supplied justification explain why the code does not violate GNATprove assumption [SPARK_INITIALIZED_ATTRIBUTE]?

Worklist item 4.6 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Restrictions:Max_Protected_Entries=>0 rule in SPARK code, does the protected entry have an informal precondition that prohibits the protected entry from being called (directly or indirectly) from a dispatching call?

Rationale: This facilitates compliance with GNATprove assumption [SPARK_OVERRIDING_AND_TASKING].

Worklist item 4.7 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Restrictions:No_Floating_Point rule in SPARK code, does the supplied justification explain why the code does not violate GNATprove assumption [SPARK_FLOATING_POINT]?

Worklist item 4.8 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Restrictions:No_Protected_Types rule in SPARK code, does the supplied justification explain why the code does not violate GNATprove assumption [SPARK_OVERRIDING_AND_TASKING]?

Worklist item 4.9 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Restrictions:No_Specification_Of_Aspect=>Iterable rule in SPARK code, does the supplied justification explain why the code does not violate GNATprove assumptions [SPARK_ITERABLE] and [SPARK_ITERABLE_FOR_PROOF]?

Worklist item 4.10 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Restrictions:No_Use_Of_Entity=>Ada.Task_Identification.Current_Task rule in SPARK code, does the supplied justification explain why the code does not violate GNATprove assumption [SPARK_OVERRIDING_AND_TASKING]?

Worklist item 4.11 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Forbidden_Attributes:Initialized rule in SPARK code, does the supplied justification explain why the code does not violate GNATprove assumption [SPARK_OVERRIDING_AND_TASKING]?

Worklist item 4.12 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Ada_2022_Outside_Of_Contracts rule, does the supplied justification explain why the violation will not result in unsafe compiler behavior?

Rationale: Ada 2022 compiler features are not qualified for safety.

Worklist item 4.13 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Forbidden_Pragmas:Validity_Checks rule, does the supplied justification explain why the violation will not result in unsafe compiler behavior?

Rationale: pragma Validity_Checks is not qualified for safety.

Worklist item 4.14 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Forbidden_Pragmas:Assertion_Policy rule, does the supplied justification explain why the violation will not result in unsafe compiler behavior?

Rationale: This pragma could be used to enable assertions in production code, assertions can use Ada 2022 features, and Ada 2022 compiler features are not qualified for safety.

Worklist item 4.15 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Forbidden_Pragmas:Ignore_Pragma rule, does the supplied justification explain why the violation will not result in import pragmas (e.g., SPARK_Mode) being ignored?

Worklist item 4.16 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Metrics_Cyclomatic_Complexity:10 rule in non-proven code, does the supplied justification explain why the increased complexity does not mask a bug, and is the non-proven code in-context-comprehensible to the reviewer in spite of the elevated complexity?

Worklist item 4.17 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Procedures_Without_Globals rule in SPARK code, does the supplied justification explain why the absence of Global contracts does not mask unintended behavior?

Worklist item 4.18 (GNATcheck rule exemptions)

Applies to: Up to and including SPARK Gold

For each GNATcheck rule exemption that disables the Goto_Statements:Only_Unconditional rule, does the supplied justification explain why the conditional goto does not mask a bug?

8.2.4. Non-Proven Ada Worksheet

Complete this worksheet if required by the Verification Checklist for Software Unit Implementation and Verification.

In completing this worksheet, consider all non-proven code, and only answer “yes” to a checklist question if the answer is “yes” for all the non-proven code:

• Code with no explicit SPARK_Mode aspect or pragma

• Code for which the innermost relevant SPARK_Mode aspect or pragma set SPARK_Mode to Off

• Code with the Annotate => (GNATprove, Skip_Proof) aspect

• Code with the Annotate => (GNATprove, Skip_Flow_And_Proof) aspect

Worklist item 1.1 (Justification and Scope)

Applies to: Interfaces and units containing Ada

For each compilation unit that has neither a SPARK_Mode aspect with default value nor a SPARK_Mode => On aspect, is there a comment justifying the decision to disable SPARK for the entire compilation unit?

Worklist item 1.2 (Justification and Scope)

Applies to: Interfaces and units containing Ada

Is each aspect or pragma that disables SPARK_Mode and each Annotate => (GNATprove, Skip_Proof) or Annotate => (GNATprove, Skip_Flow_And_Proof) annotation preceded with a comment justifying the decision to disable SPARK, reduce the SPARK level to Bronze, or reduce the SPARK level to Stone, respectively?

Worklist item 1.3 (Justification and Scope)

Applies to: Interfaces and units containing Ada

For each justification for disabling SPARK, proof, or flow and proof, is the scope of the disabling minimized? (Is all code that should have SPARK, proof, or flow and proof enabled, respectively, outside the range of code for which it is disabled?)

Worklist item 2.1 (Packages)

Applies to: Interfaces and units containing Ada

For each package specification and each package body that is at least partly non-proven, does the package must comply with all parts of GNATprove assumption [ADA_ELABORATION]?

Worklist item 2.2 (Packages)

Applies to: Interfaces and units containing Ada

For each private part of a package specification and each package body that is at least partly non-proven, does the private part of package body comply with all parts of GNATprove assumptions [ADA_EXTERNAL_ABSTRACT_STATE] and [ADA_STATE_ABSTRACTION]?

Worklist item 3.1 (Data and Types)

Applies to: Interfaces and units containing Ada

For each global variable accessed by non-proven code, is there a comment justifying the usage of a global variable? (ISO 26262-6:2018, Table 6, row 1e)

Worklist item 3.2 (Data and Types)

Applies to: Interfaces and units containing Ada

For each object shared between non-proven code and proven SPARK code, does the non-proven code comply with GNATprove assumptions [ADA_EXTERNAL] and [ADA_EXTERNAL_NAME]?

Worklist item 3.3 (Data and Types)

Applies to: Interfaces and units containing Ada

For each type completion in non-proven code for a type that was declared in proven SPARK code, does the completion comply with all parts of GNATprove assumption [ADA_PRIVATE_TYPES]?

Worklist item 3.4 (Data and Types)

Applies to: Interfaces and units containing Ada

For each type defined by non-proven code as an extension of a type declared in proven SPARK code, does the type definition comply with GNATprove assumption [ADA_TAGGED_TYPES]?

Worklist item 3.5 (Data and Types)

Applies to: Interfaces and units containing Ada

For each value assigned by non-proven code to an object of recursive type, does the value comply with GNATprove assumption [ADA_RECURSIVE_TYPES]?

Worklist item 4.1 (Subprograms)

Applies to: Interfaces and units containing Ada

For each non-proven subprogram called from proven SPARK code, does the subprogram comply with all parts of GNATprove assumption [ADA_SUBPROGRAMS], [ADA_OBJECT_ADDRESSES], [ADA_LOGICAL_EQUAL], and [ADA_INLINE_FOR_PROOF]?

Worklist item 4.2 (Subprograms)

Applies to: Interfaces and units containing Ada

For each call from non-proven code to a subprogram with a proven body, does the call comply with all parts of GNATprove assumption [ADA_CALLS]?

Worklist item 4.3 (Subprograms)

Applies to: Interfaces and units containing Ada

For each non-proven subprogram whose declaration is annotated with the No_Heap_Allocations or No_Secondary_Stack local restriction (whether directly, or indirectly via a Forward_Progress user aspect), does the subprogram and all subprograms called from it (whether directly or indirectly) refrain from heap allocations or secondary stack allocations, respectively?

Worklist item 4.4 (Subprograms)

Applies to: Interfaces and units containing Ada

For each call from non-proven code, does the caller either consume all the outputs and return values or explicitly discard them, and are all documented error cases handled by the caller? (ISO 26262-6:2018 8.4.5f)

Worklist item 5.1 (Pragmas)

Applies to: Interfaces and units containing Ada

Is all non-proven code contained within pragma Unsuppress (All_Checks) regions?

Worklist item 5.2 (Pragmas)

Applies to: Interfaces and units containing Ada

For each check suppression (i.e., pragma Suppress, pragma Suppress_All, or pragma Assertion_Policy with the Ignore parameter) in ASIL C or ASIL D non-proven code, does the non-proven code include comparable defensive checks to compensate for the disabled language-defined checks and test-time assertions?

Worklist item 5.3 (Pragmas)

Applies to: Interfaces and units containing Ada

For each check suppression in non-proven code, if the non-proven code does not include comparable defensive checks to compensate for the disabled language-defined checks and test-time assertions, does the check suppression have its own unique ID as described in the Traceability Model section?

8.2.5. Code Inspection Worksheet

Complete the code inspection worksheet once per unit. Here, the “code” of a software unit includes all the contents of the ADS/ADB files, including software unit design.

Worklist item 1.1 (Comprehensibility)

Applies to: Up to and including SPARK Platinum

Is all of the code in-context-comprehensible to the reviewer?

Worklist item 1.2 (Comprehensibility)

Applies to: Up to and including SPARK Platinum

Does all the code fully observe the fragments of the Ada/SPARK Guidelines identified therein as manually enforced?

Worklist item 1.3 (Comprehensibility)

Applies to: Up to and including SPARK Platinum

Does the code use symbolic names for constants where appropriate (instead of hard-coding constants in the code)?

Worklist item 1.4 (Comprehensibility)

Applies to: Up to and including SPARK Platinum

Are all the comments in the code consistent with the code itself?

Worklist item 1.5 (Comprehensibility)

Applies to: Up to and including SPARK Platinum

In the reviewer’s estimation, are there sufficient code comments to enable the review to efficiently comprehend the code?

Worklist item 1.6 (Comprehensibility)

Applies to: Up to and including SPARK Platinum

Given the complexity of the unit’s requirements, and in the reviewer’s estimation, is the code not unreasonably difficult to verify against the requirements and design?

Worklist item 2.1 (Correctness)

Applies to: Up to and including SPARK Gold

Does the code limit itself to the behavior and properties specified in the unit requirements and unit design?

Worklist item 2.2 (Correctness)

Applies to: Up to and including SPARK Gold

Does the code limit its use of with to package specifications that are within the scope of the unit (external packages of interface specifications provided/used by the software unit and internal packages of the unit itself)?

Worklist item 2.3 (Correctness)

Applies to: Up to and including SPARK Gold

Does each subprogram in the code satisfy all the non-formally-verified unit requirements imposed on the subprogram, all the non-formally-verified unit design constraints imposed on the subprogram, and all the claims made in unit design documentation fragments concerning the subprogram?

Worklist item 2.4 (Correctness)

Applies to: Up to and including SPARK Gold

Has the reviewer approached the code from the perspective of assuming the code has bugs until the reviewer confirms otherwise?

Worklist item 2.5 (Correctness)

Applies to: Up to and including SPARK Gold

Has the reviewer thoroughly studied all the software unit requirements and software unit files (especially ADS and ADB file) and been unable to find any bugs in the code?

Worklist item 2.6 (Correctness)

Applies to: Up to and including SPARK Gold

Are all assumptions made by the code captured as unit requirements or unit design fragments?

Worklist item 3.1 (Robustness)

Applies to: Up to and including SPARK Gold

Does each subprogram perform plausibility checks to ensure that input parameters comply with non-formal preconditions?

Worklist item 3.2 (Robustness)

Applies to: Up to and including SPARK Gold

For each subprogram not marked Forward_Progress, Always_Terminates, or No_Return, do all loops and recursions terminate?

Worklist item 3.3 (Robustness)

Applies to: Interfaces and units containing Ada

For each call to a subprogram that can raise an exception, does the caller handle the possible exceptions?