SPARK란 무엇인가요? Ada와는 어떤 관계인가요?

SPARK는 Ada의 서브셋(부분 언어)으로, 프로그램의 성질을 수학적으로 증명할 수 있도록 설계되어 있습니다. 포인터를 이용한 동적 메모리 관리나 자유로운 예외 사용 등을 제한하는 대신, 증명 가능성을 얻고 있습니다. SPARK 코드는 Ada 코드에 계약 주석을 추가한 것이므로, 평소의 Ada 개발의 연장선에 있으며 특별한 문법을 새로 익힐 필요는 없습니다. 도구는 AdaCore가 제공하는 GNATprove가 중심이며, 계약을 Why3 중간 언어로 변환한 뒤 Z3 등의 자동 증명기로 증명을 시도합니다.

형식 검증은 테스트와 무엇이 다른가요?

테스트는 「선택한 입력에 대해 올바르게 동작하는지」를 확인하는 반면, 형식 검증은 「모든 입력에 대해 성질이 성립하는지」를 수학적으로 증명합니다. 입력의 조합은 무한하기 때문에, 테스트만으로는 모든 입력에서의 정확성을 보일 수 없습니다. 다만 둘은 대립하는 것이 아니라 서로 보완하는 관계이며, SPARK로 Silver 레벨(런타임 오류 없음)을 보증하고, 단위 테스트로 구체적인 입출력을 확인하고, 증명할 수 없는 부분에 집중적으로 테스트를 작성하는 병행 사용이 실용적입니다.

SPARK의 증명 레벨(Stone~Platinum)이란 무엇인가요?

단계적으로 증명의 엄격함을 높여가기 위한 개념입니다. Stone은 계약의 문법과 타입의 일관성 검사만, Bronze는 초기화되지 않은 변수를 읽지 않는다는 증명, Silver는 런타임 오류(범위 초과, 오버플로, 0으로 나누기)가 발생하지 않는다는 증명, Gold는 Pre/Post 조건의 증명을 통한 완전한 기능적 정당성, Platinum은 여기에 더해 정보 흐름의 증명까지 포함한 보안 중시 레벨입니다. 실무에서는 우선 Silver 레벨을 목표로 하는 것이 가장 실용적인 목표로 여겨집니다.

GNATprove로 증명할 수 없을 때는 어떻게 해야 하나요?

메시지별로 대응합니다. 「postcondition might fail」은 Post 조건이 너무 강하거나 Pre 조건이 너무 약한 경우, 혹은 루프 불변조건이 부족한 것이 원인입니다. 「overflow check might fail」은 Pre 조건으로 값의 범위를 제한하거나 타입 자체의 범위를 좁힙니다. 「array index check might fail」은 루프 범위가 배열 범위 안에 있음을 불변조건으로 보여줍니다. 「prover timeout」은 불변조건으로 증명을 단계적으로 나누거나 함수를 더 작게 분할합니다. 정말로 실패할 수 있는지 코드를 읽고 판단하는 것이 첫 단계입니다.

SPARK를 이용한 형식 검증 입문 —— Ada의 계약에서 수학적 증명으로

2026년 06월 13일 00:00 · 小村豪 · Ada, SPARK, FormalVerification, GNATprove, DesignByContract, HighIntegrity, ProgrammingLanguage, 형식검증, 고신뢰성

1. 시작하며 —— 「실행해서 확인한다」의 다음 단계로

소프트웨어의 품질을 보증하는 방법으로 가장 일반적인 것은 테스트입니다.

테스트: 선택한 입력에 대해 올바르게 동작하는지 확인한다

하지만 테스트에는 한계가 있습니다. 입력의 조합은 무한하며, 「모든 입력에서 올바르다」는 것은 테스트만으로는 보일 수 없습니다.

여기서 등장하는 것이 형식 검증(Formal Verification)입니다.

형식 검증: 모든 입력에 대해 성질이 성립함을 수학적으로 증명한다

지난 글 「Ada 언어의 매력」에서는 Ada의 전체적인 모습을 소개하고, SPARK에 대해서도 간단히 다루었습니다.

이 글에서는 SPARK를 이용한 형식 검증의 실전에 초점을 맞춰, 다음 내용을 정리합니다.

