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

1. 먼저 잡아 둘 것

Ada라는 언어 이름을 들어 본 적이 있습니까?

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

그러나 Ada는 지금도 현역 언어입니다.

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

Ada를 이해할 때 중요한 것은 다음 관점입니다.

Ada는 「버그를 실행 전에 없애는」 데 전력을 기울인 언어이다
타입은 데이터를 담는 그릇이 아니라, 설계 의도를 표현하는 도구이다
명세와 구현의 분리, 계약, 병행 처리가 언어에 내장되어 있다
유행하지는 않았지만, 설계 사상은 현대 언어에 이어져 있다

이 기사에서는 Ada의 역사, 구문, 강한 타입 시스템, 범위 제약, 패키지, Design by Contract, task, SPARK, 개발 환경, 그리고 약점까지 Ada의 매력을 정리합니다.

평소 C#, C++, Java 등을 쓰는 분이 「타입으로 설계를 말한다」는 감각을 가져갈 수 있도록 하는 것이 목표입니다.

전체 21장으로 길기 때문에, 먼저 지도를 둡니다.

이 기사의 구성:
  1~3장    Ada란 무엇인가, 역사, 어디에서 쓰이는가
  4~5장    첫걸음(Hello, World)과, 가독성을 우선한 구문
  6~11장   타입 시스템: 강한 타입 시스템, 범위 제약, 배열, 패키지, 레코드, 제네릭
  12~13장  예외 처리와 Design by Contract(Pre/Post)
  14~15장  병행 처리: task와 protected object
  16~17장  SPARK에 의한 형식 검증과 C/C++ 상호운용
  18장      개발 환경(GNAT과 Alire)
  19~21장  약점과 주의점, 장수명 소프트웨어에서 본 가치, 정리

먼저 돌려 보고 싶은 분은 4장과 18장, 설계 사상만 잡고 싶은 분은 1·6·7·13장을 골라 읽어도 맥락이 이어지도록 썼습니다.

또한 이 기사에 나오는 코드 조각은, 장별로 파일에 정리한 참조용 코드 모음으로 GitHub에 공개하고 있습니다.

ada-language-appeal - komurasoft-blog-samples (GitHub)

그림의 실선은 항상 성립하는 관계, 점선은 조건이 붙는 관계입니다(성립 조건은 상세 페이지의 관계별 설명에 적혀 있습니다). 관계 전체 목록(총 18건, 근거와 확신도 포함)과 주요 개념의 정의는 지식 맵 상세 페이지에 정리되어 있습니다(일본어). 데이터: JSON-LD / Turtle

2. Ada란 무엇인가 ── 이름의 유래와 역사

Ada는 1970년대 후반에 미국 국방부(DoD) 주도로 태어난 범용 프로그래밍 언어입니다.

당시 국방부는 프로젝트마다 제각각인 언어가 쓰여, 소프트웨어 유지보수 비용이 부풀어 오르는 문제를 안고 있었습니다.

그래서 임베디드 시스템이나 실시간 시스템에도 쓸 수 있는 표준 언어를, 국제 설계 공모로 선정했습니다.

채택된 것은 Jean Ichbiah가 이끈 팀의 설계안입니다.

언어 이름 Ada는 세계 최초의 프로그래머로 불리는 Ada Lovelace(오거스타 에이다 킹, 러브레이스 백작 부인)에서 유래합니다.

Ada의 역사를 대략 정리하면 다음과 같습니다.

1980년 MIL-STD-1815로 최초의 사양이 제정된다
1983년 Ada 83(ANSI 표준)
1987년 ISO 표준이 된다
1995년 Ada 95(객체지향, protected object 도입)
2005년 Ada 2005(인터페이스, 컨테이너 라이브러리 확충)
2012년 Ada 2012(Design by Contract를 언어 기능으로 도입)
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;

