타입 검사보다 넓은 질문
타입이 맞는 프로그램도 계산 결과나 입출력 순서가 요구 사항과 다를 수 있다. Nagini는 타입 정보를 바탕으로 프로그램을 다루면서 별도의 명세로 확인할 속성을 표현한다. 타입 표기만 추가했다고 기능적 정확성까지 자동으로 증명되는 것은 아니다.
명세로 다루는 속성
기본적인 안전성뿐 아니라 입출력 행동, 진행에 관한 조건, 안전한 정보 흐름 등을 표현하는 기능을 갖는다. 이를 통해 단순 반환값 비교보다 넓은 요구 사항을 분석할 수 있다. 어떤 속성을 검증했는지는 작성한 명세를 기준으로 판단해야 한다.
지원 범위 이해하기
Python의 동적인 모든 기능을 그대로 처리하는 도구는 아니다. 지원하는 정적 타입 Python 부분집합 안에서 코드와 명세를 준비해야 한다. 모듈식 검증에서는 각 구성 요소의 계약이 연결되므로 외부 코드에 대한 가정도 결과 해석에 영향을 준다.
관련 문서
Viper 검증 기반 / Gobra / Prusti / Dafny