SPARK란 무엇인가. Ada와의 관계는 어떻게 되어 있는가
계약(Pre/Post)을 어떻게 작성하는가
GNATprove로 어떻게 증명하는가
루프 불변조건을 어떻게 설계하는가
데이터 흐름 계약(Global/Depends)으로 부작용을 관리하는 방법
증명 레벨(Stone~Platinum)의 단계적 적용 전략
실제 프로젝트에 적용하는 방법

테스트에서 증명으로 단계를 밟아가는 과정을, 실제 코드 예제와 함께 체험할 수 있도록 하는 것을 목표로 합니다.

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

ada-spark-formal-verification - komurasoft-blog-samples (GitHub)

2. SPARK란 무엇인가 —— Ada의 부분 언어이자 증명의 세계로 가는 입구

SPARK는 Ada의 서브셋(부분 언어)입니다.

서브셋이라는 점에는 명확한 의도가 있습니다.

Ada의 모든 기능 → 표현력은 높지만, 전부를 형식 검증하는 것은 현실적이지 않다
SPARK       → 증명 가능한 기능만으로 좁혀, 증명을 현실적으로 만든다

SPARK가 제한하는 주요 항목은 다음과 같습니다.

포인터(액세스 타입)를 이용한 동적 메모리 관리 → 소유권 모델로 제어
예외 핸들러의 자유로운 사용               → 제한적으로 허용
재귀적인 데이터 구조                     → 증명이 어려워 제한
태스크의 자유로운 사용                   → Ravenscar 프로파일로 제한

「제한」이라는 말을 들으면 답답하게 느껴질 수도 있습니다. 하지만 이러한 제한은 증명 가능성과 교환해서 얻은 것입니다.

SPARK의 도구 세트는 AdaCore가 제공하는 GNATprove가 중심입니다.

GNATprove의 동작:
SPARK로 작성된 Ada 코드를 분석한다
계약(Pre/Post)이나 단정문을 Why3 중간 언어로 변환한다
Z3, CVC4, Alt-Ergo 등의 자동 증명기로 증명을 시도한다
결과를 소스 코드 상의 메시지로 보고한다

중요한 것은 SPARK가 Ada 위에 구축되어 있다는 점입니다.

SPARK 코드 = Ada 코드 + 계약 주석

즉, 평소의 Ada 개발의 연장선상에 SPARK가 있습니다. 특별한 문법을 새로 익힐 필요는 없습니다.

3. GNATprove 설치와 첫 증명

먼저 GNATprove를 동작시킬 환경을 준비합니다.

Alire를 사용하면 다음 명령으로 SPARK 대응 프로젝트를 만들 수 있습니다.

alr init --bin spark_demo
cd spark_demo

GNATprove는 GNAT 컴파일러에 동봉되어 있으므로, alr build로 빌드할 수 있는 환경이라면 그대로 gnatprove 명령을 사용할 수 있습니다.

첫 증명 대상으로, 절댓값을 반환하는 함수를 작성해 봅니다.

package Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer
     with Post => Abs_Value'Result >= 0;

end Simple_Proof;

package body Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer is
   begin
      if X < 0 then
         return -X;
      else
         return X;
      end if;
   end Abs_Value;

end Simple_Proof;

주목할 포인트를 정리합니다.

with SPARK_Mode를 패키지 규격과 본체 양쪽에 붙인다
Post 조건으로 「결과는 0 이상」이라는 성질을 선언한다
'Result 속성으로 함수의 반환값을 참조한다

이 코드에 대해 GNATprove를 실행합니다.

gnatprove -P spark_demo.gpr

결과는 다음과 같이 나옵니다.

SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved

postcondition proved라는 메시지. 이것은 모든 Integer 입력에 대해, 반환값이 0 이상임이 증명되었다는 뜻입니다.

이 경험이 SPARK의 입구입니다.

4. 계약에 의한 설계의 기초 —— Pre와 Post 작성법

SPARK의 증명은 계약을 작성하는 것에서 시작됩니다.

계약은 Ada 2012의 언어 기능이지만, SPARK에서는 그것이 증명의 입력이 됩니다.

procedure Transfer (From, To : in out Account; Amount : Positive)
  with Pre  => From.Balance >= Amount,
       Post => From.Balance = From.Balance'Old - Amount
                and then
                To.Balance = To.Balance'Old + Amount;

