언어와 계약의 결합
프로그램이 수행할 동작과 함께 함수가 지켜야 하는 조건을 명시한다. SPARK는 Ada의 단순한 축소판을 넘어 추상화와 정제를 표현하는 기능을 갖는다. 구현이 명세에 부합하는지 구성 요소별로 분석할 수 있도록 설계되었다.
정적 분석과 증명
정보 흐름 분석과 형식 검증은 관련되어 있지만 같은 작업은 아니다. 값의 전달 관계를 확인하는 것과 계산 결과가 요구한 성질을 만족함을 증명하는 것은 구분된다. GNATprove는 이러한 분석을 지원하는 GNAT 도구 체계의 구성 요소다.
테스트와 함께 사용하기
전체 프로그램을 한 방식으로만 확인할 필요는 없다. 일부 단위는 증명하고 다른 단위는 테스트하는 접근을 지원한다. 언어를 선택했다는 사실만으로 검증이 끝나는 것은 아니며, 작성한 명세와 실제로 확인한 단위의 범위를 함께 관리해야 한다.