Ada 언어의 매력 —— 타입으로 설계를 말하고, 수십 년간 동작하는 소프트웨어를 지탱하는 언어

1. 먼저 짚어둘 것

Ada라는 언어의 이름을 들어본 적이 있으신가요?

「옛날 언어」, 「군용 언어」, 「수업에서 이름만 들어봤다」는 인상을 가진 분이 많을지도 모릅니다.

하지만 Ada는 지금도 현역인 언어입니다.

항공기의 비행 제어, 철도의 신호 시스템, 로켓, 항공 관제, 인공위성, 의료 기기 등 멈추면 인명에 직결되는 소프트웨어의 세계에서, Ada는 수십 년에 걸쳐 계속 사용되고 있습니다.

Ada를 이해할 때 중요한 것은 다음과 같은 시각입니다.

Ada는 "버그를 실행 전에 없애는" 데 온 힘을 쏟은 언어이다
타입은 데이터를 담는 그릇이 아니라, 설계 의도를 표현하는 도구이다
사양과 구현의 분리, 계약, 병행 처리가 언어에 내장되어 있다
유행하지는 않았지만, 설계 사상은 현대 언어에 계승되고 있다

이 글에서는 Ada의 역사, 문법, 강한 타입, 범위 제약, 패키지, 계약에 의한 설계, 태스크, 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)이 요구되는 시스템입니다.

민간 항공기의 비행 제어나 항공 전자기기
항공 관제 시스템
철도의 신호·보안 시스템
로켓·인공위성
방위 시스템
의료 기기
금융이나 산업의 일부 기간 시스템

이 분야들에는 공통되는 특징이 있습니다.

버그가 인명이나 막대한 손실로 직결된다
인증이나 심사에서 "정당성의 근거"를 요구받는다
한번 배포하면 수십 년 동안 계속 사용한다
나중에 수정하는 비용이 극도로 높다

「릴리스하고 나서 고치면 된다」는 사고방식이 통하지 않는 세계입니다.

Ada의 언어 설계는 바로 이 요구에 응답하기 위한 것입니다.

컴파일 시점에 발견할 수 있는 버그는 컴파일 시점에, 실행 시점에서만 발견할 수 있는 것은 실행 시 검사로, 더 나아가 수학적으로 증명할 수 있는 것은 증명으로 없앤다는 사상이 언어 전체를 관통하고 있습니다.

이 사상은 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 계열 언어와 같은 암묵적인 폴스루는 존재하지 않는다
범위(Mon .. Fri)나 선택지(Sat | Sun)로 조건을 묶을 수 있다

열거형에 값을 추가하면, 망라하지 않은 case문이 전부 컴파일 오류가 됩니다.

「사양 변경의 영향 범위를 컴파일러가 나열해준다」는 경험은, 한번 맛보면 손을 놓을 수 없게 됩니다.

또한 인수에는 이름 붙은 연결(named association)을 사용할 수 있습니다.

Draw_Rectangle (Left => 10, Top => 20, Width => 100, Height => 50);

인수를 혼동하는 것을 방지하고, 호출하는 쪽의 코드가 그대로 문서가 됩니다.

대입은 :=, 비교는 =이며, C 계열 언어의 if (a = b)와 같은 혼동은 문법 수준에서 일어나지 않습니다.

6. 강한 타입 —— 단위 혼동을 컴파일 오류로 만든다

Ada의 가장 큰 매력은 강한 타입(strong typing)입니다.

많은 언어에서 「강한 타입」이라는 말이 사용되지만, 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부터는 임의의 조건을 술어(predicate)로 붙일 수 있습니다.

subtype Even is Integer
  with Dynamic_Predicate => Even mod 2 = 0;

고정소수점 타입과 같은, 하드웨어 제어를 위한 타입도 언어에 내장되어 있습니다.

type Temperature is delta 0.1 range -50.0 .. 150.0;

많은 언어에서는, 부정한 값의 검사가 다음과 같이 되기 쉽습니다.

