한줄평
“정확성이 핵심인 코드를 형식적으로 보장하고 싶을 때 매우 강력합니다. 명세를 작성하는 노력이 필요해 일상적인 개발에 두루 쓰기엔 무겁습니다.”
이런 분께 정확성 보장이 중요한 알고리즘을 형식 검증하려는 분께
좋은 점
- 명세 기반으로 코드의 정확성을 자동 증명
- 검증 교육·연구에 널리 활용
아쉬운 점
- 명세·불변식 작성에 상당한 노력이 필요
- 일반 앱 개발에는 과함
대프니 소개
프로그램이 명세대로 동작함을 수학적으로 증명해주는 검증기를 내장한 프로그래밍 언어입니다. 함수에 사전·사후 조건과 불변식을 적어두면 컴파일 과정에서 그 조건이 항상 성립하는지 자동으로 검사합니다. 버그가 있으면 안 되는 알고리즘이나 교육·연구용 검증에 쓰며, 명령줄에서 검증·컴파일합니다.
