使软件符合人脸标准并完全可移植：Ada的编码指南

降低军事生命周期成本的FACE（未来机载能力环境）方法基于在不同平台和机载系统中重用软件组件。FACE技术标准通过参考架构和数据模型，定义明确的接口以及广泛使用的基础行业标准（IDL，Posix，ARINC-653）解决了这个问题。

符合FACE ［未来机载能力环境］要求是重用和软件可移植性的必要条件，但完整的源代码可移植性意味着比使用一组通用接口更重要。为了使符合 FACE 的软件组件（称为一致性单元或 UoC）完全可移植，它应该在不同的平台和/或编译器实现中具有等效的行为。但是，FACE技术标准中提到的每种编程语言（C，C++，Ada和Java）都具有其影响可能取决于编译器实现或目标平台的功能。用这些语言中的任何一种编写完全可移植的 UoC 都涉及避免潜在的实现依赖关系。在无法实现完全可移植性的情况下，例如，如果存在固有的目标依赖项，则软件结构应封装此类依赖项。

Ada 在软件工程支持和程序可靠性方面对 FACE UoC 开发人员具有很强的优势，它旨在促进完全可移植代码的开发，但即使是 Ada 也具有实现依赖性的功能。本文介绍了应用程序开发人员如何使用 Ada 或其形式上可分析的 SPARK 子集来实现 FACE UoC 的完全可移植性，特别是对于 FACE 技术标准中定义的安全或安保功能集/配置文件。

功能便携性

可移植性，或者这里所说的功能可移植性，以区别于FACE一致性意义上的可移植性，从早期开始就是编程语言设计的目标。理想情况下，功能可移植性意味着可以在一个平台上编译和运行源程序，然后，可能使用不同供应商的编译器，可以在同一平台或不同平台上成功编译和运行同一程序，并具有等效的效果。（“等效”非正式地意味着程序具有相同的外部影响，但允许的时间差异除外。实时程序对于允许哪些时序差异的概念有限 - 即，它的一些时序约束是必不可少的 - 因为错过截止日期可能意味着程序无法满足其要求。然而，在实践中，一些障碍可能会干扰功能可移植性。这些可以包括：使用非标准的语言功能（即特定编译器供应商独有的语言功能），或者标准但可选且并非由所有编译器实现的语言功能;使用语义定义不精确的标准语言特征;以及对目标平台特征的依赖性。

以下内容将提供有关 Ada 功能可移植性的指导，涵盖 Ada 95 和 Ada 2012，重点介绍 FACE 技术标准版 3.0 或更高版本的安保和安全功能集允许的功能。如果适用，该指南显示了如何使用 SPARK Ada 子集来缓解潜在的不可移植性。（除非另有说明，否则语言名称“Ada”是指 Ada 95 和 Ada 2012。本指南并非详尽无遗的清单;Ada 参考手册是关于哪些功能可以产生与实现相关的效果的权威信息来源。

语言扩展

为了防止供应商“锁定”非标准扩展，Ada 编译器的认证策略从一开始就包含“无超集”指令。但是，该策略始终承认供应商特定功能的效用，前提是不引入新语法，从而允许某些类型的语言扩展;特别是，实现定义的库、编译指示、属性、编译指示限制的参数以及（对于 Ada 2012）方面。

FACE 安全扩展和安全基础与安保功能集在这方面施加了一些限制，但不会限制此类语言扩展。为了便于移植，应尽量减少使用实现定义的语言扩展。Ada 2012 明确支持通过编译指示限制的参数来强制缺少实现定义的扩展;例如，No_Implementation_Pragmas和No_Implementation_Units。

可选功能

功能可移植性的另一个障碍是使用并非所有编译器都支持的标准功能。Ada 的认证策略通过禁止子集来解决此问题：每个 Ada 编译器都必须实现完整的语言。然而，导致Ada 95的修订过程承认，特定领域具有专门的（有时是相互冲突的）要求，因此，在编译器认证方面，一些附件（“特殊需要”附件）是可选的。编译器必须实现完整的“核心”语言，包括预定义的环境（标准库）和跨语言接口设施，但系统编程、实时系统、分布式系统、数字、信息系统和安全与安保附件是可选的。

