자바에 대한 확장된 정적 검사

소프트웨어 개발 및 유지 관리 비용은 높습니다. 개발 주기 초기에 더 많은 소프트웨어 결함을 발견하면 비용을 줄일 수 있습니다. 본 논문에서는 일반적인 프로그래밍 오류를 찾는 실험적인 컴파일 타임 프로그램 검사기인 자바용 확장 정적 검사기(ESC/Java)를 소개합니다. 이 검사기는 검증 조건 생성 및 자동 정리 증명 기술에 의해 구동됩니다. 프로그래머의 설계 결정을 공식적으로 표현할 수 있는 간단한 주석 언어를 제공합니다. ESC/Java는 주석이 달린 소프트웨어를 검사하고 주석에 기록된 설계 결정과 실제 코드 간의 불일치에 대해 경고하며, 코드의 잠재적인 런타임 오류에 대해서도 경고합니다. 이 논문은 검사기 아키텍처 및 주석 언어에 대한 개요를 제공하고 검사기를 수만 줄의 자바 프로그램에 적용한 경험을 설명합니다.