SEMBridge: 최약 전제조건(Weakest-Precondition) 및 유계 검사(Bounded-Checking) 해석을 이용한

형식 방법론(Formal methods)은 프로그램 동작에 대한 엄격한 설명을 제공하지만, 실제 소프트웨어 공학은 종종 실행 가능한 라이브러리, 테스트 및 점진적 설계를 통해 이루어집니다. 본 논문은 동일한 실행 가능한 객체 프로그램(object programs)으로부터 최약 전제조건(weakest-precondition) 및 유계 검사(bounded-checking) 해석을 생성하기 위한 소규모 태그리스-파이널(tagless-final) 프레임워크인 SEMBridge를 제시합니다. 프로그램 의미론(program semantics)을 하나의 추상 구문 트리(abstract syntax tree)에 고정하고 별도의 순회(traversal) 코드를 작성하는 대신, 객체 프로그램은 하나의 의미론적 인터페이스(semantic interface)를 대상으로 한 번만 작성되며, 이를 통해 가독성 있는 코드, 구체적인 실행(concrete execution), 술어 변환기(predicate transformers), 유계 반례 탐색(bounded counterexample search), 그리고 향후 증명 보조 도구(proof-assistant)나 SMT 백엔드로의 다중적인 의미로 해석됩니다. Python 프로토타입은 할당(assignments), 조건문(conditionals), 가정(assumptions) 및 단언(assertions)을 포함하는 루프가 없는 명령형 코어(loop-free imperative core)를 구현합니다. 5개의 예제 프로그램을 통해, 동일한 태그리스-파이널 정의가 실행 가능한 상태 변환기(state transformers)와 검증 조건(verification conditions)을 생성하였으며, 이는 최대 729개의 상태에 걸친 도메인에서 유계 검사를 통과했습니다. 본 연구의 기여는 Scala 코드 생성 시스템이나 새로운 검증기(verifier)를 만드는 것이 아니라, 실행 가능한 의미론, 최약 전제조건 산출물, 그리고 유계 검증을 동기화된 상태로 유지하기 위한 컴팩트한 아키텍처를 제공하는 데 있습니다.