使軟件符合人臉標(biāo)準(zhǔn)并完全可移植：Ada的編碼指南

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

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

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

功能便攜性

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

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

語言擴(kuò)展

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

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

可選功能

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

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

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

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

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

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

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

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

參數(shù)傳遞

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

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

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

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

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

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

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

異常傳播問題可以通過適當(dāng)?shù)木幊谭绞絹肀苊猓簩⑷魏螌π问絽?shù)的賦值推遲到可以確保不會發(fā)生異常傳播之后。SPARK 完全避免了此問題，因為證明工具可以證明不存在運行時異常。

對未初始化變量的引用

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

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

幾個 Ada 語言功能可以提供幫助：

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

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

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

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

并發(fā)

Ada 具有強(qiáng)大且高級的并發(fā)模型，但為了支持廣泛的目標(biāo)環(huán)境，該語言允許許多調(diào)度策略決策由實現(xiàn)確定。Ravenscar配置文件緩解了這種非確定性，Ravenscar配置文件是Ada任務(wù)功能的一個簡單，確定性和有效的子集。FACE Safety-Extended 和 Safety-Base & Security 功能集都將 Ada 任務(wù)工具限制為 Ravenscar 子集，從而避免了完整任務(wù)模型的功能可移植性問題。（在 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 程序通常由主子程序以及主子程序直接或間接依賴的模塊（“包”）組成。程序執(zhí)行首先在各種依賴包中執(zhí)行運行時代碼（例如初始化全局?jǐn)?shù)據(jù)） - 稱為“包細(xì)化” - 然后調(diào)用主子程序。包的詳細(xì)說明順序部分受語言語義的約束，但通常依賴于實現(xiàn)，不同的順序可能會產(chǎn)生不同的結(jié)果。實現(xiàn)依賴性是語言語義所固有的，因為任何完全指定詳細(xì)說明順序的嘗試也會禁止有用的情況，例如相互依賴的包。

有幾種技術(shù)可以幫助確?？梢浦残裕?/p>

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

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

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

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

目標(biāo)依賴項指南

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

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

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

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

遵循使用模式

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

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

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

審核編輯：郭婷