이 코드는 저장한 뒤 바로 실행할 수 있습니다. Ada의 대표적인 처리계는 GNAT(GCC에 포함되는 무상의 Ada 컴파일러. 이 기사의 코드 예 컴파일 옵션도 GNAT의 것입니다)이며, 빌드와 실행은 두 줄입니다.

gnatmake hello.adb   -> 실행 파일 hello (Windows에서는 hello.exe) 가 생성된다
./hello              -> Hello, Ada!

파일 이름은 「유닛 이름을 소문자로 한 것 + .adb」로 하는 규칙입니다(procedure Hello라면 hello.adb). GNAT 본체 입수 방법과, 패키지 매니저 Alire를 쓰는 한 단계 더 쉬운 절차는 18장에 정리해 두었습니다. 먼저 환경을 만들어 손을 움직여 보고 싶은 분은, 지금 18장으로 건너뛰어도 됩니다.

처음에 눈에 들어오는 것은 다음 점일 것입니다.

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계 언어 같은 암묵적 fall-through는 없다
범위(Mon .. Fri)나 선택지(Sat | Sun)로 조건을 묶을 수 있다

열거형에 값을 추가하면, 망라하지 않은 case 문이 모두 컴파일 에러가 됩니다.

「사양 변경의 영향 범위를 컴파일러가 열거해 준다」는 경험은, 한 번 맛보면 놓기 어려워집니다.

또한 인자에는 이름 있는 연관(named association)을 쓸 수 있습니다.

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부터는 임의의 조건을 술어(predicate)로 붙일 수 있습니다.

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

고정소수점 타입처럼 하드웨어 제어용 타입도 언어에 들어 있습니다.

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

많은 언어에서는 잘못된 값 검사가 다음과 같이 되기 쉽습니다.

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

Ada에서는 「이 타입의 값인 시점에서 범위는 이미 보장된다」고 말할 수 있습니다.

validation 책임이 데이터 타입으로 옮겨지면, 함수 로직은 본래 일에 집중할 수 있습니다.

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의 모듈 시스템은 패키지입니다.

패키지는 명세(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. 레코드와 discriminant

Ada의 구조체에 해당하는 것이 레코드입니다.

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);

discriminant는 레코드의 「모양」을 정하는 매개변수입니다.

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의 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  범위 제약 위반, 배열 경계 위반, 0 나누기 등
Program_Error     언어 규칙 위반(도달해서는 안 되는 곳에 도달하는 등)
Storage_Error     메모리 부족
Tasking_Error     task 간 통신 실패

주목하고 싶은 것은, 범위 제약이나 경계 검사 위반이 모두 이 예외 처리 체계에 통합되어 있다는 점입니다.

「타입에 적은 제약」이 깨지면 Constraint_Error가 된다.

즉 7장에서 본 범위 제약은 자동 생성되는 런타임 assertion으로 기능합니다.

직접 if 문 검사 코드를 흩뿌릴 필요가 없습니다.

13. Design by Contract ── 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. task ── 병행 처리가 언어에 내장되어 있다

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

C/C++가 스레드를 OS 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를 선언하면, 감싸고 있는 블록의 시작과 동시에 병행 실행이 시작됩니다.

그리고 중요한 것은 블록은 내부 task가 모두 끝날 때까지 종료하지 않는다는 점입니다.

「스레드의 join을 잊어 프로세스 종료 때 이상한 일이 생긴다」는 종류의 버그가 구조적으로 일어나지 않습니다.

task 간 동기에는 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");처럼, 프로시저 호출과 같은 형태로 쓸 수 있습니다.

메시지 패싱에 의한 task 간 통신을, 락 지식 없이 쓸 수 있습니다.

실시간 시스템용으로는 스케줄링 방침이나 우선순위 제어, 나아가 검증하기 쉽도록 task 기능을 제한하는 Ravenscar 프로파일까지 표준화되어 있습니다.

15. protected object ── 배타 제어를 타입으로 쓴다

공유 데이터의 배타 제어에는 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;

protected object의 데이터에는 정의한 조작을 통해서만 접근할 수 있습니다.

