언어의 동작을 정의하기
프로그래밍 언어는 문법뿐 아니라 각 구문이 상태를 어떻게 바꾸는지도 필요하다. K는 이런 동작을 명세로 작성하고 활용하기 위한 기반을 제공한다. 일반 응용 프로그램을 작성하는 언어와는 목표가 다르며, 언어 자체를 분석 대상으로 삼을 수 있다.
명세에서 도구로
K 명세를 컴파일해 실행과 분석에 사용할 수 있다. kompile은 정의를 컴파일하는 데, krun은 프로그램을 실행하는 데 사용된다. 구성과 백엔드에 따라 제공되는 분석 기능이 달라지므로 하나의 명세가 모든 검증 질문을 자동으로 해결한다고 이해하면 안 된다.
사용 환경 구분
K 기반의 완성된 도구를 쓰는 경우에는 해당 도구의 설치 안내를 따른다. 프레임워크 자체를 소스에서 빌드하는 과정과는 요구 사항이 다를 수 있다. 언어 정의와 분석 대상 프로그램, 사용한 실행 구성을 구분해 기록해야 결과를 재현하기 쉽다.
관련 문서
Boogie / Viper 검증 기반 / Dafny / KLEE