在实践中，这种可选性并不是一个问题，因为最常用的附件 - 系统编程和实时系统 - 由Ada生态系统中的供应商支持。此外，Ada 的 FACE 安全和安保功能集禁止分布式系统、数字和信息系统附件，因此它们的可选性与功能可移植性无关。尽管如此，系统编程和实时附件提出了一些可能影响FACE UoC开发人员的问题：

这些附件中定义并由 FACE 安全和安保功能集允许的某些服务本质上依赖于系统（例如，中断处理），因此在移植到不同的执行环境时需要修订。设计应用程序以封装此类依赖项将简化移植工作。

FACE安全和安保功能集极大地限制了这些附件提供的功能。UoC 开发人员需要通过静态分析或代码审查/检查来证明未使用这些附件中禁止的功能。

具有与实现相关的语义的功能指南

功能可移植性需要明确定义的语义，以便源程序对编译它的每个平台具有等效的效果。但是，在实践中，有时会在精确定义的语义和高效的运行时性能之间进行权衡。由于效率通常是程序员的关键要求，因此语言标准（包括 Ada）包含的功能在不同实现中效果可能有所不同。

表达式中的求值顺序

为了便于优化，Ada 不指定包含算术表达式的项的计算顺序，但在某些情况下，效果取决于编译器选择的顺序。缓解此问题的一种方法是识别有潜在问题的实例（通过检查或静态分析），并通过将表达式重写为计算中间结果的赋值语句序列来使顺序具有确定性。或者，通过使用 SPARK Ada 子集可以完全消除潜在的不可移植性：诸如禁止函数中的副作用之类的限制可确保表达式的值相同，而不管编译器选择的计算顺序如何。

参数传递

Ada 中子程序的形式参数是根据数据流的方向指定的：

“in”，从调用方到被叫子程序

“out”，当子程序返回时，从被调用的子程序返回到调用方

“IN out”，从调用方到被调用子程序，然后在子程序返回时从被调用子程序返回到调用方

编译器选择是通过复制还是通过引用传递参数。对于某些类型的类型（特别是标量类型和访问类型（“指针”），参数传递的语义是通过复制进行的。对于其他一些类型的类型，语义是通过引用的。但是对于不属于这些类别的类型，编译器可以选择任一策略，通常使用类型的对象大小作为条件。如果每个对象的大小小于某个阈值，则使用复制，否则将按引用。

潜在的功能可移植性问题是子程序的效果可能取决于编译器的选择。这可以通过“别名”（例如，全局变量作为参数传递给子程序，并且也从子程序赋值）或异常处理（从子程序分配正式的“out”或“in out”参数，但在子程序返回之前传播异常）来实现。

可以通过多种方式缓解这些与实现相关的影响。通过确保全局变量不作为参数传递给可分配给变量的子程序，可以避免混叠问题。违规可以通过代码审查/检查或静态分析工具检测到，并在 SPARK（禁止此类混叠）中得到阻止。

异常传播问题可以通过适当的编程方式来避免：将任何对形式参数的赋值推迟到可以确保不会发生异常传播之后。SPARK 完全避免了此问题，因为证明工具可以证明不存在运行时异常。

对未初始化变量的引用

Ada 语言允许在不初始化的情况下声明变量。普遍要求初始化将是有问题的：合理的初始值可能不存在，或者程序逻辑可能需要在系统启动时由外部输入提供初始化。更微妙的是，默认初始化可能会导致难以检测的编程错误，其中需要显式初始化的变量被过早引用，从而产生对变量类型有效但不正确的默认初始化。

在初始化变量之前引用变量是编程错误。在没有保证值的情况下，Ada 语义使此类引用的效果保持未定义。确保变量在引用之前被初始化超出了 FACE 安全和安保功能集中的限制范围，因此需要通过其他方式强制执行。

几个 Ada 语言功能可以提供帮助：

某些类型需要默认初始化。特别是当在没有显式初始化的情况下声明访问值（指针）时，它将被设置为特殊值 null。尝试取消引用空值引发异常

程序员可以为记录字段定义默认初始值

在 Ada 2012 中，任何标量类型都可以定义默认初始值

