SPARK로 하는 형식 검증 입문 ── Ada의 계약에서 수학적 증명으로

1. 들어가며 ── 「실행해서 확인한다」의 다음

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

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

그러나 테스트에는 한계가 있습니다. 입력 조합은 무한히 있으며, 「모든 입력에서 올바르다」는 사실은 테스트만으로는 보일 수 없습니다.

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

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

이전 기사 「Ada 언어의 매력」에서는 Ada의 전체 모습을 소개하고 SPARK도 간단히 언급했습니다.

이 기사에서는 SPARK를 이용한 형식 검증의 실무에 초점을 맞춰 다음을 정리합니다.

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

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

이 기사의 대상 독자와 전제 지식

대상으로 하는 독자는 다음과 같습니다.

• Ada의 기본 문법(패키지, in / out / in out 파라미터 모드, 타입과 subtype)을 한 번은 본 적 있는 분
• 계약 프로그래밍이나 정적 분석에 관심이 있고, 「테스트의 다음」을 찾는 분
• 고신뢰성·임베디드·제어 시스템 소프트웨어에서 품질 보증 수단을 검토하는 분

Ada를 처음 접해도 읽을 수 있지만, 전제를 두 가지만 보충합니다. 이 기사의 코드 예에는 package ... is와 package body ... is로 패키지 명세와 본문(body)을 나누는 방식, 그리고 procedure P (X : in out Integer)와 같은 파라미터 모드가 반복해서 나옵니다. 이 두 가지가 익숙하지 않다면, 먼저 「Ada 언어의 매력」에서 Ada 쪽 기초를 잡은 뒤 돌아오면 계약 이야기에 집중할 수 있습니다.

바꿔 말하면, 이 두 가지만 알면 읽어 나갈 수 있습니다. SPARK 고유 표기(SPARK_Mode, Pre, Post, Loop_Invariant, Global, Depends)는 모두 이 기사 안에서 설명합니다. 증명기 이론이나 논리학 지식도 필요 없습니다. GNATprove가 낸 메시지를 읽고 코드나 계약을 고칩니다. 실제로 필요한 것은 그것뿐입니다.

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

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

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

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

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

서브셋인 것에는 분명한 의도가 있습니다.

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

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

포인터(access type)에 의한 동적 메모리 관리 → 소유권 모델로 제어
예외 핸들러의 자유로운 사용               → 제한적으로 허용
재귀적 데이터 구조                       → 증명이 어렵기 때문에 제한
task의 자유로운 사용                   → Ravenscar 프로파일로 제한

「제한」이라고 하면 답답하게 느껴질 수 있습니다. 그러나 이러한 제한은 증명 가능성과 맞바꾼 것입니다.

SPARK의 툴셋은 AdaCore가 제공하는 GNATprove가 중심입니다.

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

그림으로 보면 다음과 같은 흐름입니다.

flowchart LR
    Src["SPARK로 작성된 Ada 코드<br/>Pre / Post / Assert"] --> GP[GNATprove]
    GP --> VC[검증 조건 생성]
    VC --> Why3["Why3<br/>중간 언어와 증명 플랫폼"]
    Why3 --> P1[cvc5]
    Why3 --> P2[Z3]
    Why3 --> P3[Alt-Ergo]
    P1 --> Res[결과 집계]
    P2 --> Res
    P3 --> Res
    Res --> Msg["소스 코드 위치가 붙은 메시지<br/>info / medium / high"]

개발자가 직접 다루는 것은 양끝, 즉 왼쪽 코드와 오른쪽 메시지만입니다. 가운데 Why3와 증명기는 자동으로 동작하므로 평소에는 신경 쓸 필요가 없습니다. 신경 쓰는 것은 증명이 통과하지 않아 증명기를 바꾸거나 시간을 더 들이는 단계에 와서입니다.

이 장에서 나온 이름

처음 나온 고유 명사를 여기서 정리해 둡니다. 이후에는 설명 없이 사용합니다.

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

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

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

3. GNATprove 설치와 첫 증명

우선 GNATprove를 실행할 환경을 갖춥니다.

Alire를 설치한다

GNATprove는 GNAT 툴체인에 포함되어 있습니다. 그 툴체인을 구하는 가장 손쉬운 방법이 Alire입니다. Ada / SPARK용 소스 기반 패키지 매니저이며, 명령 이름은 alr입니다. 배포물은 Alire의 GitHub 리포지토리 릴리스 페이지에서 받습니다.

설치했으면 기본 컴파일러를 고릅니다.

alr toolchain --select

선택 도우미가 시작되고, 설치 가능한 GNAT 목록에서 기본 컴파일러를 고를 수 있습니다. 인자 없이 alr toolchain을 실행하면 설치된 컴파일러와 현재 기본값이 표시됩니다.

