매칭 논리 속성(Matching Logic Properties)의 구문 기반 점진적 프로그램 검증

점진성(Incrementality)은 대규모의 장기 생존 소프트웨어 시스템의 복잡성을 제어하기 위한 근본적인 설계 원칙입니다. 이 원칙은 애자일 개발 프로세스(Agile development processes)에 의해 수용되었으며, 지속적인 소프트웨어 진화의 기초를 형성합니다. 이러한 맥락에서의 주요 과제는 매번 변경이 발생할 때마다 소프트웨어 산출물의 정확성을 점진적으로 재검증하는 것이며, 검증 노력을 변경의 영향을 받는 부분에만 집중하는 것입니다. 본 논문에서는 매칭 논리(Matching logic)로 표현된 속성들이 주석으로 달린 KernelC로 작성된 프로그램의 점진적 검증(Incremental verification) 접근 방식을 제시합니다. 이 접근 방식은 코드 청크(Code chunks)를 독립적으로 분석할 수 있게 하는 구문-의미론적 프레임워크(Syntactic-semantic framework)를 기반으로 하며, 이를 통해 프로그램 파편(Program fragment)의 변경 후에는 변경에 의해 의미론(Semantics)이 영향을 받는 부분만 재처리됩니다. 이러한 속성은 연산자 우선순위 문법(Operator precedence grammar)을 통해 언어 구문(Language syntax)을 표현하고, 합성 속성 스키마(Synthesized attribute schema)를 통해 의미론을 공식화함으로써 얻어집니다. 우리는 프로토타입 도구에 이 기술을 구현하였으며 그 효과를 실험적으로 평가하였습니다. 결과에 따르면, 우리의 접근 방식은 형식 검증(Formal verification)의 효율성을 저해하지 않으며, 주석의 존재 여부와 유형, 변경 위치 및 프로그램 구조에 따라 변경 후 프로그램 재검증 성능을 능가할 수 있음을 보여줍니다.