다른 답변은 이미 아이디어의 상대적인 장점을 고려했습니다. 나는 또 다른 것을 제안합니다 : 변수 가 0 일 수 있는지 여부를 결정하기 위해 기본 흐름 분석을 사용하십시오 . 그런 다음 잠재적으로 0 인 변수로 나누기를 허용하지 않을 수 있습니다.

x = ...
y = ...

if y ≠ 0:
  return x / y    // In this block, y is known to be nonzero.
else:
  return x / y    // This, however, is a compile-time error.

또는 변하지 않는 변수를 설정하는 지능적인 어설 션 함수를 사용하십시오.

x = ...
require x ≠ 0, "Unexpected zero in calculation"
// For the remainder of this scope, x is known to be nonzero.

이는 정의되지 않은 작업을 완전히 없애는 런타임 오류를 발생시키는 것만큼이나 좋지만, 잠재적 인 오류가 노출되기 위해 코드 경로에 도달 할 필요가 없다는 이점이 있습니다. 불변량을 추적하고 확인하기 위해 중첩 된 타이핑 환경으로 프로그램의 모든 분기를 평가하여 일반적인 유형 검사와 매우 유사합니다.

x = ...           // env1 = { x :: int }
y = ...           // env2 = env1 + { y :: int }
if y ≠ 0:         // env3 = env2 + { y ≠ 0 }
  return x / y    // (/) :: (int, int ≠ 0) → int
else:             // env4 = env2 + { y = 0 }
  ...
...               // env5 = env2

또한 null언어에 그러한 기능이있는 경우 자연스럽게 범위와 검사 까지 확장됩니다 .

답변