버전을 확인한다

환경이 갖춰지면 버전을 기록해 두십시오. 증명 결과는 증명기 버전에 의존합니다. 나중에 「같은 코드가 증명되지 않게 되었다」가 되었을 때 먼저 확인할 정보입니다.

alr version
gnatprove --version

프로젝트를 만든다

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의 입구입니다.

증명되지 않았을 때의 출력

성공했을 때의 출력만 보고 있어서는 부족합니다. 실무에서 필요한 것은 실패했을 때 출력을 읽는 방법입니다. GNATprove는 증명하지 못한 검사를 소스 코드 위치와 함께 보고합니다. 기본 형태는 다음 한 줄입니다.

file.adb:12:37: medium: divide by zero might fail

file.adb의 12행 37열, 즉 나눗셈 기호 /가 있는 위치에 대해 「제수가 0이 아님을 증명하지 못했다」는 뜻입니다. 여기서 중요한 것은 might fail(실패할 수도 있다)이지 will fail(실패한다)이 아니라는 점입니다. 정말로 버그가 있다고는 할 수 없습니다. 정보가 부족해 증명기가 판단하지 못했을 뿐인 경우가 대부분입니다.

반례가 나오면 더 자세한 형태로 보고됩니다.

high: assertion might fail
--> counterex.adb:11:25
 11 |    pragma Assert (R < 42);
    |                  ^~~~~~
  + e.g. when R = 42
  + provers gave up before completing the proof

e.g. when R = 42가 반례로, 「R이 42일 때 성립하지 않는다」고 구체적으로 알려 줍니다. 계약 부족이 원인이라고 GNATprove가 추정한 경우에는 수정안이 붙는 일도 있습니다.

possible fix: subprogram at line xxx should mention Var in a precondition
possible fix: loop at line xxx should mention Var in a loop invariant
possible fix: call at line xxx should mention Var in a postcondition

이런 메시지는 스스로 의도적으로 내 보는 것이 가장 빨리 익숙해집니다. 예를 들어 위의 Abs_Value의 Post를 Abs_Value'Result > 0(0보다 큼)으로 바꾸면 X = 0 케이스를 증명하지 못해 postcondition might fail이 나옵니다. 5장에서 다루는 Increment에서 Pre를 빼면 overflow check might fail이 나옵니다. 성공 예와 실패 예를 번갈아 내면서 진행하는 것이 GNATprove에 익숙해지는 지름길입니다.

또한 메시지의 심각도(info / medium / high)와 검사 종류 목록은 12장에서 정리합니다.

4. Design by Contract의 기초 ── 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 계약으로 부작용을 명시한다(8장)

5. overflow 증명 ── 수치 계산의 안전성을 보장한다

SPARK 증명에서 실무적으로 가장 혜택이 큰 것 중 하나가 overflow 방지입니다.

다음 코드를 보겠습니다.

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

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

계약이 없으면 GNATprove는 overflow 가능성을 경고합니다.

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의 합이 overflow하지 않는다」는 조건을 부호를 고려해 경우로 나눈 것입니다.

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

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;

루프 불변조건 설계에는 다음 접근이 필요합니다.

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

하나 더, 배열 탐색 예를 봅니다.

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 pragma ── 코드 안에 쓰는 부분적 성질

