정적 분석은 비행기가 추락하지 않음을 증명할 수 없습니다. 대신 더 유용한 것을 증명할 수 있습니다.
추상 해석은 모든 가능한 프로그램 상태를 과대 근사합니다. 추상화 안에서 0으로 나누기에 도달할 수 없다면, 실제 코드에서도 도달할 수 없습니다. 다음은 그 작동 원리와 한계입니다.
정적 분석은 비행기가 추락하지 않음을 증명할 수 없습니다. 하지만 고도계 제어 루프가 0으로 나누기를 절대 하지 않고, 배열 범위를 벗어나는 인덱싱을 절대 하지 않으며, 고정 소수점 누산기에서 오버플로우가 절대 발생하지 않음은 증명할 수 있습니다. 이 둘의 차이가 중요한 이유는,…