그리고 배타 제어는 언어가 보증합니다.

procedure  읽기 쓰기 가능, 배타적으로 실행된다
function   읽기 전용, 여러 task의 동시 실행을 허용한다
entry      조건(배리어)을 만족할 때까지 호출 측을 기다리게 할 수 있다

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

이 데이터를 건드릴 때는 이 mutex를 잡을 것
락 해제를 잊지 말 것
락 순서를 지킬 것

Ada의 protected object에서는 「락을 잡는 것을 잊은 코드」를 애초에 쓸 수 없습니다.

데이터와, 그것을 지키는 배타 제어가 하나의 타입으로 선언되기 때문입니다.

entry의 배리어 조건을 쓰면 「큐에 데이터가 들어올 때까지 기다린다」 같은 조건 동기도, 플래그나 조건 변수를 손으로 관리하지 않고 쓸 수 있습니다.

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와의 상호운용이 언어 사양 부속서 B(Annex B ── Ada 참조 매뉴얼 ARM의 “Interface to Other Languages”, C나 Fortran 등 다른 언어와의 인터페이스를 정한 부속서)에서 표준화되어 있습니다.

예를 들어 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 로켓 1호기 폭발 사고는, Ada로 쓰인 소프트웨어가 원인 중 하나였습니다.

Ariane 4용으로 쓰인 코드를, 비행 특성이 다른 Ariane 5에 재사용한 결과, 예상 밖의 큰 값이 변환 시에 Constraint_Error를 일으켰고, 적절히 처리되지 않은 채 시스템이 정지했습니다.

구체적 경위는 이렇습니다. 관성 기준 장치(SRI) 안에, 이륙 전 위치 맞춤용으로 계산되는 BH(Horizontal Bias, 수평 방향 속도와 관련된 내부 값)를 64비트 부동소수점에서 16비트 부호 있는 정수로 변환하는 처리가 있었습니다. Ariane 5의 비행 경로는 Ariane 4의 약 5배의 수평 속도를 내기 때문에, BH는 16비트로 나타낼 수 있는 범위를 넘어 변환이 실패했습니다(조사 보고서 용어로는 「오퍼랜드 에러」, Ada의 범위 검사로서는 범위 밖 변환에 해당합니다). 게다가 이 변환은 보호되어 있지 않았습니다. SRI 계산기에 「최대 부하 80%」라는 목표가 있었기 때문에, 위험이 있는 7개 변수 중 보호된 것은 4개이고, 나머지 3개는 「물리적으로 제한되거나, 충분한 여유가 있다」고 판단해 보호를 빼 두었습니다. BH에 대해서는 그 판단이 Ariane 5에서는 더 이상 성립하지 않게 되어 있었습니다.

이 사고가 보여 주는 것은 다음입니다.

언어의 런타임 체크는 문제를 검출했다(조용히 망가지지는 않았다)
그러나 운용 전제가 바뀌었는데도 검증되지 않았다
예외 발생 후의 설계(fail-safe)가 불충분했다

타입 시스템도 계약도, 전제를 다시 검토하는 프로세스를 대신하지 않습니다.

언어는 안전 공학의 일부이지, 전부가 아니다.

이것은 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)으로, 명세를 검증 가능한 형태로 코드에 남길 수 있다
task와 protected object로, 병행 처리를 언어 기능으로서 안전하게 쓸 수 있다
SPARK를 쓰면, 계약을 런타임 체크에서 수학적 증명으로 격상할 수 있다
GNAT과 Alire로, 무상으로 Windows에서도 바로 써 볼 수 있다
에코시스템의 작음과 인력의 적음이 약점
언어의 안전 장치는, 전제를 다시 검토하는 프로세스를 대신하지 않는다

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

그러나 null safety, 망라성 검사, 계약, 소유권에 가까운 엄격함처럼, 현대 언어가 「신기능」으로 넣고 있는 것의 상당수를 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 언어의 약점은 무엇인가요?

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

저자 프로필

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

Go Komura

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

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