계약(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;

pragma 쓰임새를 정리합니다.

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

Assert를 쓰는 장면은 다음과 같습니다.

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

8. 데이터 플로 계약 ── Global과 Depends

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

subprogram이 읽고/쓰는 전역 변수를 명시합니다.

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 계약의 모드는 다음 세 가지입니다.

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

나아가 변수 사이 의존 관계를 Depends로 표현할 수 있습니다.

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

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

데이터 플로 계약의 이점:
  1. 「이 함수는 무엇을 건드리는가」가 한눈에 보인다
  2. 의도하지 않은 부작용을 컴파일 시점에 검출할 수 있다
  3. 변수의 정보 흐름 분석의 입력이 된다
  4. 대규모 시스템에서 데이터 흐름 시각화에 도움이 된다

9. 증명 레벨 ── Stone에서 Platinum으로의 단계적 적용

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

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

Stone:
  SPARK 서브셋으로서 타당한 코드인지를 확인
  도입 중간 단계로 사용한다

Bronze:
  Stone + 초기화되지 않은 변수를 읽지 않을 것,
  데이터 플로가 의도대로라는 보장
  가능한 한 넓은 범위에 적용한다

Silver:
  Bronze + 런타임 오류(범위 밖, overflow, 0으로 나누기)가
  일어나지 않는다는 증명 (AoRTE: Absence of Run-time Errors)
  크리티컬 소프트웨어의 기본 목표

Gold:
  Silver + 중요한 integrity 프로퍼티
  (안전성·보안상 핵심이 되는 성질)의 증명
  그런 성질을 가진 일부 코드에만 적용한다

Platinum:
  요구 사양의 완전한 기능적 정확성 증명
  최고 수준 요구가 있는 부분에만 적용한다
  비용이 높고, 적용 예는 많지 않다

「레벨」이라는 말이 가리키는 것 ── --mode와 --level은 별개

여기서 혼동하기 쉬운 점을 정리해 둡니다. Stone~Platinum은 소프트웨어 보증 레벨이며, gnatprove의 --level 옵션과는 다른 개념입니다. 전자에 대응하는 것은 --mode 쪽입니다.

Silver, Gold, Platinum은 같은 스위치로 실행합니다. 차이는 도구를 돌리는 방식이 아니라, 무엇을 어디까지 검증 대상으로 정하는가라는 목표 설정 쪽에 있습니다.

한편 --level=0 ~ --level=4는 증명에 얼마나 품을 들일지를 정하는 프리셋입니다. 값을 올릴수록 시간은 걸리지만 증명력은 올라갑니다. 내용은 개별 스위치의 조합이며, 다음과 같습니다.

즉 --mode가 「무엇을 검증하는가」, --level이 「얼마나 끈질기게 하는가」입니다. 먼저 의식할 것은 --mode 쪽이고, --level은 증명이 통과하지 않을 때 올려 가는 조정 손잡이라고 생각하면 됩니다.

한 가지 더, 실무상의 주의가 있습니다. --level은 제한 시간으로 제어하므로 머신의 성능이나 부하에 따라 결과가 바뀌고, 재현성이 없습니다. CI나 여러 사람이 결과를 공유하는 경우에는, 시간이 아니라 추론 스텝 수로 상한을 정하는 --steps나, 기존 증명 결과를 재생하는 --replay를 쓰는 것이 공식적으로 권장됩니다.

출처: SPARK User’s Guide(8.1 Levels of Software Assurance, 및 Appendix A Command Line Invocation)

실무적인 도입 전략은 다음과 같습니다.

1단계: 프로젝트 전체를 Stone 레벨로 통과시킨다
  → 계약의 잘못된 작성을 찾는다

2단계: 중요한 모듈을 Silver 레벨로 만든다
  → overflow나 범위 밖 접근을 없앤다
  → 실무상 버그의 상당수는 여기서 막을 수 있다

3단계: 핵심 로직을 Gold 레벨로 만든다
  → 안전성·보안의 핵심 성질을 수학적으로 보장한다
  → 코드 전체가 아니라 그 성질을 가진 부분으로 좁힌다

4단계: 최고 수준 요구가 있는 부분만 Platinum으로
  → 요구 사양의 완전한 기능적 정확성을 증명한다
  → 비용이 높으므로 적용 범위는 최소한으로 한다

10. 실무적인 증명의 흐름 ── 재작업을 줄이는 워크플로

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

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

2. 계약(Pre/Post)을 쓴다
   구현 전에 사양을 계약으로 표현한다

3. 컴파일을 통과시킨다
   GNAT으로 컴파일 오류를 없앤다

4. Stone 레벨로 GNATprove를 실행한다
   gnatprove -P proj.gpr --mode=stone

5. 경고를 확인하고, 필요하면 계약을 수정한다
   특히 초기화 누락에 주의
   초기화와 데이터 플로만 보려면 Bronze
   gnatprove -P proj.gpr --mode=bronze

6. Silver 레벨을 목표로 한다
   gnatprove -P proj.gpr --mode=silver
   런타임 오류를 없앤다

7. 루프가 있으면 불변조건을 추가한다
   증명되지 않으면 불변조건이 부족한지 확인한다

8. Gold 레벨에서 중요한 성질을 증명한다
   gnatprove -P proj.gpr --mode=gold
   실행 스위치는 Silver와 같고, 바뀌는 것은 검증 목표 쪽
   시간 안에 증명이 끝나지 않을 때만 --level을 올려 끈질기게 한다
   예: gnatprove -P proj.gpr --mode=gold --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의 증명:
  모든 입력에 대해 성질이 성립한다
  계약에 쓴 성질만 대상이다
  증명하지 못하는 케이스는 수동 확인이나 테스트에 맡긴다

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

함께 쓰는 패턴입니다.

1. SPARK로 Silver 레벨(런타임 오류 없음)을 보장
2. 단위 테스트로 구체적인 입출력의 올바름을 확인
3. Gold 레벨로 코어 로직을 증명
4. 증명하지 못한 부분에 테스트를 집중해서 쓴다

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

12. GNATprove 결과를 읽는다 ── 메시지 해석

GNATprove 출력에는 다음 세 레벨이 있습니다.

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

자주 있는 메시지와 그 의미입니다.

「postcondition proved」          Post 조건이 증명되었다
「range check proved」            범위 검사가 증명되었다
「overflow check proved」         overflow하지 않음이 증명되었다
「index check proved」            배열 첨자 범위가 증명되었다
「divide by zero check proved」   0으로 나누기가 일어나지 않음이 증명되었다

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

might fail이 나왔을 때의 대응 절차입니다.

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

13. 실제 프로젝트에 넣는 방법

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

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

2. Silver를 목표로 한다
   Gold(중요한 완전성 증명)나 Platinum(완전 기능 증명)은 이상적이지만,
   Silver(런타임 오류 없음)부터 시작한다
   overflow 방지뿐이라도 실무상 가치는 매우 크다

3. 인터페이스부터 계약을 쓴다
   구현보다 먼저 패키지 명세(.ads)에 계약을 쓴다
   사양이 굳어 있으면 구현자가 누구든 계약을 충족하는 코드를 쓸 수 있다

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

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

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

1. 신규 모듈은 Ada/SPARK로 쓴다
2. C/C++와는 Interfaces.C를 통해 연동한다
3. 중요한 데이터 구조와 검증 로직을 SPARK로 옮긴다
4. 단계적으로 SPARK 범위를 넓힌다

14. SPARK의 한계와 주의점

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

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

증명기의 한계:
  자동 증명기로는 증명하지 못하는 복잡한 성질이 있다
  그 경우에는 수동 증명(Coq 등)에 의지해야 한다
  그렇다 해도 실무 범위에서는 자동 증명으로 충분한 경우가 많다

언어의 제한:
  포인터를 많이 쓰는 코드는 SPARK로 옮기지 못한다
  동적 메모리 할당의 증명은 한정된다
  재귀적 데이터 구조의 증명은 어렵다

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

15. 정리 ── 증명을 일상 개발에

SPARK에 의한 형식 검증의 실무를 정리해 왔습니다.

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

「형식 검증은 어렵고, 특별한 프로젝트만의 것」이라는 선입견이 있을 수 있습니다.

그러나 오늘날의 SPARK와 GNATprove 조합은 다음 레벨에 도달해 있습니다.

1. 계약을 쓴다. 이것은 타입이나 테스트를 쓰는 것과 본질적으로 같은 설계 작업
2. gnatprove를 실행한다. 컴파일과 비슷한 감각
3. 결과를 보고, 코드나 계약을 수정한다

이 사이클은 컴파일러 오류 메시지를 보면서 코드를 고치는 일상 개발 흐름과 다르지 않습니다.

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

이전 기사에서 소개한 Ada의 캐치프레이즈 「버그는 찾는 것이 아니라, 타입과 계약으로 쓰지 못하게 하는 것」은 SPARK에 의해 다음 단계로 나아갑니다.

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

우선 작은 함수에 SPARK_Mode와 Post를 붙이고 gnatprove를 실행해 보시기 바랍니다.

postcondition proved의 초록 메시지를 보았을 때, 소프트웨어 품질 보증에 대한 시각이 바뀔 것입니다.

참고

• 이 기사의 코드 조각을 장마다 정리한 참조용 코드 모음 - komurasoft-blog-samples (GitHub)
• SPARK - AdaCore
• Introduction to SPARK - learn.adacore.com
• SPARK 2014 Reference Manual
• GNATprove User’s Guide
• Ada Reference Manual (Ada 2022)
• Alire - Ada Library Repository
• Why3 - Platform for Deductive Program Verification
• Ada 언어의 매력 ── 타입으로 설계를 말하고, 수십 년 동안 동작하는 소프트웨어를 지탱하는 언어 - 이 사이트

관련 기사

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

관련 토픽

이 기사와 가까운 토픽 페이지입니다. 기사를 출발점 삼아 관련 서비스와 다른 기사로 이어집니다.

자주 묻는 질문

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

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

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

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

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

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

증명 엄격도를 단계적으로 올리는 개념입니다. Stone은 유효한 SPARK일 것, Bronze는 미초기화 변수 읽기가 없고 데이터 플로가 올바르다는 증명, Silver는 런타임 오류(범위 밖, overflow, 0으로 나누기)가 일어나지 않는다는 증명입니다. Gold는 여기에, 중요한 데이터 불변조건이 유지되거나 상태 전이가 사양대로라는 식의, 핵심이 되는 완전성(integrity) 성질의 증명을 더합니다. Platinum은 계약이 기능 요구를 망라하고 구현이 사양대로임을 증명하는 완전한 기능적 정확성 레벨로, 비용이 높고 도달 사례는 많지 않습니다. 실무에서는 우선 Silver 레벨을 목표로 하는 것이 가장 실용적인 목표로 여겨집니다.

GNATprove에서 증명되지 않을 때는 어떻게 하면 되나요?

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

저자 프로필

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

Go Komura

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

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