TL;DR

  • 형식적 소프트웨어 검증 방법은 직관으로는 도달하기 어려운 극단 사례까지 탐색하게 하며, 기능과 선택지가 많을수록 그 영역이 실제 사용 경로의 대부분을 차지할 수 있음.
  • 고차원 공간에서는 구 내부의 부피 비율이 급격히 감소해 10차원에서는 0.25%, 나머지 99.75%가 모서리 영역에 해당함.
  • 100차원에서는 구 내부의 부피가 약 2/10^70에 불과하며, 100개가 넘는 소프트웨어 기능도 이와 유사하게 조합 수를 폭발시킴.
  • 소프트웨어의 각 독립 선택을 기하학적 차원으로 보면 개별적으로 드문 경로들이 함께 고려될 때 거의 모든 사용량을 차지할 수 있음.
  • scipy.special.gamma와 math.pi를 사용하면 차원별 단위 구와 단위 정육면체의 부피 비율을 계산할 수 있으며, 기능 조합은 완전히 독립적이지 않아도 대규모 시스템에는 상상하기 어려울 만큼 많은 경로가 존재함.

형식 검증이 탐색하는 모서리 영역

  • 형식적 소프트웨어 검증 방법의 장점은 직관이 자연스럽게 이끌지 않는 사례, 즉 소프트웨어의 모서리 영역까지 탐색하게 한다는 점임.
  • 이 개념은 기하학적 의미의 모서리로 생각할 수 있으며, 고차원 상자 안에 구가 있을 때 부피의 거의 전부가 구 바깥쪽 모서리 영역에 위치함.
  • 이는 단순한 비유가 아니라 소프트웨어 선택지를 기하학적으로 생각하는 방식이며, 각각의 독립적인 선택이 하나의 차원에 대응함.
  • 개별적으로 드문 소프트웨어 경로도 함께 고려하면 전체 사용량의 대부분을 차지할 수 있음.

차원 증가에 따른 구의 부피 감소

  • 정사각형 안에 원이 있을 때 면적의 약 78.5%가 원 내부에 위치함.
  • 3차원 상자 안에 공이 있을 때 부피의 52.4%가 공 내부에 위치함.
  • 차원이 증가할수록 구 내부에 있는 부피의 비율이 빠르게 감소함.
  • 10차원 상자 안에 10차원 구가 있을 때 구 내부의 부피는 0.25%이며, 나머지 99.75%가 모서리 영역에 해당함.
  • 100차원으로 올라가면 구 내부 부피의 비율은 약 2/10^70이며, 이는 1 뒤에 0이 70개 붙은 수를 기준으로 한 규모임.

소프트웨어 기능 조합과 고차원 공간

  • 100차원이 순수한 공상처럼 느껴지더라도, 100개가 넘는 기능을 가진 소프트웨어를 생각하면 기능 조합이 기하학적 차원처럼 곱셈적으로 증가함.
  • 기하학적 차원은 완전히 독립적이지만 소프트웨어 기능 조합은 완전히 독립적이지 않음.
  • 논리적으로 일부 기능 조합은 불가능할 수 있음.
  • 확률적으로는 특정 경로를 탐색할 확률이 다른 경로를 탐색할 확률에 조건부일 수 있음.
  • 그럼에도 규모가 큰 소프트웨어 시스템에는 상상하기 어려울 만큼 많은 경로가 존재함.
  • 대규모 운영 환경에서는 발생해서는 안 되는 사건도 정기적으로 발생함.

차원별 부피 비율 계산

  • 차원에 따른 구의 부피를 확인하려면 scipy.special.gamma의 감마 함수와 math.pi의 원주율을 사용할 수 있음.
  • 단위 구의 n차원 부피를 π^(n/2) / Γ(n/2 + 1)로 계산하고, 각 변의 길이가 2인 n차원 단위 정육면체의 부피를 2^n으로 계산함.
  • 두 값을 나누어 구가 정육면체에서 차지하는 부피 비율을 구한 뒤, 1차원부터 19차원까지의 비율을 목록으로 출력함.

주석

  • [1] 이처럼 매우 큰 수에는 명칭이 존재하지만 거의 사용되지 않으며, 과학적 표기법이 훨씬 실용적임. 10^70은 미국식 명명법에서 ten duovigintillion, 유럽식 명명법에서 ten undecilliard로 불림.
  • [2] 기하학적 차원은 완전히 독립적이지만 소프트웨어 기능 조합은 그렇지 않음. 일부 조합은 논리적으로 불가능할 수 있고, 일부 경로의 탐색 확률은 다른 경로의 탐색 여부에 조건부일 수 있음. 그럼에도 대규모 소프트웨어 시스템에는 상상하기 어려울 만큼 많은 경로가 존재하며, 대규모 운영에서는 절대 일어나지 않아야 할 사건도 정기적으로 발생함.