귀납적 불변량
시스템의 모든 가능한 상태에서 항상 참으로 유지되는 성질을 의미한다. 소프트웨어의 안전성을 수학적으로 증명할 때 시스템이 원치 않는 상태에 빠지지 않음을 보장하는 핵심 요소로 사용된다.