10. SPARK 소개

SPARK(SPADE Ada Kernel의 합성어)는 고신뢰성 소프트웨어 개발을 위해 특별히 설계된 Ada 언어의 형식적으로 분석 가능한 하위 집합입니다.

SPARK는 두 가지 전략의 조합을 통해 정확성 증명을 가능하게 하는 목표를 달성합니다:

1. 언어 부분집합화: 일반적인 접근 형식(에일리어싱 방지), 예외 처리(모든 런타임 오류가 없음을 증명하므로), 함수 내 부작용 등 형식적으로 분석하기 어려운 Ada의 기능을 제외합니다.

2. 강화된 계약: Ada의 DbC 모델을 확장하여 데이터 의존성(어떤 입력이 어떤 출력에 영향을 미치는지), 정보 흐름 정책, 상태 추상화와 같은 속성을 지정할 수 있는 더 상세한 계약을 추가합니다.

GNATprove와 같은 도구 모음을 사용하여 개발자는 형식적 방법을 통해 수학적 증명의 높은 확신도로 SPARK 프로그램이 언어 정의 런타임 오류로부터 자유롭고, 기능적 명세를 준수하며, 중요한 안전 및 보안 속성을 준수함을 증명할 수 있습니다. 이는 테스트(버그의 존재만을 보여줄 수 있음)를 넘어 증명(버그의 부재를 보여줄 수 있음)으로 나아가는 높은 수준의 소프트웨어 보증을 나타냅니다. 강력한 형식 시스템에서부터 런타임 검사, 계약에 의한 설계, 그리고 SPARK를 이용한 형식적 증명에 이르기까지 이 계층적 접근 방식이 Ada 언어 제품군을 고무결성 소프트웨어 구축에 적합하게 만듭니다.