Pre와 Post의 설계 지침을 정리합니다.

Pre(사전조건):
  호출하는 쪽의 책임
  「이 조건을 만족하고 호출하면, Post를 보증한다」
  충분히 약하게(호출하는 쪽이 만족할 수 있는 범위에서), 필요한 만큼만 강하게

Post(사후조건):
  구현하는 쪽의 책임
  「호출 후 세계의 상태가 이렇게 되어 있다」
  'Old 속성으로 호출 전의 값을 참조할 수 있다
  너무 강하면 구현이 답답해지고, 너무 약하면 유용한 성질을 증명할 수 없다

흔히 하는 실수와 대책도 짚어둡니다.

실수1: Pre가 너무 강하다
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → 호출하는 쪽이 항상 만족할 수 있는 조건인지 확인한다
  → 테스트가 통과한다고 해서 Pre를 지나치게 좁히지 않는다

실수2: Post가 너무 약하다
  Post => True
  → 아무것도 보증하지 않는다. 증명의 의미가 없다

실수3: 부작용을 Post에 적는 것을 잊는다
  Post => Result = X * 2  (전역 변수의 갱신을 놓치고 있다)
  → Global/Depends 계약으로 부작용을 명시한다(9장)

5. 오버플로 증명 —— 수치 계산의 안전성을 보증한다

SPARK의 증명 중에서 실무적으로 가장 큰 이득을 주는 것 중 하나가 오버플로 방지입니다.

다음 코드를 봐 주세요.

procedure Increment (X : in out Integer)
  with SPARK_Mode,
       Pre  => X < Integer'Last,
       Post => X = X'Old + 1;

Pre => X < Integer'Last가 핵심입니다. 이 계약이 있으면, GNATprove는 덧셈이 오버플로하지 않음을 증명할 수 있습니다.

계약이 없는 경우, GNATprove는 오버플로 가능성을 경고합니다.

medium: overflow check might fail

더 복잡한 계산에서도 마찬가지입니다.

