降低軍事生命周期成本的FACE（未來(lái)機(jī)載能力環(huán)境）方法基于在不同平臺(tái)和機(jī)載系統(tǒng)中重用軟件組件。FACE技術(shù)標(biāo)準(zhǔn)通過(guò)參考架構(gòu)和數(shù)據(jù)模型，定義明確的接口以及廣泛使用的基礎(chǔ)行業(yè)標(biāo)準(zhǔn)（IDL，Posix，ARINC-653）解決了這個(gè)問(wèn)題。

符合FACE ［未來(lái)機(jī)載能力環(huán)境］要求是重用和軟件可移植性的必要條件，但完整的源代碼可移植性意味著比使用一組通用接口更重要。為了使符合 FACE 的軟件組件（稱(chēng)為一致性單元或 UoC）完全可移植，它應(yīng)該在不同的平臺(tái)和/或編譯器實(shí)現(xiàn)中具有等效的行為。但是，F(xiàn)ACE技術(shù)標(biāo)準(zhǔn)中提到的每種編程語(yǔ)言（C，C++，Ada和Java）都具有其影響可能取決于編譯器實(shí)現(xiàn)或目標(biāo)平臺(tái)的功能。用這些語(yǔ)言中的任何一種編寫(xiě)完全可移植的 UoC 都涉及避免潛在的實(shí)現(xiàn)依賴(lài)關(guān)系。在無(wú)法實(shí)現(xiàn)完全可移植性的情況下，例如，如果存在固有的目標(biāo)依賴(lài)項(xiàng)，則軟件結(jié)構(gòu)應(yīng)封裝此類(lèi)依賴(lài)項(xiàng)。

Ada 在軟件工程支持和程序可靠性方面對(duì) FACE UoC 開(kāi)發(fā)人員具有很強(qiáng)的優(yōu)勢(shì)，它旨在促進(jìn)完全可移植代碼的開(kāi)發(fā)，但即使是 Ada 也具有實(shí)現(xiàn)依賴(lài)性的功能。本文介紹了應(yīng)用程序開(kāi)發(fā)人員如何使用 Ada 或其形式上可分析的 SPARK 子集來(lái)實(shí)現(xiàn) FACE UoC 的完全可移植性，特別是對(duì)于 FACE 技術(shù)標(biāo)準(zhǔn)中定義的安全或安保功能集/配置文件。

功能便攜性

可移植性，或者這里所說(shuō)的功能可移植性，以區(qū)別于FACE一致性意義上的可移植性，從早期開(kāi)始就是編程語(yǔ)言設(shè)計(jì)的目標(biāo)。理想情況下，功能可移植性意味著可以在一個(gè)平臺(tái)上編譯和運(yùn)行源程序，然后，可能使用不同供應(yīng)商的編譯器，可以在同一平臺(tái)或不同平臺(tái)上成功編譯和運(yùn)行同一程序，并具有等效的效果。（“等效”非正式地意味著程序具有相同的外部影響，但允許的時(shí)間差異除外。實(shí)時(shí)程序?qū)τ谠试S哪些時(shí)序差異的概念有限 - 即，它的一些時(shí)序約束是必不可少的 - 因?yàn)殄e(cuò)過(guò)截止日期可能意味著程序無(wú)法滿足其要求。然而，在實(shí)踐中，一些障礙可能會(huì)干擾功能可移植性。這些可以包括：使用非標(biāo)準(zhǔn)的語(yǔ)言功能（即特定編譯器供應(yīng)商獨(dú)有的語(yǔ)言功能），或者標(biāo)準(zhǔn)但可選且并非由所有編譯器實(shí)現(xiàn)的語(yǔ)言功能;使用語(yǔ)義定義不精確的標(biāo)準(zhǔn)語(yǔ)言特征;以及對(duì)目標(biāo)平臺(tái)特征的依賴(lài)性。

