降低軍事生命周期成本的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帶來的保證優勢。

審核編輯：郭婷