실행과 명세를 함께 준비하기
Gobra 프로그램은 검사하려는 Go 코드에 검증용 설명을 추가한 형태다. 프로그램을 실행해 관측한 결과만 비교하기보다, 함수나 구성 요소가 지켜야 하는 조건을 표현한다. 명세가 잘못되거나 부족하면 검증 결과도 실제 요구 사항과 어긋날 수 있다.
동시성 코드 분석
Go는 여러 실행 흐름과 채널 통신을 언어 차원에서 다룬다. Gobra는 이런 프로그램을 모듈별로 추론하는 것을 목표로 한다. 특정 라이브러리나 언어 기능이 처리되는지는 도구의 지원 범위와 사용한 모델을 따로 확인해야 한다.
검증 도구의 구성
Go 컴파일러만 설치해서 실행하는 검사기는 아니다. Viper 검증 기반과 SMT 해결기 등 별도의 구성 요소가 사용된다. 기본 Silicon 백엔드와 Carbon 백엔드의 의존 조건도 다르므로 분석 기록에는 백엔드와 도구 버전을 함께 남긴다.
관련 문서
Viper 검증 기반 / Boogie / Z3 / Prusti