以下內(nèi)容將提供有關(guān) Ada 功能可移植性的指導(dǎo)，涵蓋 Ada 95 和 Ada 2012，重點(diǎn)介紹 FACE 技術(shù)標(biāo)準(zhǔn)版 3.0 或更高版本的安保和安全功能集允許的功能。如果適用，該指南顯示了如何使用 SPARK Ada 子集來(lái)緩解潛在的不可移植性。（除非另有說(shuō)明，否則語(yǔ)言名稱(chēng)“Ada”是指 Ada 95 和 Ada 2012。本指南并非詳盡無(wú)遺的清單;Ada 參考手冊(cè)是關(guān)于哪些功能可以產(chǎn)生與實(shí)現(xiàn)相關(guān)的效果的權(quán)威信息來(lái)源。

語(yǔ)言擴(kuò)展

為了防止供應(yīng)商“鎖定”非標(biāo)準(zhǔn)擴(kuò)展，Ada 編譯器的認(rèn)證策略從一開(kāi)始就包含“無(wú)超集”指令。但是，該策略始終承認(rèn)供應(yīng)商特定功能的效用，前提是不引入新語(yǔ)法，從而允許某些類(lèi)型的語(yǔ)言擴(kuò)展;特別是，實(shí)現(xiàn)定義的庫(kù)、編譯指示、屬性、編譯指示限制的參數(shù)以及（對(duì)于 Ada 2012）方面。

FACE 安全擴(kuò)展和安全基礎(chǔ)與安保功能集在這方面施加了一些限制，但不會(huì)限制此類(lèi)語(yǔ)言擴(kuò)展。為了便于移植，應(yīng)盡量減少使用實(shí)現(xiàn)定義的語(yǔ)言擴(kuò)展。Ada 2012 明確支持通過(guò)編譯指示限制的參數(shù)來(lái)強(qiáng)制缺少實(shí)現(xiàn)定義的擴(kuò)展;例如，No_Implementation_Pragmas和No_Implementation_Units。

可選功能

功能可移植性的另一個(gè)障礙是使用并非所有編譯器都支持的標(biāo)準(zhǔn)功能。Ada 的認(rèn)證策略通過(guò)禁止子集來(lái)解決此問(wèn)題：每個(gè) Ada 編譯器都必須實(shí)現(xiàn)完整的語(yǔ)言。然而，導(dǎo)致Ada 95的修訂過(guò)程承認(rèn)，特定領(lǐng)域具有專(zhuān)門(mén)的（有時(shí)是相互沖突的）要求，因此，在編譯器認(rèn)證方面，一些附件（“特殊需要”附件）是可選的。編譯器必須實(shí)現(xiàn)完整的“核心”語(yǔ)言，包括預(yù)定義的環(huán)境（標(biāo)準(zhǔn)庫(kù)）和跨語(yǔ)言接口設(shè)施，但系統(tǒng)編程、實(shí)時(shí)系統(tǒng)、分布式系統(tǒng)、數(shù)字、信息系統(tǒng)和安全與安保附件是可選的。

在實(shí)踐中，這種可選性并不是一個(gè)問(wèn)題，因?yàn)樽畛Ｓ玫母郊?- 系統(tǒng)編程和實(shí)時(shí)系統(tǒng) - 由Ada生態(tài)系統(tǒng)中的供應(yīng)商支持。此外，Ada 的 FACE 安全和安保功能集禁止分布式系統(tǒng)、數(shù)字和信息系統(tǒng)附件，因此它們的可選性與功能可移植性無(wú)關(guān)。盡管如此，系統(tǒng)編程和實(shí)時(shí)附件提出了一些可能影響FACE UoC開(kāi)發(fā)人員的問(wèn)題：

這些附件中定義并由 FACE 安全和安保功能集允許的某些服務(wù)本質(zhì)上依賴(lài)于系統(tǒng)（例如，中斷處理），因此在移植到不同的執(zhí)行環(huán)境時(shí)需要修訂。設(shè)計(jì)應(yīng)用程序以封裝此類(lèi)依賴(lài)項(xiàng)將簡(jiǎn)化移植工作。

FACE安全和安保功能集極大地限制了這些附件提供的功能。UoC 開(kāi)發(fā)人員需要通過(guò)靜態(tài)分析或代碼審查/檢查來(lái)證明未使用這些附件中禁止的功能。

