Ada 是一種強(qiáng)類型語言，是開發(fā)高可靠性程序的自然選擇。一些語言，如C，擅長低級編程，但不能解決其他挑戰(zhàn) - 正如我之前的博客所介紹的那樣。您需要為工作選擇合適的工具。與其對每個問題使用一種語言或一種工具，不如為工程師提供多種選擇來開發(fā)高可靠性軟件——這正是 Ada 的亮點。

我們可以通過高層次的視角來說明這一點，而無需深入研究特定的語言細(xì)節(jié)和個人偏好。第一步是研究強(qiáng)類型語言如何避免難以檢測的錯誤和不正確的程序操作。

Ada在高可靠性應(yīng)用中的優(yōu)勢

Ada 的許多高可靠性軟件開發(fā)功能并非 Ada 所獨有，可以在各種其他（強(qiáng)類型）編程語言中找到。Ada的獨特之處在于所有這些功能都可以在一種編程語言中找到。

Ada 是強(qiáng)類型。簡單來說，這意味著變量、常量或?qū)ο蟊仨氃谑褂弥奥暶鳌５?，它也允許語言（編譯器）靜態(tài)檢查使用此類標(biāo)識符的有效性。

此設(shè)計功能的一個有趣效果是，可以將拼寫錯誤和拼寫錯誤檢測為錯誤并為開發(fā)人員標(biāo)記。任何人類的寫作努力都會有錯誤，隨著總寫作工作量的增加，錯誤的數(shù)量也會增加。由于許多拼寫錯誤對于不經(jīng)意的觀察者來說看起來是正確的（或者它們一開始就不會發(fā)生），讓語言檢測到這些是非常有價值的。

假設(shè)程序員打算將車輛位置“L”計算為實數(shù)，并將整數(shù)索引“I”用于其他目的。在 Ada 中，如果使用變量“I”而不是“L”，則它將被標(biāo)記為操作的錯誤類型。在 C 中，索引“I”將被隱式轉(zhuǎn)換（“強(qiáng)制轉(zhuǎn)換”）為表達(dá)式中的實值，從而引入錯誤。像這樣的簡單錯誤可能保持隱藏，難以發(fā)現(xiàn)，并且對軟件的預(yù)期含義有潛移默化的變化。例如，“位置”應(yīng)該是程序中此時的車輛位置，但索引“I”是不相關(guān)的。

Ada 支持將程序規(guī)范與實現(xiàn)分離的概念。該語言支持外部程序單元可見和調(diào)用的程序規(guī)范的定義。這定義了單元或子程序的名稱及其參數(shù)、類型等。該規(guī)范對使用“with”構(gòu)造的調(diào)用方可見。實現(xiàn)或正文可能位于單獨的文件中，并包含規(guī)范的完整算法實現(xiàn)。此單元在語義上始終對調(diào)用方不可見。因此，調(diào)用方無法更改算法的內(nèi)部詳細(xì)信息。

這是Ada語言的一個關(guān)鍵特征，因為可以單獨開發(fā)，測試和驗證單元集合，而不必?fù)?dān)心組合時會發(fā)生副作用。這允許以安全和可擴(kuò)展的方式構(gòu)建分層或組件架構(gòu)。Ada 在這方面具有其他功能，但此基本概念對于開發(fā)高可靠性應(yīng)用程序至關(guān)重要。具有“#Include”樣式的其他語言功能在語義上將引用單元的源文本“包含”到引用/調(diào)用單元的源中。這使得所有內(nèi)部詳細(xì)信息對調(diào)用方可見，并允許發(fā)生意外或有目的的副作用。在小程序中，可以手動檢測對這些內(nèi)部細(xì)節(jié)的操縱。讀者可以看到，調(diào)用方中的拼寫錯誤可能會意外引用并更改被調(diào)用單元中的內(nèi)部值（開發(fā)人員鍵入的“X”未在本地聲明，但最終在所包含的單元中引用了“X”）。再一次，在較大的程序中，像這樣的簡單引用可能保持隱藏狀態(tài)，難以發(fā)現(xiàn)，并且對軟件的預(yù)期含義有隱蔽的變化。

通過結(jié)合這兩個簡單的功能，語言還可以檢查兩個標(biāo)識符是否可以在表達(dá)式中一起使用。假設(shè)兩個變量“A”和B“聲明為：

? A 和 B 是整數(shù)類型? A 是整數(shù)，B 是顏色類型

加號（“+”）是一個子程序，具有定義數(shù)量的參數(shù)輸入，具有特定類型，具有特定的返回值類型。是否有 1 “+” 1 （A+B） 的操作“+”？是否有 1“+” 藍(lán)色 （A+B） 的操作“+”？在 C 語言的情況下，這兩個表達(dá)式都可能是有效的，但它們是什么意思？在 Ada 的情況下，第一個表達(dá)式有效，但第二個表達(dá)式無效。同樣，此類錯誤在開發(fā)生命周期的早期就被發(fā)現(xiàn)，在那里它們很容易被廉價地發(fā)現(xiàn)和糾正。

我只概述了 Ada 的一些非常基本功能的一些高級優(yōu)勢，因此可以在直觀的層面上理解它們，為什么這些使程序更容易開發(fā)而沒有錯誤。Ada 語言還有更多有助于開發(fā)高可靠性程序的功能，我鼓勵您自己探索和測試它們。

審核編輯：郭婷