Ada 語言的魅力 —— 用型別闡述設計理念,支撐運作數十年軟體的語言
· 小村 豪 · Ada, ProgrammingLanguage, StrongTyping, SPARK, GNAT, Alire, HighIntegrity, Embedded, 高可靠性
1. 首先要掌握的重點
你聽過 Ada 這個語言名稱嗎?
或許很多人對它的印象是「老舊的語言」「軍用的語言」「只在課堂上聽過名字」。
但事實上,Ada 至今仍是一門現役語言。
在民航機的飛行控制、鐵路號誌系統、火箭、航空管制、人工衛星、醫療器材等一旦停擺就會關係到人命的軟體世界裡,Ada 已經被持續使用了數十年。
理解 Ada 時,重要的是下面這個觀點:
Ada 是一門全力投入「在執行前就把 bug 消滅」的語言
型別不是資料的容器,而是用來表達設計意圖的工具
規格與實作的分離、契約、並行處理都內建於語言之中
它並未流行起來,但其設計理念被現代語言繼承下來
本文將整理 Ada 的歷史、語法、強型別、範圍限制、套件、契約式設計、任務(task)、SPARK、開發環境,以及它的弱點,帶你認識 Ada 的魅力。
希望平常寫 C#、C++、Java 的讀者,能從中帶回「用型別闡述設計」的感覺。
順帶一提,本文出現的程式碼片段,已依章節整理成參考用程式碼集,發布在 GitHub 上。
ada-language-appeal - komurasoft-blog-samples (GitHub)
2. Ada 是什麼 —— 名稱的由來與歷史
Ada 是 1970 年代後期,由美國國防部(DoD)主導誕生的通用程式語言。
當時的國防部面臨一個問題:每個專案使用的語言各不相同,導致軟體的維護成本不斷膨脹。
因此,他們透過國際性的設計競賽,選出一款也能用於嵌入式系統與即時系統的標準語言。
最後獲選的,是由 Jean Ichbiah 領導的團隊所提出的設計方案。
語言名稱 Ada,來自於被稱為世界上第一位程式設計師的 Ada Lovelace(奧古斯塔·愛達·金,勒芙蕾絲伯爵夫人)。
大致整理 Ada 的歷史如下:
1980年 制定第一版規格 MIL-STD-1815
1983年 Ada 83(ANSI 標準)
1987年 成為 ISO 標準
1995年 Ada 95(引入物件導向、受保護物件)
2005年 Ada 2005(介面、擴充容器函式庫)
2012年 Ada 2012(將契約式設計納入語言功能)
2022年 Ada 2022(最新標準)
Ada 95 是最早期通過 ISO 標準化的物件導向語言之一。
而在 Ada 2012 中,事前條件、事後條件、型別不變條件等契約式設計(Design by Contract)被納入語言規格。
Ada 並不是「老舊的語言」,而是一門持續修訂超過 40 年的語言。
3. Ada 用在哪些地方
Ada 持續被使用的代表性領域,是需要高可靠性(High Integrity)的系統。
民航機的飛行控制與航空電子設備
航空管制系統
鐵路的號誌與保安系統
火箭、人工衛星
國防系統
醫療器材
金融與產業界部分的核心系統
這些領域有共通的特徵:
bug 會直接關係到人命或造成巨額損失
認證與稽核會要求「正確性的證據」
一旦部署就會持續使用數十年
事後修正的成本極高
在這個世界裡,「先發布,之後再修就好」的想法並不適用。
Ada 的語言設計,正是為了回應這樣的需求。
編譯期能檢測出的 bug 在編譯期處理,只有執行期才能檢測出的用執行期檢查處理,甚至更進一步,能用數學方式證明的就用證明來消滅——這個思路貫穿了整個語言。
這種思維方式,對於寫 Web 或桌面業務應用的開發者來說,也很有學習價值。
4. 先來個 Hello, World
我們來看看 Ada 的程式碼。
with Ada.Text_IO;
procedure Hello is
begin
Ada.Text_IO.Put_Line ("Hello, Ada!");
end Hello;
第一眼會注意到下面幾點:
用 with 引入函式庫單元
程式的主體是程序(procedure)
用 begin / end 包住區塊
end 之後要重複寫一次名稱
陳述句以分號結尾
像 end Hello; 這樣在結尾重新寫出名稱,是很有 Ada 味道的地方。
即使區塊層層嵌套,也能一眼看出「這個 end 是誰的 end」。
編譯器也會檢查名稱是否對應,區塊結尾寫錯就會變成編譯錯誤。
看起來是件小事,但這正體現了 Ada 的理念:「讓語言撐住人容易讀錯的地方」。
5. 重視易讀性的語法
Ada 的語法設計,易讀性優先於易寫性。
因為它建立在一個前提之上:軟體被閱讀的次數,遠遠多於被撰寫的次數。
舉例來說,迴圈與條件分支是這樣寫的:
for I in 1 .. 5 loop
Ada.Text_IO.Put_Line (Integer'Image (I * I));
end loop;
if Temperature > 80.0 then
Start_Cooling;
elsif Temperature < 20.0 then
Start_Heating;
else
Keep_Current_State;
end if;
case 陳述句有個很有 Ada 味道的特徵:
case Today is
when Mon .. Fri =>
Put_Line ("Weekday");
when Sat | Sun =>
Put_Line ("Weekend");
end case;
重點如下:
case 沒有涵蓋所有值就會編譯錯誤
不存在像 C 系語言那樣隱含的 fallthrough
可以用範圍(Mon .. Fri)或選項(Sat | Sun)歸納條件
只要在列舉型別中新增一個值,沒有涵蓋到的 case 陳述句就會全部變成編譯錯誤。
「編譯器會幫你列出規格變更所影響的位置」這種體驗,一旦嘗過就很難放手。
此外,引數還能使用具名關聯:
Draw_Rectangle (Left => 10, Top => 20, Width => 100, Height => 50);
這能防止引數順序搞錯,呼叫端的程式碼本身就成了文件。
賦值用 :=,比較用 =,像 C 系語言 if (a = b) 那樣的手誤,在語法層級就不會發生。
6. 強型別 —— 讓單位搞混變成編譯錯誤
Ada 最大的魅力,就是強型別。
許多語言都會用「強型別」這個詞,但 Ada 的強型別更深一層。
在 Ada 中,即使結構完全相同,用不同名稱宣告的型別也是不同的型別。
type Meters is new Float;
type Seconds is new Float;
Distance : Meters := 100.0;
Time : Seconds := 9.58;
這兩者的本質都是浮點數,但不能混著用。
Distance := Time; -- 編譯錯誤
Distance := Distance + Time; -- 編譯錯誤
只有刻意要轉換時,才需要明確寫出來。
Speed : constant Float := Float (Distance) / Float (Time);
為什麼要嚴格到這個地步?
現實世界中,不少軟體事故的原因都是「單位搞混」。
一個知名的例子是,1999 年的火星探測器 Mars Climate Orbiter,就是因為英制單位與公制單位混用而失蹤的。
Ada 的答案很單純:
把公尺與英尺變成不同的型別
混用就變成編譯錯誤
轉換要明確寫出來
不是靠「小心一點」「靠審查抓出來」「靠測試抓出來」,而是一開始就讓它編譯不過。
這就是 Ada 的基本態度。
7. 範圍限制 —— 在資料型別層級防止不合法的值
在 Ada 中,型別可以帶有數值範圍。
subtype Percentage is Integer range 0 .. 100;
Progress : Percentage := 50;
如果試圖把超出範圍的值放進 Percentage 型別的變數,會在執行期引發 Constraint_Error 例外。
Progress := 120; -- 執行期發生 Constraint_Error
編譯期就能判斷出的違規,會在編譯期被檢測出來。
「應該是 0 到 100 之間的值」「應該是 1 以上的值」這種隱含的前提,不用寫在註解裡,而是能用型別直接表達出來。
事實上,Ada 標準函式庫中也預先定義了一些常用的受限型別。
Natural = Integer range 0 .. Integer'Last
Positive = Integer range 1 .. Integer'Last
而且從 Ada 2012 開始,還能為型別附加任意條件作為述語。
subtype Even is Integer
with Dynamic_Predicate => Even mod 2 = 0;
像固定小數點型別這種面向硬體控制的型別,也內建於語言之中。
type Temperature is delta 0.1 range -50.0 .. 150.0;
在許多語言裡,不合法值的檢查往往會變成這樣:
在函式開頭用 if 陳述句做驗證
漏檢查與否全靠 code review
哪個函式收到的是已檢查過的值並不清楚
在 Ada 中,可以說「只要是這個型別的值,範圍就已經被保證了」。
驗證的責任轉移到資料型別上,函式的邏輯就能專注在它本來該做的事上。
8. 陣列與索引 —— 邊界檢查與列舉型別索引
Ada 的陣列可以自由選擇索引的型別。
type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
type Hours_Array is array (Day) of Natural;
Work_Hours : Hours_Array := (Mon .. Fri => 8, others => 0);
這是以列舉型別 Day 作為索引的陣列。
可以用 Work_Hours (Wed) 這樣的方式存取,不需要記住「這個數字索引代表什麼意思」。
迴圈也能沿著索引型別來寫。
for D in Work_Hours'Range loop
Put_Line (Day'Image (D) & ":" & Natural'Image (Work_Hours (D)));
end loop;
'Range、'First、'Last、'Length 這類屬性,可以隨時取得陣列的邊界資訊。
因為不會把邊界寫死,陣列大小的變更不會波及到迴圈。
而更重要的是,陣列存取永遠會做邊界檢查。
Buffer : String (1 .. 10);
Index : Integer := 11;
Buffer (Index) := 'x'; -- 執行期發生 Constraint_Error
C/C++ 的緩衝區溢位,多年來一直是安全漏洞的主要原因之一。
在 Ada 中,越界存取不是未定義行為,而是定義明確的例外。
不是悄悄破壞記憶體、在別的地方引發莫名其妙的當機,而是在問題發生的那一刻立刻大聲停下來。
考慮到長期運作系統的調查成本,這個差異非常巨大。
9. 套件 —— 規格與實作的分離
Ada 的模組機制是套件(package)。
套件會分成規格(spec)與本體(body)兩個檔案。
counters.ads 規格:對外公開的介面
counters.adb 本體:實作細節
規格這樣寫:
package Counters is
type Counter is private;
procedure Increment (C : in out Counter);
function Value (C : Counter) return Natural;
private
type Counter is record
Count : Natural := 0;
end record;
end Counters;
本體這樣寫:
package body Counters is
procedure Increment (C : in out Counter) is
begin
C.Count := C.Count + 1;
end Increment;
function Value (C : Counter) return Natural is
begin
return C.Count;
end Value;
end Counters;
值得注意的地方是:
把 type 宣告為 private,使用端就無法碰觸內部結構
只要讀規格(.ads),就能了解全部的使用方式
只要規格不變,修改本體(.adb)對使用端而言重新編譯的範圍就是最小的
這跟 C/C++ 的標頭檔有點類似,但不是像 #include 那樣的文字展開,而是作為語言規格接受一致性檢查。
規格與本體不一致,會是編譯錯誤。
此外,引數一定要寫出 in、out、in out 這種模式。
procedure Increment (C : in out Counter);
「這個引數只是讀取、只是寫入,還是讀寫兩用」,光看簽名就能知道。
即使沒有指標或參照的知識,也能讀出資料流動的方向。
10. 記錄與判別子
Ada 中相當於結構體的是記錄(record)。
type Point is record
X : Float := 0.0;
Y : Float := 0.0;
end record;
P : Point := (X => 1.0, Y => 2.0);
欄位可以有預設值,也能用具名初始化的集成體(aggregate)來初始化。
很有 Ada 特色的功能是判別子(discriminant)。
type Buffer (Size : Positive) is record
Data : String (1 .. Size);
Length : Natural := 0;
end record;
Small : Buffer (Size => 16);
Large : Buffer (Size => 4096);
判別子是決定記錄「形狀」的參數。
Buffer (16) 與 Buffer (4096) 是同一個型別,但內部陣列的大小在宣告時就已確定,之後不會改變。
大概可以想像成,C 語言中「帶有可變長度成員的結構體 + 大小欄位」這種模式,被語言以型別的形式安全地管理起來。
大小與實體不一致這種在 C 中常見的 bug 入口,在 Ada 中一開始就不存在。
11. 泛型
Ada 從 1983 年最初的標準開始,就已經具備泛型(generic)。
這遠比 C++ 的樣板(1990 年代)或 Java 的泛型(2004 年)出現得早得多。
generic
type Element is private;
procedure Swap (Left, Right : in out Element);
procedure Swap (Left, Right : in out Element) is
Temp : constant Element := Left;
begin
Left := Right;
Right := Temp;
end Swap;
使用端會用具體的型別來實體化。
procedure Swap_Integers is new Swap (Element => Integer);
procedure Swap_Floats is new Swap (Element => Float);
Ada 泛型的特徵是明確標示所要求的操作。
generic
type Element is private;
with function "<" (Left, Right : Element) return Boolean is <>;
function Max (Left, Right : Element) return Element;
規格上會寫明「這個泛型函式,要求 Element 型別具有比較運算子」。
C++ 的樣板長年為之所苦的「只有在實體化之後才知道錯誤」的問題,在 Ada 中從一開始就不會發生。
C++20 的 concepts 或 Rust 的 trait bound 試圖解決的問題,Ada 在 40 年前就已經有了答案。
12. 例外處理
Ada 也有例外處理機制。
with Ada.Text_IO;
with Ada.Exceptions;
procedure Read_Config is
begin
Load_File ("config.txt");
exception
when Ada.Text_IO.Name_Error =>
Ada.Text_IO.Put_Line ("找不到設定檔");
when E : others =>
Ada.Text_IO.Put_Line (Ada.Exceptions.Exception_Information (E));
raise;
end Read_Config;
在區塊的最後寫上 exception 部分,按例外種類逐一列出處理程序。
語言內建定義的例外,具代表性的有下列幾種:
Constraint_Error 範圍限制違規、陣列邊界違規、除以零等
Program_Error 違反語言規則(到達不該到達的地方等)
Storage_Error 記憶體不足
Tasking_Error 任務間通訊失敗
值得注意的是,範圍限制與邊界檢查的違規,全都被整合進這一套例外機制中。
「型別中寫下的限制」一旦被打破,就會變成 Constraint_Error。
也就是說,第 7 章看到的範圍限制,會作為自動產生的執行期斷言發揮作用。
不需要自己動手到處寫 if 陳述句去檢查。
13. 契約式設計 —— 用語言功能寫 Pre/Post 條件
Ada 2012 的一大亮點,就是契約式設計(Design by Contract)的語言支援。
可以直接在副程式上寫事前條件(Pre)與事後條件(Post)。
package Stacks is
type Stack is private;
function Is_Full (S : Stack) return Boolean;
function Is_Empty (S : Stack) return Boolean;
function Count (S : Stack) return Natural;
procedure Push (S : in out Stack; Item : Integer)
with Pre => not Is_Full (S),
Post => Count (S) = Count (S)'Old + 1;
procedure Pop (S : in out Stack; Item : out Integer)
with Pre => not Is_Empty (S),
Post => Count (S) = Count (S)'Old - 1;
private
-- 實作細節
end Stacks;
Pre 是「呼叫端應遵守的約定」,Post 是「實作端所保證的約定」。
用 'Old 屬性可以參照呼叫前的值。
這個契約可以透過編譯選項(GNAT 中是 -gnata)啟用為執行期檢查。
違反契約會引發 Assertion_Error 例外,能夠清楚知道是哪一方違背了約定。
違反 Pre -> 呼叫端的 bug
違反 Post -> 實作端的 bug
在文件註解裡寫「這個函式不能對空堆疊呼叫」,跟契約有什麼不同呢?
註解和實作走岔了也沒人會發現
契約會被編譯器檢查語法與型別
契約能在執行期自動驗證
契約會成為 SPARK 靜態證明的輸入(第16章)
規格以可驗證的形式存在於程式碼之中。
這就是 Ada 2012 之後的世界。
使用型別不變條件(Type_Invariant),還能寫出「這個型別的值永遠滿足這個性質」這樣的限制。
14. 任務(Task) —— 並行處理內建於語言之中
Ada 另一個很大的魅力,是並行處理是語言規格的一部分。
C/C++ 讓執行緒依賴作業系統的 API 或函式庫(pthread、std::thread),而 Ada 早在 1983 年,就已經把任務(task)內建於語言之中。
with Ada.Text_IO;
procedure Task_Demo is
task Worker;
task body Worker is
begin
for I in 1 .. 3 loop
Ada.Text_IO.Put_Line ("worker:" & Integer'Image (I));
delay 0.5;
end loop;
end Worker;
begin
for I in 1 .. 3 loop
Ada.Text_IO.Put_Line ("main :" & Integer'Image (I));
delay 0.5;
end loop;
end Task_Demo;
宣告 task 之後,並行執行會在包住它的區塊開始的同一時間啟動。
而重要的是,這個區塊要等內部所有任務都結束才會結束。
「忘了對執行緒做 join,導致程序結束時發生奇怪的事」這類 bug,在結構上不會發生。
任務間的同步,有一個叫做會合(rendezvous)的語言功能。
task Logger is
entry Write (Message : String);
end Logger;
task body Logger is
begin
loop
select
accept Write (Message : String) do
Ada.Text_IO.Put_Line (Message);
end Write;
or
terminate;
end select;
end loop;
end Logger;
使用端可以用 Logger.Write ("hello"); 這種跟程序呼叫一樣的形式來寫。
透過訊息傳遞進行任務間通訊,完全不需要鎖的知識就能寫出來。
面向即時系統,甚至還把排程策略、優先權控制,以及為了容易驗證而限制任務功能的 Ravenscar profile 都標準化了。
15. 保護物件 —— 把互斥控制寫成型別
共享資料的互斥控制,會使用 Ada 95 引入的保護物件(protected object)。
protected Shared_Counter is
procedure Increment;
function Value return Natural;
private
Count : Natural := 0;
end Shared_Counter;
protected body Shared_Counter is
procedure Increment is
begin
Count := Count + 1;
end Increment;
function Value return Natural is
begin
return Count;
end Value;
end Shared_Counter;
保護物件的資料,只能透過定義好的操作存取。
而互斥控制則是由語言來保證的。
procedure 可讀寫,排他性執行
function 唯讀,允許多個任務同時執行
entry 可以讓呼叫端等到條件(barrier)滿足為止
在許多語言中,互斥控制往往只能靠下面這種紀律來維持:
碰這份資料的時候要拿這個互斥鎖(mutex)
別忘了釋放鎖
要遵守鎖的取得順序
在 Ada 的保護物件中,「忘記拿鎖的程式碼」根本就寫不出來。
因為資料和保護它的互斥控制,被宣告成同一個型別。
利用 entry 的 barrier 條件,「等到佇列裡有資料為止」這類條件同步,也不用自己手動管理旗標或條件變數就能寫出來。
16. SPARK —— 通往形式驗證之路
在 Ada 的世界裡,有一個強大的夥伴叫做 SPARK。
SPARK 是 Ada 的子集(部分語言),設計目的是讓程式的性質能被用數學方式證明。
procedure Increment (X : in out Integer)
with SPARK_Mode,
Pre => X < Integer'Last,
Post => X = X'Old + 1;
SPARK 的工具(GNATprove),可以對這段程式碼在不執行的情況下證明下列事項:
不會發生溢位
不會違反範圍限制
不會發生除以零
不會讀取未初始化的變數
Pre 與 Post 的一致性
它跟測試的差異是決定性的。
測試 確認在選定的輸入下,程式是否正確運作
證明 證明性質在所有輸入下都成立
第 13 章看到的契約(Pre/Post),在 SPARK 中直接成為證明的對象。
原本寫成執行期檢查的契約,之後可以升級為「已證明」。
SPARK 在航太、國防領域積累了實績,而近年來 NVIDIA 為了韌體資安也採用了它,產業界的應用正在擴展。
「形式方法太學術,實務上用不上」這種常識,正被 Ada/SPARK 生態系不斷靜靜地推翻。
17. 與 C、C++ 的互通
Ada 並不是一門孤立的語言。
與 C 的互通,已經以語言規格(Annex B)的形式標準化。
舉例來說,要從 Ada 呼叫 Windows API 的 Sleep,可以這樣寫:
with Interfaces.C;
procedure Sleep_Demo is
procedure Sleep (Milliseconds : Interfaces.C.unsigned)
with Import,
Convention => Stdcall,
External_Name => "Sleep";
begin
Sleep (1000);
end Sleep_Demo;
重點如下:
Import 引入外部實作
Convention 指定呼叫慣例(C、Stdcall 等)
External_Name 指定連結時的符號名稱
Interfaces.C 提供對應 C 型別(int、unsigned、char* 等)的型別
反方向也可以做到。
使用 Export,可以把用 Ada 寫的程序公開成能被 C 呼叫的函式。
也就是說,可以做到下面這種階段性的使用方式:
從 Ada 使用既有的 C 函式庫
系統的核心部分只用 Ada/SPARK 寫,周邊維持 C/C++ 不變
把 Ada 的程式碼做成 DLL,讓其他語言呼叫
這不是一門「只能整套改寫」的語言,而是能與既有資產共存,從重要的部分開始逐步提升可靠性。
18. 開發環境 —— GNAT 與 Alire(在 Windows 上也能跑)
你可能會覺得「要試用 Ada,應該需要昂貴的工具吧」。
但現在,免費就能建置起相當完整的開發環境。
GNAT GCC 內建的 Ada 編譯器(免費)
Alire Ada 的套件管理工具兼建置工具
GNAT Studio AdaCore 製作的 IDE
VS Code 裝上 Ada Language Server 擴充後,可用自動完成、跳轉定義
特別是 Alire(指令名稱是 alr)的出現,讓 Ada 的入門變得大幅簡單。
體驗上很接近 Rust 的 cargo。
alr init --bin hello_ada
cd hello_ada
alr build
alr run
用 alr init 建立專案,用 alr build 建置,用 alr run 執行。
工具鏈(GNAT 本體)也是由 Alire 負責取得,因此連手動安裝編譯器都不需要。
Windows、Linux、macOS 皆可執行。
如果你是在 Windows 上開發,下面的流程最快:
1. 從 Alire 官方網站取得 Windows 用安裝程式
2. 用 alr init --bin 建立雛形
3. 在 VS Code 裝上 Ada 擴充套件(AdaCore 製作)
4. 用 alr build 建置並執行
函式庫也可以用 alr with 函式庫名稱 加入。
「因環境建置而放棄」的時代已經過去了。
19. Ada 的弱點與注意事項
到目前為止介紹了 Ada 的魅力,但 Ada 也有弱點。
在這裡公平地整理一下。
生態系規模小
Web 框架、GUI、雲端 SDK 等選項比主流語言少
Alire 的套件數量跟主流語言差了一個量級
人才與資訊較少
尤其中文資訊特別少
在團隊開發中導入,需要預留教育成本
語法容易讓人覺得冗長
型別宣告與規格/實作分離,對小型腳本來說顯得笨重
不適合「先跑起來再說」這種用途
求職市場有限
偏向航太、國防、鐵路等領域
而且歷史也告訴我們,「用了 Ada 就安全」並不是這麼單純的事。
1996 年 Ariane 5 火箭首航爆炸事故,其原因之一就是用 Ada 寫的軟體。
把為 Ariane 4 寫的程式碼,直接重用在飛行特性不同的 Ariane 5 上,結果轉換時遇到超出預期範圍的大數值,引發了 Constraint_Error,卻沒有被妥善處理,導致系統停止。
這個事故揭示的是:
語言的執行期檢查確實檢測出了問題(沒有悄悄壞掉)
但運作前提改變了卻沒有被重新驗證
例外發生後的設計(容錯機制)並不充分
型別系統與契約,都無法取代重新檢視前提假設的流程。
語言只是安全工程的一部分,不是全部。
我認為,這是學習 Ada 時最誠實的一則警語。
20. 長生命週期軟體與 Ada —— 從維護的角度看
本站經常討論 Windows 既有資產的維護與延壽議題。
從這個角度來看,Ada 有另一種魅力。
用 Ada 寫成的系統,以數十年為單位持續運作的並不少見。
而且,Ada 的語言設計本身,就是以長期維護為前提的。
規格(.ads)與實作(.adb)分離
-> 20 年後的維護者,只要讀規格就能掌握介面
強型別與範圍限制
-> 隱含的前提會留在程式碼裡,不用靠口頭傳承或註解
契約(Pre/Post)
-> 「這個函式的約定」以可驗證的形式留存下來
case 的完整性檢查
-> 規格變更時受影響的位置,編譯器會幫你列出來
標準修訂也重視向後相容
-> 大多數 Ada 83 的程式碼,在現代編譯器上依然能通過
這些觀念,在用 C# 或 C++ 做長期維護時,也能直接當成設計方針借用:
不要用 int,而是定義有意義的型別(表示 ID 的型別、帶有單位的型別)
設計成無法產生不合法值的型別(在建構子中做驗證)
有意識地把公開介面與實作分離
用斷言(assertion)或測試來表達事前條件、事後條件
把列舉型別的 switch 寫得完整,並把警告當成錯誤處理
即使工作上沒有機會用到 Ada,學習 Ada 的設計理念仍然非常有價值。
作為學習「用型別闡述設計」這種感覺的教材,Ada 至今仍是一流的選擇。
21. 總結
我們整理了 Ada 的魅力,回顧一下重點:
Ada 是在高可靠性系統中已使用超過 40 年的現役語言
名稱源自 Ada Lovelace,最新標準是 Ada 2022
結構相同但名稱不同的型別,是不同的型別。單位搞混會變成編譯錯誤
透過範圍限制,可以在型別層級防止不合法的值
陣列會做邊界檢查,緩衝區溢位不會變成未定義行為
用套件分離規格與實作,用引數模式明確標示資料流向
泛型會在規格中寫明所要求的操作,因此使用時的錯誤很明確
Ada 2012 的契約(Pre/Post),能讓規格以可驗證的形式留在程式碼中
任務與保護物件,能讓並行處理以安全的語言功能來撰寫
用了 SPARK,就能把契約從執行期檢查升級為數學證明
有了 GNAT 與 Alire,免費在 Windows 上就能立刻試用
生態系規模小、人才少是它的弱點
語言的安全機制,無法取代重新檢視前提假設的流程
就流行程度而言,Ada 並沒有成為主流語言。
但 null 安全、完整性檢查、契約、接近所有權概念的嚴格性,這些現代語言當作「新功能」引進的東西,Ada 幾十年前就已經具備了。
Ada 的本質,可以用一句話概括:
bug 不是用來找出來的,而是用型別與契約讓它「寫不出來」的東西。
週末找個時間,用 Alire 建立一個專案,試著在被編譯器唸的過程中寫一支小程式看看。
當你發現,那一個個編譯錯誤,都是「在變成生產環境事故之前就被抓住的 bug」時,你應該就能體會到 Ada 的魅力所在。
參考資料
- 本文程式碼片段依章節整理的參考用程式碼集 - komurasoft-blog-samples (GitHub)
- Ada Programming Language - AdaCore
- Learn Ada - AdaCore (learn.adacore.com)
- Introduction to Ada - learn.adacore.com
- Ada Reference Manual (Ada 2022)
- Alire - Ada Library Repository
- GNAT User’s Guide - GCC
- SPARK - AdaCore
- Introduction to SPARK - learn.adacore.com
- Ada Conformity Assessment Authority
- Ariane 501 Inquiry Board Report (ESA)
相關文章
共用相同標籤的最新文章。能以相近的主題延伸理解。
Ada 的泛型程式設計 ── 以型別撰寫契約,零成本達成程式碼重用
系統性說明 Ada 的泛型程式設計,涵蓋泛型子程式、泛型套件、形式子程式參數、型別類別、正式套件參數,以及實務上的設計方針。搭配 Mermaid 圖與實例,整理型別安全的重用與零成本抽象化的思路。
用 Ada 打造即時系統程式設計 ── 優先權、週期、執行時間控制實戰
本文透過 8 個實戰程式碼範例,逐步學習 Ada Annex D(即時系統)所提供的即時功能──任務優先權、Ceiling_Locking 協定、delay until 的週期執行、Ravenscar 設定檔、計時事件、保護佇列、依任務量測執行時間、多週期整合。
Ada 的安全並行處理 ── 任務與保護物件實戰指南
本文是 Ada 語言內建並行處理機制──任務(task)與保護物件(protected object)的實戰入門文章。內容涵蓋會合(entry/accept)、選擇性接受(select)、生產者消費者模式、保護物件實現的排他控制、帶屏障的保護入口、附逾時的呼叫,以及任務優先...
SPARK形式驗證入門 ── 從Ada的契約到數學證明
本文是使用Ada子集語言SPARK進行形式驗證的實務入門文章,整理從契約(Pre/Post)進階到證明的方法、GNATprove的使用方式、迴圈不變條件、資料流契約、證明等級,以及在實際專案中導入的方法。
用 PerfView 與 dotnet-trace 找出「變慢」的原因 ── .NET 效能調查實務入門
當商用應用程式「變慢」「CPU 卡住不動」「偶爾當掉」時,該用哪個工具看什麼?本文整理 PerfView 與 dotnet-trace 的角色分工、CPU 取樣的讀法(inclusive/exclusive)、用 ThreadTime 調查阻塞時間,以及與 EventSou...
相關主題
與本文相近的主題頁面。以本文為起點,可進一步連到相關服務與其他文章。
Windows 技術主題
彙整 KomuraSoft LLC 關於 Windows 開發、故障調查與既有資產活用文章的主題中心。
常見問題
整理諮詢這個主題時常見的問題。
- Ada 語言現在還有人在用嗎?
- 有,而且仍在持續使用。民航機的飛行控制、航空管制、鐵路的號誌與保安系統、火箭與人工衛星、國防系統、醫療器材等,這些一旦出錯就會直接關係到人命或造成巨額損失的高可靠性系統中,Ada 已經被使用了數十年之久。Ada 是一門持續修訂超過 40 年的語言,從 1983 年的 Ada 83 開始,經過 Ada 95、Ada 2005、Ada 2012,最新標準是 Ada 2022。
- Ada 語言的強型別跟其他語言有什麼不同?
- 在 Ada 中,即使結構完全相同,用不同名稱宣告的型別也會被視為不同型別。例如同樣以 Float 建立 Meters 型別與 Seconds 型別,混用時會出現編譯錯誤,轉換必須明確寫出來。此外,subtype 還能讓型別帶有數值範圍限制(例如 0~100),違反時會在執行期產生 Constraint_Error 例外。這種設計不是靠『小心一點』來防止像單位搞混這類錯誤,而是讓『根本編譯不過』來防止。
- 要免費體驗 Ada 語言該怎麼做?
- 使用 GNAT(GCC 內建的免費 Ada 編譯器)與 Alire(Ada 的套件管理工具兼建置工具,指令名稱 alr),在 Windows、Linux、macOS 上都能免費建置完整的開發環境。從 Alire 官方網站取得安裝程式後,用 alr init --bin 建立雛形專案、alr build 建置、alr run 執行,體驗上很接近 Rust 的 cargo。工具鏈本身也由 Alire 負責取得,因此不需要手動安裝編譯器。VS Code 也有 AdaCore 製作的 Ada 擴充功能。
- Ada 語言的弱點是什麼?
- 生態系規模小,Web 框架、GUI、雲端 SDK 等選擇比主流語言少;人才與資訊(尤其是中文資訊)較少,導入團隊需要預留教育成本;型別宣告與規格/實作分離對小型腳本來說顯得笨重;求職市場也偏向航太、國防、鐵路等領域。此外,正如 1996 年的 Ariane 5 事故所顯示的,語言的安全機制無法取代重新檢視前提假設的流程。
作者檔案
本文作者的個人檔案頁面。
Go Komura
小村軟體有限公司 代表
以 Windows 軟體開發、技術諮詢與故障調查為中心,在難以重現的故障調查與既有資產仍在運作的專案上具有優勢。