具有與實(shí)現(xiàn)相關(guān)的語(yǔ)義的功能指南

功能可移植性需要明確定義的語(yǔ)義，以便源程序?qū)幾g它的每個(gè)平臺(tái)具有等效的效果。但是，在實(shí)踐中，有時(shí)會(huì)在精確定義的語(yǔ)義和高效的運(yùn)行時(shí)性能之間進(jìn)行權(quán)衡。由于效率通常是程序員的關(guān)鍵要求，因此語(yǔ)言標(biāo)準(zhǔn)（包括 Ada）包含的功能在不同實(shí)現(xiàn)中效果可能有所不同。

表達(dá)式中的求值順序

為了便于優(yōu)化，Ada 不指定包含算術(shù)表達(dá)式的項(xiàng)的計(jì)算順序，但在某些情況下，效果取決于編譯器選擇的順序。緩解此問(wèn)題的一種方法是識(shí)別有潛在問(wèn)題的實(shí)例（通過(guò)檢查或靜態(tài)分析），并通過(guò)將表達(dá)式重寫(xiě)為計(jì)算中間結(jié)果的賦值語(yǔ)句序列來(lái)使順序具有確定性。或者，通過(guò)使用 SPARK Ada 子集可以完全消除潛在的不可移植性：諸如禁止函數(shù)中的副作用之類(lèi)的限制可確保表達(dá)式的值相同，而不管編譯器選擇的計(jì)算順序如何。

參數(shù)傳遞

Ada 中子程序的形式參數(shù)是根據(jù)數(shù)據(jù)流的方向指定的：

“in”，從調(diào)用方到被叫子程序

“out”，當(dāng)子程序返回時(shí)，從被調(diào)用的子程序返回到調(diào)用方

“IN out”，從調(diào)用方到被調(diào)用子程序，然后在子程序返回時(shí)從被調(diào)用子程序返回到調(diào)用方

編譯器選擇是通過(guò)復(fù)制還是通過(guò)引用傳遞參數(shù)。對(duì)于某些類(lèi)型的類(lèi)型（特別是標(biāo)量類(lèi)型和訪問(wèn)類(lèi)型（“指針”），參數(shù)傳遞的語(yǔ)義是通過(guò)復(fù)制進(jìn)行的。對(duì)于其他一些類(lèi)型的類(lèi)型，語(yǔ)義是通過(guò)引用的。但是對(duì)于不屬于這些類(lèi)別的類(lèi)型，編譯器可以選擇任一策略，通常使用類(lèi)型的對(duì)象大小作為條件。如果每個(gè)對(duì)象的大小小于某個(gè)閾值，則使用復(fù)制，否則將按引用。

潛在的功能可移植性問(wèn)題是子程序的效果可能取決于編譯器的選擇。這可以通過(guò)“別名”（例如，全局變量作為參數(shù)傳遞給子程序，并且也從子程序賦值）或異常處理（從子程序分配正式的“out”或“in out”參數(shù)，但在子程序返回之前傳播異常）來(lái)實(shí)現(xiàn)。

可以通過(guò)多種方式緩解這些與實(shí)現(xiàn)相關(guān)的影響。通過(guò)確保全局變量不作為參數(shù)傳遞給可分配給變量的子程序，可以避免混疊問(wèn)題。違規(guī)可以通過(guò)代碼審查/檢查或靜態(tài)分析工具檢測(cè)到，并在 SPARK（禁止此類(lèi)混疊）中得到阻止。

異常傳播問(wèn)題可以通過(guò)適當(dāng)?shù)木幊谭绞絹?lái)避免：將任何對(duì)形式參數(shù)的賦值推遲到可以確保不會(huì)發(fā)生異常傳播之后。SPARK 完全避免了此問(wèn)題，因?yàn)樽C明工具可以證明不存在運(yùn)行時(shí)異常。

對(duì)未初始化變量的引用