function Average (A, B : Integer) return Integer
  with SPARK_Mode,
       Pre  => (if A >= 0 and B >= 0 then A <= Integer'Last - B
                elsif A < 0 and B < 0 then A >= Integer'First - B),
       Post => (if A <= B then A <= Average'Result and Average'Result <= B
                else B <= Average'Result and Average'Result <= A);

Pre가 복잡해 보이지만, 이것은 「A와 B의 합이 오버플로하지 않는다」는 조건을, 부호를 고려해 경우를 나눈 것입니다.

포인트:
  오버플로 증명의 본질은, 덧셈/곱셈 전에 「결과가 타입의 범위에 들어간다」
  는 조건을 Pre로 선언하는 것
  번거로워 보이지만, 한 번 작성하면 두 번 다시 오버플로 버그에 시달리지 않는다

6. 루프 불변조건 —— 루프의 성질을 증명한다

형식 검증에서 가장 어려운 부분 중 하나가 루프의 증명입니다.

루프는 임의의 횟수만큼 실행되기 때문에, 테스트로는 모든 패턴을 커버할 수 없습니다. SPARK에서는 루프 불변조건(Loop Invariant)을 사용해 증명합니다.

function Sum_Of_Naturals (N : Natural) return Natural
  with SPARK_Mode,
       Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;

function Sum_Of_Naturals (N : Natural) return Natural is
   Result : Natural := 0;
begin
   for I in 1 .. N loop
      Result := Result + I;
      pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
   end loop;
   return Result;
end Sum_Of_Naturals;

루프 불변조건을 설계할 때는 다음과 같은 사고방식이 필요합니다.

루프의 각 반복이 시작되는 시점에 성립하는 성질을 적는다
루프의 마지막 반복 후에, 목표로 하는 Post 조건이 도출되는 것을 고른다
불변조건은, 그 시점까지의 계산 결과를 수식으로 표현한다

배열 탐색의 예도 하나 더 살펴보겠습니다.

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
  with SPARK_Mode,
       Post => (if Find'Result = 0 then
                  (for all K in Arr'Range => Arr (K) /= Target)
                else
                  Arr (Find'Result) = Target);

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
   for I in Arr'Range loop
      if Arr (I) = Target then
         return I;
      end if;
      pragma Loop_Invariant
        (for all K in Arr'First .. I => Arr (K) /= Target);
   end loop;
   return 0;
end Find;

여기서의 불변조건은 「여기까지 살펴본 범위에는 Target이 존재하지 않는다」입니다.

루프 불변조건 설계의 원칙:
  「루프를 n번 돌았을 때, 무엇을 말할 수 있는가」를 수식으로 표현한다
  배열 루프에서는 「처리 완료된 범위에 대해 ~가 성립한다」의 형태가 많다
  불변조건이 너무 강하면 증명할 수 없다. 너무 약하면 Post를 도출할 수 없다
  이 균형을 잡는 것이, 루프 증명의 진짜 실력이 드러나는 부분이다

7. Assert 프래그마 —— 코드 중간에 적는 부분적인 성질

계약(Pre/Post)에 더해, SPARK에서는 코드 중간에 단정문(Assert)을 적을 수 있습니다.

procedure Divide (A, B : Integer; Q, R : out Integer)
  with SPARK_Mode,
       Pre  => B /= 0,
       Post => A = Q * B + R and R >= 0 and R < abs (B);

procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
   Q := A / B;
   R := A rem B;

   pragma Assert (A = Q * B + R);
   pragma Assert (R >= 0);
   pragma Assert (R < abs (B));
end Divide;

프래그마의 용도를 정리합니다.

Pre/Post:      서브프로그램의 입구와 출구에서의 약속
Assert:        코드의 특정 지점에서 성립해야 하는 성질
Loop_Invariant:루프의 각 반복에서 유지되는 성질
Loop_Variant:  루프가 반드시 종료됨을 보이기 위한 감소량

Assert의 활용 장면은 다음과 같습니다.

복잡한 계산의 중간 결과 확인
if/else 분기 후의 상태 확인
프로시저 호출 후 반환값의 성질 확인
이후 증명을 위한 보조 정리(lemma)의 제공

8. 데이터 흐름 계약 —— Global과 Depends

SPARK의 강력한 기능 중 하나가 데이터 흐름 계약입니다.

서브프로그램이 읽고/쓰는 전역 변수를 명시합니다.

package Counter_Unit with SPARK_Mode is

   Count : Natural := 0;

   procedure Increment
     with Global => (In_Out => Count);

   procedure Reset
     with Global => (Output => Count);

   function Get_Value return Natural
     with Global => (Input => Count);

end Counter_Unit;

Global 계약의 모드는 다음 3가지입니다.

Input:  읽기만(함수용)
Output: 쓰기만(초기화용)
In_Out: 읽고 쓰기(갱신용)

또한, 변수 간의 의존 관계를 Depends로 표현할 수 있습니다.

procedure Transfer
  (From, To : in out Account_Type)
  with Global => (Input => Exchange_Rate),
       Depends => (From =>+ (From, Exchange_Rate),
                   To   =>+ (To, Exchange_Rate));

=>+는 「이전 값에 더해, 이 입력들에도 의존한다」는 뜻입니다.

데이터 흐름 계약의 장점:
「이 함수는 무엇을 만지는가」를 한눈에 알 수 있다
의도하지 않은 부작용을 컴파일 시점에 검출할 수 있다
변수의 정보 흐름 분석의 입력이 된다
대규모 시스템에서 데이터 흐름을 시각화하는 데 도움이 된다

9. 증명 레벨 —— Stone에서 Platinum으로 단계적으로 적용하기

SPARK에는 증명 레벨(Proof Level)이라는 개념이 있습니다.

모든 코드를 한 번에 완전히 증명하려고 하면 좌절하기 쉽습니다. 그래서 SPARK는 단계적으로 증명의 엄격함을 높여가는 전략을 제공합니다.

Stone (레벨0):
  계약의 문법과 타입의 일관성 검사만
  가장 먼저 도달해야 할 레벨

Bronze (레벨1):
  Stone + 초기화되지 않은 변수를 읽지 않는다는 증명
  기본적인 정당성의 보증

Silver (레벨2):
  Bronze + 런타임 오류(범위 초과, 오버플로, 0으로 나누기)가
  발생하지 않는다는 증명
  가장 실용적인 목표

Gold (레벨3):
  Silver + Pre/Post 조건의 증명
  완전한 기능적 정당성의 보증

Platinum (레벨4):
  Gold + 데이터의 비의존성·정보 흐름의 증명
  보안을 중시하는 시스템용

실전적인 도입 전략은 다음과 같이 됩니다.

1단계: 프로젝트 전체를 Stone 레벨로 통과시킨다
  → 계약을 잘못 작성한 부분을 찾아낸다

2단계: 중요한 모듈을 Silver 레벨로 만든다
  → 오버플로나 범위 밖 접근을 뿌리 뽑는다
  → 실무상의 버그 대부분은 여기서 막을 수 있다

3단계: 핵심 로직을 Gold 레벨로 만든다
  → 기능적 정당성을 수학적으로 보증한다
  → 알고리즘의 정확성을 증명한다

4단계: 보안 요건이 있다면 Platinum으로
  → 정보 유출 경로의 검출

10. 실전적인 증명 흐름 —— 시행착오를 줄이는 워크플로

GNATprove를 일상적으로 사용하기 위한 워크플로를 소개합니다.

1. 타입과 규격을 설계한다
   범위 제약, 타입 불변조건을 정한다

2. 계약(Pre/Post)을 작성한다
   구현 전에 규격을 계약으로 표현한다

3. 컴파일을 통과시킨다
   GNAT로 컴파일 오류를 해소한다

4. Stone 레벨에서 GNATprove를 실행한다
   gnatprove -P proj.gpr --level=0

5. 경고를 확인하고, 필요에 따라 계약을 수정한다
   특히 초기화 누락에 주의

6. Silver 레벨을 목표로 한다
   gnatprove -P proj.gpr --level=2
   런타임 오류를 뿌리 뽑는다

7. 루프가 있다면 불변조건을 추가한다
   증명할 수 없는 경우, 불변조건이 부족하지 않은지 확인한다

8. Gold 레벨에서 기능적 정당성을 증명한다
   gnatprove -P proj.gpr --level=3

흔히 겪는 「증명할 수 없는」 경우와 그 대처법입니다.

케이스1: 「medium: postcondition might fail」
  → Post 조건이 너무 강하거나, Pre 조건이 너무 약하다
  → 또는 루프 불변조건이 부족하다

케이스2: 「medium: overflow check might fail」
  → Pre 조건으로 값의 범위를 제한한다
  → 또는 타입 자체의 범위를 좁힌다

케이스3: 「medium: array index check might fail」
  → 루프 범위가 배열 범위 안에 있음을 불변조건으로 보여준다
  → for I in Arr'Range를 사용한다(SPARK가 범위의 자동 인식을 돕는다)

케이스4: 「prover timeout」
  → 증명기가 시간 초과. 불변조건으로 단계적으로 나눈다
  → 함수를 더 작게 분할한다

11. SPARK와 테스트의 병행 —— 보완 관계를 이해한다

형식 검증과 테스트는 대립하는 것이 아니라 서로 보완합니다.

SPARK의 증명:
  모든 입력에 대해 성질이 성립한다
  계약에 적은 성질만 대상이 된다
  증명할 수 없는 경우는, 수동 확인이나 테스트에 맡긴다

테스트:
  선택한 입력에 대해 실제 동작을 확인한다
  계약에 적혀 있지 않은 암묵적인 전제도 발견할 수 있다
  실행 환경과의 상호작용을 확인할 수 있다

병행 사용의 패턴입니다.

SPARK로 Silver 레벨(런타임 오류 없음)을 보증
단위 테스트로 구체적인 입출력의 정확성을 확인
Gold 레벨로 핵심 로직을 증명
증명할 수 없는 부분에 집중적으로 테스트를 작성

Ada에는 AUnit이라는 단위 테스트 프레임워크가 있습니다. SPARK로 타입과 계약을 다지고, AUnit으로 동작을 테스트하는 조합이 실전적입니다.

12. GNATprove의 결과 읽기 —— 메시지 해석

GNATprove의 출력에는 다음 3가지 레벨이 있습니다.

info:    증명에 성공했다
medium:  증명할 수 없었다(경고). 수동 확인이 필요하다
high:    증명에 실패했다(오류). 계약 위반의 가능성이 높다

흔히 보는 메시지와 그 의미입니다.

「postcondition proved」          Post 조건이 증명되었다
「range check proved」            범위 검사가 증명되었다
「overflow check proved」         오버플로하지 않음이 증명되었다
「index check proved」            배열 인덱스의 범위가 증명되었다
「divide by zero check proved」   0으로 나누는 일이 없음이 증명되었다

「might fail」                    증명할 수 없었다
「cannot prove」                  증명기가 증명을 완료하지 못했다
「prover timeout」                제한 시간 안에 증명이 끝나지 않았다

might fail이 나왔을 때의 대응 순서입니다.

정말로 실패할 수 있는지, 코드를 읽고 판단한다
실패할 수 있다면, 코드를 수정한다
실패하지 않을 것이라면, 계약(Pre/불변조건)을 강화한다
그래도 증명할 수 없다면, pragma Assume으로 가정으로 선언한다
   (다만 Assume은 증명되지 않은 가정이므로 주의)

13. 실제 프로젝트에 적용하는 방법

기존 프로젝트에 SPARK를 도입할 때의 현실적인 접근법입니다.

1. 신규 코드부터 시작한다
   기존 코드 전체를 한 번에 SPARK화하려고 하지 않는다
   새로 작성하는 모듈부터 SPARK_Mode를 활성화한다

2. Silver를 목표로 한다
   Gold(완전한 기능 증명)는 이상적이지만, Silver(런타임 오류 없음)부터 시작한다
   오버플로 방지만으로도, 실무상의 가치는 매우 크다

3. 인터페이스부터 계약을 작성한다
   구현보다 먼저, 패키지 규격(.ads)에 계약을 작성한다
   규격이 확정되어 있으면, 구현자가 누구든 계약을 만족하는 코드를 작성할 수 있다

4. CI/CD에 통합한다
   gnatprove를 CI 파이프라인에 추가한다
   증명에 실패하면 빌드를 멈춘다(또는 경고를 낸다)

5. 증명 리포트를 축적한다
   gnatprove --report=all로 리포트를 생성한다
   증명되지 않은 항목의 추이를 추적한다

C/C++ 기존 코드가 섞여 있는 프로젝트에서는 다음과 같은 단계적 접근이 유효합니다.

신규 모듈은 Ada/SPARK로 작성한다
C/C++와는 Interfaces.C를 통해 연동한다
중요한 데이터 구조와 검증 로직을 SPARK로 옮긴다
단계적으로 SPARK의 범위를 넓혀간다

14. SPARK의 한계와 주의점

SPARK도 만능은 아닙니다. 한계를 솔직하게 이해해 두는 것이 올바른 적용으로 이어집니다.

증명할 수 있는 범위:
  SPARK가 증명하는 것은 「계약에 적은 성질」뿐이다
  계약의 누락(적지 않은 성질)은 증명되지 않는다
  예: Post에서 정렬 완료를 증명해도, 「파괴적이지 않다」는 것을 적지 않으면
  원래의 요소가 보존됨은 보증되지 않는다

증명기의 한계:
  자동 증명기로는 증명할 수 없는 복잡한 성질이 있다
  그런 경우는 수동 증명(Coq 등)에 의존할 필요가 있다
  다만 실무 범위에서는 자동 증명으로 충분한 경우가 많다

언어의 제한:
  포인터를 많이 사용하는 코드는 SPARK화할 수 없다
  동적 메모리 할당의 증명은 제한적이다
  재귀적 데이터 구조의 증명은 어렵다

개발자의 숙련도:
  계약을 작성하는 방법에는 훈련이 필요하다
  루프 불변조건의 설계는 특히 익히는 데 시간이 걸린다
  팀 전체의 스킬 향상 계획이 반드시 필요하다

15. 정리 —— 증명을 일상적인 개발로

SPARK를 이용한 형식 검증의 실전을 정리해 보았습니다.

SPARK는 Ada의 서브셋으로, 증명 가능한 기능으로 좁혀져 있다
계약(Pre/Post)이 증명의 입력이 된다. Ada 2012의 계약을 그대로 사용할 수 있다
GNATprove가 자동 증명을 실행하고, 결과를 소스 코드 수준에서 보고한다
루프 불변조건으로 루프의 성질을 증명한다
Global/Depends로 데이터 흐름을 명시하고, 부작용을 관리한다
증명 레벨(Stone~Platinum)로 단계적으로 엄격함을 높여갈 수 있다
우선 Silver 레벨(런타임 오류 없음)을 목표로 하는 것이 실전적이다
테스트와 증명은 대립하는 것이 아니라, 서로 보완한다

「형식 검증은 어렵고, 특별한 프로젝트에만 쓰는 것」이라는 선입견이 있을지도 모릅니다.

하지만 오늘날의 SPARK와 GNATprove의 조합은, 다음과 같은 수준에 도달해 있습니다.

계약을 작성한다. 이것은 타입이나 테스트를 작성하는 것과 본질적으로 같은 설계 작업이다
gnatprove를 실행한다. 컴파일과 비슷한 느낌이다
결과를 보고, 코드나 계약을 수정한다

이 순환은, 컴파일러의 오류 메시지를 보면서 코드를 수정하는 일상적인 개발 흐름과 별반 다르지 않습니다.

차이는, 컴파일러가 「문법이 올바르다」를 보증하는 데 반해, GNATprove는 「모든 입력에서 올바르다」를 보증한다는 점입니다.

지난 글에서 소개한 Ada의 캐치프레이즈 「버그는 찾아내는 것이 아니라, 타입과 계약으로 쓸 수 없게 만드는 것」은, SPARK에 의해 다음 단계로 나아갑니다.

버그의 부재는, 증명으로 보증하는 것이다.

먼저, 작은 함수에 SPARK_Mode와 Post를 붙이고, gnatprove를 실행해 보세요.

postcondition proved라는 초록색 메시지를 봤을 때, 소프트웨어 품질 보증에 대한 관점이 바뀔 것입니다.

참고 자료

같은 태그를 공유하는 최신 기사입니다. 더 가까운 주제로 지식을 넓힐 수 있습니다.

자주 묻는 질문

이 기사 주제에 대해 상담 시 자주 나오는 질문을 모았습니다.

SPARK란 무엇인가요? Ada와는 어떤 관계인가요?: SPARK는 Ada의 서브셋(부분 언어)으로, 프로그램의 성질을 수학적으로 증명할 수 있도록 설계되어 있습니다. 포인터를 이용한 동적 메모리 관리나 자유로운 예외 사용 등을 제한하는 대신, 증명 가능성을 얻고 있습니다. SPARK 코드는 Ada 코드에 계약 주석을 추가한 것이므로, 평소의 Ada 개발의 연장선에 있으며 특별한 문법을 새로 익힐 필요는 없습니다. 도구는 AdaCore가 제공하는 GNATprove가 중심이며, 계약을 Why3 중간 언어로 변환한 뒤 Z3 등의 자동 증명기로 증명을 시도합니다.
형식 검증은 테스트와 무엇이 다른가요?: 테스트는 「선택한 입력에 대해 올바르게 동작하는지」를 확인하는 반면, 형식 검증은 「모든 입력에 대해 성질이 성립하는지」를 수학적으로 증명합니다. 입력의 조합은 무한하기 때문에, 테스트만으로는 모든 입력에서의 정확성을 보일 수 없습니다. 다만 둘은 대립하는 것이 아니라 서로 보완하는 관계이며, SPARK로 Silver 레벨(런타임 오류 없음)을 보증하고, 단위 테스트로 구체적인 입출력을 확인하고, 증명할 수 없는 부분에 집중적으로 테스트를 작성하는 병행 사용이 실용적입니다.
SPARK의 증명 레벨(Stone~Platinum)이란 무엇인가요?: 단계적으로 증명의 엄격함을 높여가기 위한 개념입니다. Stone은 계약의 문법과 타입의 일관성 검사만, Bronze는 초기화되지 않은 변수를 읽지 않는다는 증명, Silver는 런타임 오류(범위 초과, 오버플로, 0으로 나누기)가 발생하지 않는다는 증명, Gold는 Pre/Post 조건의 증명을 통한 완전한 기능적 정당성, Platinum은 여기에 더해 정보 흐름의 증명까지 포함한 보안 중시 레벨입니다. 실무에서는 우선 Silver 레벨을 목표로 하는 것이 가장 실용적인 목표로 여겨집니다.
GNATprove로 증명할 수 없을 때는 어떻게 해야 하나요?: 메시지별로 대응합니다. 「postcondition might fail」은 Post 조건이 너무 강하거나 Pre 조건이 너무 약한 경우, 혹은 루프 불변조건이 부족한 것이 원인입니다. 「overflow check might fail」은 Pre 조건으로 값의 범위를 제한하거나 타입 자체의 범위를 좁힙니다. 「array index check might fail」은 루프 범위가 배열 범위 안에 있음을 불변조건으로 보여줍니다. 「prover timeout」은 불변조건으로 증명을 단계적으로 나누거나 함수를 더 작게 분할합니다. 정말로 실패할 수 있는지 코드를 읽고 판단하는 것이 첫 단계입니다.

저자 프로필

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

Go Komura

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

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

프로필 보기 문의하기

공개 링크

GitHub LinkedIn X COM_BLAS COM_BigDecimal

블로그 목록으로 돌아가기

SPARK를 이용한 형식 검증 입문 —— Ada의 계약에서 수학적 증명으로

1. 시작하며 —— 「실행해서 확인한다」의 다음 단계로

2. SPARK란 무엇인가 —— Ada의 부분 언어이자 증명의 세계로 가는 입구

3. GNATprove 설치와 첫 증명

4. 계약에 의한 설계의 기초 —— Pre와 Post 작성법

5. 오버플로 증명 —— 수치 계산의 안전성을 보증한다

6. 루프 불변조건 —— 루프의 성질을 증명한다

7. Assert 프래그마 —— 코드 중간에 적는 부분적인 성질

8. 데이터 흐름 계약 —— Global과 Depends

9. 증명 레벨 —— Stone에서 Platinum으로 단계적으로 적용하기

10. 실전적인 증명 흐름 —— 시행착오를 줄이는 워크플로

11. SPARK와 테스트의 병행 —— 보완 관계를 이해한다

12. GNATprove의 결과 읽기 —— 메시지 해석

13. 실제 프로젝트에 적용하는 방법

14. SPARK의 한계와 주의점

15. 정리 —— 증명을 일상적인 개발로

참고 자료

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

Ada 제네릭 프로그래밍 ── 타입으로 계약을 작성하고 재사용을 제로 코스트로 실현하기

Ada를 활용한 실시간 시스템 프로그래밍 ── 우선순위·주기·실행 시간 제어의 실전

Ada의 안전한 동시성 처리 ── 태스크와 보호 객체 실전 가이드

PerfView와 dotnet-trace로 “느림”의 원인을 찾는다 ── .NET 성능 조사 실무 입문

관련 토픽

Windows 기술 토픽

자주 묻는 질문

저자 프로필

Go Komura

1. 시작하며 —— 「실행해서 확인한다」의 다음 단계로

2. SPARK란 무엇인가 —— Ada의 부분 언어이자 증명의 세계로 가는 입구

3. GNATprove 설치와 첫 증명

4. 계약에 의한 설계의 기초 —— Pre와 Post 작성법

5. 오버플로 증명 —— 수치 계산의 안전성을 보증한다

6. 루프 불변조건 —— 루프의 성질을 증명한다

7. Assert 프래그마 —— 코드 중간에 적는 부분적인 성질

8. 데이터 흐름 계약 —— Global과 Depends

9. 증명 레벨 —— Stone에서 Platinum으로 단계적으로 적용하기

10. 실전적인 증명 흐름 —— 시행착오를 줄이는 워크플로

11. SPARK와 테스트의 병행 —— 보완 관계를 이해한다

12. GNATprove의 결과 읽기 —— 메시지 해석

13. 실제 프로젝트에 적용하는 방법

14. SPARK의 한계와 주의점

15. 정리 —— 증명을 일상적인 개발로

참고 자료

관련 기사

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

Ada 제네릭 프로그래밍 ── 타입으로 계약을 작성하고 재사용을 제로 코스트로 실현하기

Ada를 활용한 실시간 시스템 프로그래밍 ── 우선순위·주기·실행 시간 제어의 실전

Ada의 안전한 동시성 처리 ── 태스크와 보호 객체 실전 가이드

PerfView와 dotnet-trace로 “느림”의 원인을 찾는다 ── .NET 성능 조사 실무 입문

관련 토픽

Windows 기술 토픽

자주 묻는 질문

저자 프로필

Go Komura