在实践中，Ada 编译器在许多情况下会检测到对其他类型的未初始化变量的引用，尤其是在使用复杂流分析的更高优化级别。静态分析工具也可以解决这个问题，同时最大限度地减少“误报”。与本节中讨论的所有其他潜在的不可移植性一样，SPARK 中完全禁止引用未初始化的变量，因为它们将被 SPARK 证明工具检测到。

并发

Ada 具有强大且高级的并发模型，但为了支持广泛的目标环境，该语言允许许多调度策略决策由实现确定。Ravenscar配置文件缓解了这种非确定性，Ravenscar配置文件是Ada任务功能的一个简单，确定性和有效的子集。FACE Safety-Extended 和 Safety-Base & Security 功能集都将 Ada 任务工具限制为 Ravenscar 子集，从而避免了完整任务模型的功能可移植性问题。（在 FACE 技术标准 3.0 版的 Ada 95 以及 3.1 版的 Ada 95 和 Ada 2012 的安全功能集中允许使用 Ravenscar 功能。

Ravenscar子集由SPARK支持，因此SPARK程序将避免完整Ada任务模型的非确定性。

细化顺序

Ada 程序通常由主子程序以及主子程序直接或间接依赖的模块（“包”）组成。程序执行首先在各种依赖包中执行运行时代码（例如初始化全局数据） - 称为“包细化” - 然后调用主子程序。包的详细说明顺序部分受语言语义的约束，但通常依赖于实现，不同的顺序可能会产生不同的结果。实现依赖性是语言语义所固有的，因为任何完全指定详细说明顺序的尝试也会禁止有用的情况，例如相互依赖的包。

有几种技术可以帮助确保可移植性：

添加适当的编译指示以约束详细说明顺序（有关示例，请参见图 1）或

通过将所有这些代码移动到在主子程序开始时显式调用的过程中，避免依赖包中的细化时代码

［图1 |细化顺序。

通过使用 SPARK 也可以避免细化顺序非确定性，因为 SPARK 限制确保所有细化顺序具有相同的效果。

目标依赖项指南

System.* 包层次结构和表示子句：尽管低级编程涉及访问特定于目标的特征，但 Ada 通过标准语言功能有助于减少不可移植性。包 System 声明类型地址和相关操作，子包System.Storage_Elements和System.Address_To_Access_Conversions提供用于处理“原始存储”和将指针视为物理地址的标准工具，反之亦然。表示子句允许程序定义程序实体的低级属性，例如记录的布局或变量的地址。这些功能由人脸安全和安保功能集允许。尽管它们的用法是特定于平台的，但将此类代码封装在包的主体中将进行本地化，并有助于最大限度地减少将代码移植到新目标平台时所需的适应。

数值类型表示：Ada 中预定义的数值类型（整数、浮点数等）具有实现定义的范围/精度。如果程序员隐式假定 Integer 等类型始终具有某个最小范围，则这种情况可能会导致功能可移植性问题;当将代码移植到 Integer 范围较窄的平台时，算术表达式可能会溢出并引发异常。

可以通过声明自定义数值类型而不是使用预定义类型来避免潜在的不可移植性。图 2 显示了一个示例。

［图2 |便携式数字类型。

遵循使用模式

编写完全可移植的代码不仅需要 FACE 一致性，还需要功能可移植性。这意味着遵循适当的使用模式，特别是对于语义未完全由语言标准定义的功能。

一般来说，Ada 是一种对功能可移植性有强大支持的语言，多年来，系统现代化已经成功地将大型 Ada 程序移植到新硬件和新的编译器实现中。尽管如此，功能可移植性不会自动到来，必须进行规划;开发人员应避免使用依赖于实现的语言功能，或者采取适当的缓解措施。这对于需要遵守 FACE 安全和安保功能集/配置文件之一的应用程序尤其重要。此类应用程序具有很强的保证要求，如果代码使用未精确定义的语言功能，则很难演示这些要求。Ada 的 SPARK 子集特别相关，因为 SPARK 语言限制确保了确定性语义。

简而言之，为Ada采用适当的风格约定（其中大部分可以通过静态分析工具（如AdaCore的CodePeer或GNATcheck）或使用SPARK可以帮助开发人员实现其FACE兼容软件的完全可移植性，同时实现Ada和SPARK带来的保证优势。

审核编辑：郭婷