Ada 語(yǔ)言允許在不初始化的情況下聲明變量。普遍要求初始化將是有問(wèn)題的：合理的初始值可能不存在，或者程序邏輯可能需要在系統(tǒng)啟動(dòng)時(shí)由外部輸入提供初始化。更微妙的是，默認(rèn)初始化可能會(huì)導(dǎo)致難以檢測(cè)的編程錯(cuò)誤，其中需要顯式初始化的變量被過(guò)早引用，從而產(chǎn)生對(duì)變量類(lèi)型有效但不正確的默認(rèn)初始化。

在初始化變量之前引用變量是編程錯(cuò)誤。在沒(méi)有保證值的情況下，Ada 語(yǔ)義使此類(lèi)引用的效果保持未定義。確保變量在引用之前被初始化超出了 FACE 安全和安保功能集中的限制范圍，因此需要通過(guò)其他方式強(qiáng)制執(zhí)行。

幾個(gè) Ada 語(yǔ)言功能可以提供幫助：

某些類(lèi)型需要默認(rèn)初始化。特別是當(dāng)在沒(méi)有顯式初始化的情況下聲明訪問(wèn)值（指針）時(shí)，它將被設(shè)置為特殊值 null。嘗試取消引用空值引發(fā)異常

程序員可以為記錄字段定義默認(rèn)初始值

在 Ada 2012 中，任何標(biāo)量類(lèi)型都可以定義默認(rèn)初始值

在實(shí)踐中，Ada 編譯器在許多情況下會(huì)檢測(cè)到對(duì)其他類(lèi)型的未初始化變量的引用，尤其是在使用復(fù)雜流分析的更高優(yōu)化級(jí)別。靜態(tài)分析工具也可以解決這個(gè)問(wèn)題，同時(shí)最大限度地減少“誤報(bào)”。與本節(jié)中討論的所有其他潛在的不可移植性一樣，SPARK 中完全禁止引用未初始化的變量，因?yàn)樗鼈儗⒈?SPARK 證明工具檢測(cè)到。

并發(fā)

Ada 具有強(qiáng)大且高級(jí)的并發(fā)模型，但為了支持廣泛的目標(biāo)環(huán)境，該語(yǔ)言允許許多調(diào)度策略決策由實(shí)現(xiàn)確定。Ravenscar配置文件緩解了這種非確定性，Ravenscar配置文件是Ada任務(wù)功能的一個(gè)簡(jiǎn)單，確定性和有效的子集。FACE Safety-Extended 和 Safety-Base & Security 功能集都將 Ada 任務(wù)工具限制為 Ravenscar 子集，從而避免了完整任務(wù)模型的功能可移植性問(wèn)題。（在 FACE 技術(shù)標(biāo)準(zhǔn) 3.0 版的 Ada 95 以及 3.1 版的 Ada 95 和 Ada 2012 的安全功能集中允許使用 Ravenscar 功能。

Ravenscar子集由SPARK支持，因此SPARK程序?qū)⒈苊馔暾鸄da任務(wù)模型的非確定性。

細(xì)化順序

Ada 程序通常由主子程序以及主子程序直接或間接依賴(lài)的模塊（“包”）組成。程序執(zhí)行首先在各種依賴(lài)包中執(zhí)行運(yùn)行時(shí)代碼（例如初始化全局?jǐn)?shù)據(jù)） - 稱(chēng)為“包細(xì)化” - 然后調(diào)用主子程序。包的詳細(xì)說(shuō)明順序部分受語(yǔ)言語(yǔ)義的約束，但通常依賴(lài)于實(shí)現(xiàn)，不同的順序可能會(huì)產(chǎn)生不同的結(jié)果。實(shí)現(xiàn)依賴(lài)性是語(yǔ)言語(yǔ)義所固有的，因?yàn)槿魏瓮耆付ㄔ敿?xì)說(shuō)明順序的嘗試也會(huì)禁止有用的情況，例如相互依賴(lài)的包。

有幾種技術(shù)可以幫助確保可移植性：

添加適當(dāng)?shù)木幾g指示以約束詳細(xì)說(shuō)明順序（有關(guān)示例，請(qǐng)參見(jiàn)圖 1）或

通過(guò)將所有這些代碼移動(dòng)到在主子程序開(kāi)始時(shí)顯式調(diào)用的過(guò)程中，避免依賴(lài)包中的細(xì)化時(shí)代碼