함수 맨 앞에서 if문에 의한 검증
검사 누락은 코드 리뷰에 의존
어느 함수가 검사를 마친 값을 받는지 불명확

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)라는 2개의 파일로 나뉩니다.

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에서 흔히 발생하는 버그의 입구가 처음부터 존재하지 않습니다.

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의 트레잇 바운드가 해결하려 했던 문제에, 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  범위 제약 위반, 배열 경계 위반, 0으로 나누기 등
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 위반  -> 호출하는 쪽의 버그
Post 위반 -> 구현하는 쪽의 버그

문서 주석에 「이 함수는 빈 스택에 대해 호출해서는 안 된다」라고 적는 것과, 무엇이 다를까요.

주석은 구현과 어긋나도 아무도 알아채지 못한다
계약은 컴파일러가 문법과 타입을 검사한다
계약은 실행 시에 자동으로 검증할 수 있다
계약은 SPARK에 의한 정적 증명의 입력이 된다(16장)

사양이, 검증 가능한 형태로 코드 안에 존재한다.

이것이 Ada 2012 이후의 세계입니다.

타입 불변조건(Type_Invariant)을 사용하면, 「이 타입의 값은 항상 이 성질을 만족한다」는 제약도 적을 수 있습니다.

14. 태스크 —— 병행 처리가 언어에 내장되어 있다

Ada의 또 하나의 큰 매력은, 병행 처리가 언어 사양의 일부라는 것입니다.

C/C++가 스레드를 OS의 API나 라이브러리(pthread, std::thread)에 의존하는 것과 달리, Ada는 1983년 시점에 이미 태스크를 언어에 내장하고 있었습니다.

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을 잊어버려서 프로세스 종료 시에 이상한 일이 일어난다」는 부류의 버그가, 구조적으로 일어나지 않습니다.

태스크 간의 동기화에는, 랑데부(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 프로파일까지 표준화되어 있습니다.

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)을 만족할 때까지 호출하는 쪽을 대기시킬 수 있다

많은 언어에서의 배타 제어는, 다음과 같은 규율에 의존하기 쉽습니다.

이 데이터를 다룰 때는 이 뮤텍스를 잡을 것
락 해제를 잊지 말 것
락의 순서를 지킬 것

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)는, 이 코드에 대해 다음과 같은 것을 실행하지 않고 증명합니다.

오버플로가 발생하지 않는다는 것
범위 제약 위반이 발생하지 않는다는 것
0으로 나누기가 발생하지 않는다는 것
초기화되지 않은 변수를 읽지 않는다는 것
Pre와 Post의 정합성

테스트와의 차이는 결정적입니다.

테스트  선택한 입력에 대해 올바르게 동작함을 확인한다
증명    모든 입력에 대해 성질이 성립함을 보인다

13장에서 본 계약(Pre/Post)은, SPARK에서는 그대로 증명의 대상이 됩니다.

실행 시 검사로 적은 계약을, 나중에 「증명된 것」으로 승격시킬 수 있는 것입니다.

SPARK는 항공·방위 세계에서 실적을 쌓아왔지만, 최근에는 NVIDIA가 펌웨어의 보안을 위해 채택하는 등, 산업계에서의 활용이 넓어지고 있습니다.

「정형 기법은 학술적이어서 실무에서는 쓸 수 없다」는 통설을, Ada/SPARK의 에코시스템은 조용히 계속 뒤집고 있습니다.

17. C, C++와의 상호 운용

Ada는 고립된 언어가 아닙니다.

C와의 상호 운용이 언어 사양(Annex B)으로 표준화되어 있습니다.

예를 들어, Windows API의 Sleep을 Ada에서 호출하려면, 다음과 같이 작성합니다.

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에서 호출할 수 있는 함수로 공개할 수 있습니다.

즉, 다음과 같은 단계적인 사용 방법이 가능합니다.

기존 C 라이브러리를 Ada에서 이용한다
시스템의 핵심 부분만 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에도 약점이 있습니다.

공정하게 정리해 두겠습니다.

에코시스템이 작다
  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를 나타내는 타입, 단위를 가진 타입)을 정의한다
부정한 값을 만들 수 없는 타입을 설계한다(생성자에서의 검증)
공개 인터페이스와 구현을 의식적으로 분리한다
사전조건・사후조건을 어서션이나 테스트로 표현한다
열거형의 switch를 망라적으로 작성하고, 경고를 오류로 취급한다