［圖1 |細(xì)化順序。

通過(guò)使用 SPARK 也可以避免細(xì)化順序非確定性，因?yàn)?SPARK 限制確保所有細(xì)化順序具有相同的效果。

目標(biāo)依賴(lài)項(xiàng)指南

System.* 包層次結(jié)構(gòu)和表示子句：盡管低級(jí)編程涉及訪問(wèn)特定于目標(biāo)的特征，但 Ada 通過(guò)標(biāo)準(zhǔn)語(yǔ)言功能有助于減少不可移植性。包 System 聲明類(lèi)型地址和相關(guān)操作，子包System.Storage_Elements和System.Address_To_Access_Conversions提供用于處理“原始存儲(chǔ)”和將指針視為物理地址的標(biāo)準(zhǔn)工具，反之亦然。表示子句允許程序定義程序?qū)嶓w的低級(jí)屬性，例如記錄的布局或變量的地址。這些功能由人臉安全和安保功能集允許。盡管它們的用法是特定于平臺(tái)的，但將此類(lèi)代碼封裝在包的主體中將進(jìn)行本地化，并有助于最大限度地減少將代碼移植到新目標(biāo)平臺(tái)時(shí)所需的適應(yīng)。

數(shù)值類(lèi)型表示：Ada 中預(yù)定義的數(shù)值類(lèi)型（整數(shù)、浮點(diǎn)數(shù)等）具有實(shí)現(xiàn)定義的范圍/精度。如果程序員隱式假定 Integer 等類(lèi)型始終具有某個(gè)最小范圍，則這種情況可能會(huì)導(dǎo)致功能可移植性問(wèn)題;當(dāng)將代碼移植到 Integer 范圍較窄的平臺(tái)時(shí)，算術(shù)表達(dá)式可能會(huì)溢出并引發(fā)異常。

可以通過(guò)聲明自定義數(shù)值類(lèi)型而不是使用預(yù)定義類(lèi)型來(lái)避免潛在的不可移植性。圖 2 顯示了一個(gè)示例。

［圖2 |便攜式數(shù)字類(lèi)型。

遵循使用模式

編寫(xiě)完全可移植的代碼不僅需要 FACE 一致性，還需要功能可移植性。這意味著遵循適當(dāng)?shù)氖褂媚Ｊ剑貏e是對(duì)于語(yǔ)義未完全由語(yǔ)言標(biāo)準(zhǔn)定義的功能。

一般來(lái)說(shuō)，Ada 是一種對(duì)功能可移植性有強(qiáng)大支持的語(yǔ)言，多年來(lái)，系統(tǒng)現(xiàn)代化已經(jīng)成功地將大型 Ada 程序移植到新硬件和新的編譯器實(shí)現(xiàn)中。盡管如此，功能可移植性不會(huì)自動(dòng)到來(lái)，必須進(jìn)行規(guī)劃;開(kāi)發(fā)人員應(yīng)避免使用依賴(lài)于實(shí)現(xiàn)的語(yǔ)言功能，或者采取適當(dāng)?shù)木徑獯胧＿@對(duì)于需要遵守 FACE 安全和安保功能集/配置文件之一的應(yīng)用程序尤其重要。此類(lèi)應(yīng)用程序具有很強(qiáng)的保證要求，如果代碼使用未精確定義的語(yǔ)言功能，則很難演示這些要求。Ada 的 SPARK 子集特別相關(guān)，因?yàn)?SPARK 語(yǔ)言限制確保了確定性語(yǔ)義。

簡(jiǎn)而言之，為Ada采用適當(dāng)?shù)娘L(fēng)格約定（其中大部分可以通過(guò)靜態(tài)分析工具（如AdaCore的CodePeer或GNATcheck）或使用SPARK可以幫助開(kāi)發(fā)人員實(shí)現(xiàn)其FACE兼容軟件的完全可移植性，同時(shí)實(shí)現(xiàn)Ada和SPARK帶來(lái)的保證優(yōu)勢(shì)。

審核編輯：郭婷