Ada를 업무에서 사용할 기회가 없더라도, Ada의 설계 사상을 배우는 것에는 충분한 가치가 있습니다.

「타입으로 설계를 말하는」 감각을 배우는 교재로서, Ada는 지금도 최고 수준입니다.

21. 정리

Ada의 매력을 정리해 왔습니다.

포인트를 되돌아보겠습니다.

Ada는 고신뢰 시스템에서 40년 이상 계속 사용되고 있는 현역 언어이다
이름은 Ada Lovelace에서 유래했으며, 최신 표준은 Ada 2022이다
구조가 같아도 이름이 다른 타입은 서로 다른 타입이다. 단위 혼동이 컴파일 오류가 된다
범위 제약에 의해, 부정한 값을 타입 수준에서 방지할 수 있다
배열은 경계 검사가 이루어지며, 버퍼 오버런이 미정의 동작이 되지 않는다
패키지로 사양과 구현을 분리하고, 인수 모드로 데이터의 흐름을 명시한다
제네릭은 요구하는 연산을 사양에 적기 때문에, 사용 시의 오류가 명확하다
Ada 2012의 계약(Pre/Post)으로, 사양을 검증 가능한 형태로 코드에 남길 수 있다
태스크와 보호 객체에 의해, 병행 처리를 언어 기능으로 안전하게 작성할 수 있다
SPARK를 사용하면, 계약을 실행 시 검사에서 수학적 증명으로 승격시킬 수 있다
GNAT와 Alire에 의해, 무상으로 Windows에서도 곧바로 시험해볼 수 있다
에코시스템의 작음과 인력의 부족이 약점이다
언어의 안전 장치는, 전제를 재검토하는 프로세스를 대신할 수 없다

Ada는 유행이라는 의미에서는 주류가 되지 못한 언어입니다.

하지만 null 안전, 망라성 검사, 계약, 소유권에 가까운 엄격함과 같이, 현대 언어가 「신기능」으로 도입하고 있는 것들의 대부분을, Ada는 수십 년 전부터 갖추고 있었습니다.

Ada의 본질은, 다음 한마디로 정리할 수 있습니다.

버그는 찾아내는 것이 아니라, 타입과 계약으로 “작성할 수 없게 만드는” 것.

주말에 Alire로 프로젝트를 하나 만들어, 컴파일러에게 혼나면서 작은 프로그램을 작성해 보세요.

그 컴파일 오류 하나하나가, 「실제 장애가 되기 전에 잡아낸 버그」라는 것을 깨달았을 때, 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는 40년 이상 계속 개정되고 있는 언어로, 1983년의 Ada 83에서 시작해 Ada 95, Ada 2005, Ada 2012를 거쳐 최신 표준은 Ada 2022입니다.

Ada 언어의 강한 타입은 다른 언어와 무엇이 다른가요?

Ada에서는 구조가 완전히 같아도 다른 이름으로 선언한 타입은 서로 다른 타입으로 취급됩니다. 예를 들어 Meters 타입과 Seconds 타입을 모두 Float로부터 만들었다고 해도, 이를 섞어서 사용하면 컴파일 오류가 발생하며 변환은 명시적으로 작성해야 합니다. 또한 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 언어의 약점은 무엇인가요?

에코시스템이 작아서 웹 프레임워크, GUI, 클라우드 SDK 등의 선택지가 주류 언어보다 적다는 점, 인력과 정보(특히 한국어 정보)가 적어 교육 비용을 감안해야 한다는 점, 타입 선언이나 사양/본체 분리가 작은 스크립트에는 무겁게 느껴진다는 점, 채용 시장이 항공우주·방위·철도 등에 편중되어 있다는 점을 들 수 있습니다. 또한 1996년의 Ariane 5 사고가 보여주듯, 언어의 안전 장치가 전제를 재검토하는 프로세스를 대신할 수는 없다는 점에도 주의가 필요합니다.

저자 프로필

기사 저자의 프로필 페이지입니다.

Go Komura

합동회사 코무라소프트 대표

Windows 소프트웨어 개발, 기술 상담, 장애 조사를 중심으로 재현이 어려운 장애 조사와 기존 자산이 남아 있는 프로젝트에 강점이 있습니다.