EWD249 · 1969 · 아인트호벤 공과대학

구조적 프로그래밍에 관한 노트

"느린 머리를 가진 인간으로서 나는 매우 작은 두뇌를 가지고 있으며, 나의 한계와 함께 살아가고 그것에 완전한 인정을 주는 것이 낫다는 것을 배웠다."

Notes on Structured Programming 단계적 정제 정확성 증명 추상화 계층

해설이 글은 무엇을 말하는가

구조적 프로그래밍의 개념적 기초가 여기 있다. 다익스트라는 1969년, 자신이 만든 연구 그룹이 해산되고 우울증으로 입원해 있던 시기에 — "주로 치료적 이유로" — 이 노트를 썼다.

다익스트라는 처음에 솔직히 인정한다. 그가 진정 관심을 갖는 것은 대규모 프로그램의 구성이지만, 시연 예제는 작아야 한다 — 그리고 바로 이 규모의 차이가 프로그래밍 어려움의 주요 원천이다. 한 살짜리 아이는 시속 1마일로 기어 다니고, 초음속 제트기는 시속 1000마일로 난다. 천 배의 비율은 이미 우리의 상상력을 넘어선다. "한 번 할 수 있으면 천 번도 할 수 있다"는 귀납은 거짓이다.

그다음 그는 신뢰성을 논한다. 27비트 곱셈기가 올바른지 모든 경우를 시험하려면 — 10,000년 이상이 걸린다. 메커니즘을 블랙박스로 두는 한 정확성의 납득할 만한 증명은 불가능하다. 우리의 유일한 희망은 메커니즘의 구조를 고려하는 것이다. 그리고 여기서 이 노트의 가장 유명한 한 줄이 나온다 — "프로그램 테스팅은 버그의 존재를 보여줄 수 있지만, 결코 그 부재를 보여줄 수는 없다."

그렇다면 우리는 어떻게 프로그램을 이해하는가? 다익스트라는 세 가지 정신적 도구를 든다. 연접·선택을 위한 열거(enumeration), 반복·재귀를 위한 수학적 귀납법, 그리고 열거에 대한 호소를 줄이기 위한 추상화. 그는 단순한 루프 하나를 정직하게 증명해 보이며, 그 증명의 길이에 스스로 화를 낸다 — 그리고 거기서 교훈을 끌어낸다. 정직하게 겸손하고, 단순한 구조에 스스로를 제한하고, "영리한 구조"를 전염병처럼 피하라.

노트의 절정은 단계적 정제(stepwise refinement)다. 처음 천 개의 소수를 인쇄하는 프로그램을, 다익스트라는 "한 번에 가능한 한 적게 결정하는" 방식으로 — 추상적 명세에서 시작해 한 결정씩 정제해 나가며 — 구성한다. 그 과정에서 결국 에라토스테네스의 체에 가까운 효율적 알고리즘에 도달한다. 그리고 그는 프로그램을 고립된 객체가 아니라 "관련 프로그램들의 가족"의 일원으로 보아야 한다고, 계층적 추상화가 명료성·모듈성·수정 가능성의 열쇠라고 결론짓는다.

원문 · 01우리의 능력 한계

이 노트들은 "나 자신에게 보내는 편지"의 성격을 갖는다. 나는 같은 논증을 계속해서 반복하고 있음을 발견했다. 만약 이 노트들이 영감의 원천이 되거나 프로그래머라는 직업에 대한 새로운 인식을 당신에게 준다면, 나의 목표 중 일부는 달성된 것이다.

내가 진정으로 관심을 갖는 것은 대규모 프로그램의 구성이지만, 실용적인 이유로 시연 프로그램들은 작아야 한다. 내 기본적인 문제는 바로 이 규모의 차이가 프로그래밍에서 우리가 겪는 어려움의 주요 원천 중 하나라는 것이다. 우리는 규모의 차이를 무시하도록, 그것을 "점진적인 차이이므로 본질적이지 않다"고 취급하도록 너무 잘 훈련되어 있다. 우리는 한 번 할 수 있으면 두 번도 할 수 있고, 귀납에 의해 필요한 만큼 여러 번 할 수 있다고 우리 자신에게 말하지만, 이것은 사실이 아니다. 천 배의 요소는 이미 우리의 상상력을 훨씬 넘어선다.

한 살짜리 아이가 네 발로 기어 다니는 속도는 시속 약 1마일이다. 그러나 시속 천 마일의 속도는 초음속 제트기의 속도다. 이동 능력을 가진 물체로 고려했을 때, 아이와 제트기는 비교 불가능하다. 눈을 감고 멀리서 커다란 말이 전속력으로 다가오는 것을 "보는" 것은 가능하다. 그러나 이 커다란 짐승들 천 마리가 다가오는 것을 같은 방식으로 보려면 — 정신적으로 불가능하다.

요약하자면, 느린 머리를 가진 인간으로서 나는 매우 작은 두뇌를 가지고 있으며, 나의 한계와 함께 살아가고 그것에 완전한 인정을 주는 것이, 그것을 무시하려는 헛된 노력보다 낫다는 것을 배웠다.

원문 · 02메커니즘의 신뢰성

몇 년 전 내 대학교 구내에 기계가 설치되었고, 그 문서에 따르면 27비트 정수 두 개의 고정 소수점 곱셈을 위한 회로가 있었다. 합당한 질문은 "이 곱셈기가 올바른가?"이다. 순진한 답변은 "곱셈의 수는 유한하다, 즉 2⁵⁴개이니, 그것들을 모두 시도해보자"이다. 그러나 단일 곱셈이 수십 마이크로초만 걸리지만, 이 유한한 집합에 필요한 총 시간은 10,000년 이상이다. 곱셈기와 같은 단일 구성요소조차도 철저한 테스팅은 완전히 문제가 되지 않는다.

직관적인 결론은 다음과 같다. 메커니즘이 블랙박스로 간주되는 한 정확성에 대한 납득할 만한 증명이 불가능하므로, 우리의 유일한 희망은 메커니즘을 블랙박스로 간주하지 않는 데 있다. 나는 이것을 "메커니즘의 구조를 고려하기"라고 부른다. 프로그램 정확성이 확립될 수 있는 정도는 순전히 외부 사양과 행동의 함수가 아니라 그 내부 구조에 결정적으로 의존한다.

개별 구성요소의 정확성 확률이 p와 같다면, N개의 구성요소로 구성된 전체 프로그램의 정확성 확률은

구성요소 정확성의 곱
P = pN
P 전체 프로그램이 올바를 확률 · p 개별 구성요소가 올바를 확률 · N 구성요소의 수. N이 매우 클 것이므로, P가 0과 유의미하게 다르려면 p는 매우, 매우 1에 가까워야 한다.

나의 결론은 비용/성능 비율의 최소화로서 프로그래밍을 주로 고려하는 것을 멈추는 것이 가장 긴급하게 되고 있다는 것이다. 프로그래밍은 훨씬 더 지적 도전이다. 프로그래밍의 예술은 복잡성을 조직하는 예술이며, 그 잡종 혼돈을 가능한 한 효과적으로 제어하고 피하는 예술이다.

유명한 따름정리 프로그램 테스팅은 버그의 존재를 보여주는 데 사용될 수 있지만, 결코 그 부재를 보여줄 수는 없다.

원문 · 03세 가지 정신적 도구

프로그램(또는 그 정확성의 증명)을 이해하는 데 사용할 수 있는 정신적 보조 수단 중에서 명시적으로 언급하고 싶은 세 가지가 있다 — 열거, 수학적 귀납법, 추상화.

열거. 나는 열거에 대한 호소를, 조건부 절이 두 경우를 구별하는 것을 포함하여, 열거된 진술 집합에 의해 유발될 수 있는 계산의 속성을 순서대로 검증하려는 노력으로 간주한다. 다음 프로그램 조각이 관계 0 ≤ r < dd를 불변식으로 남긴다는 것을 — 두 경우를 따라가며 — 확립할 수 있다.

열거적 추론의 예
// 가정: 0 ≤ r < dd  가 성립한다
dd := dd / 2;          // 이후: 0 ≤ r < 2·dd
if dd <= r do r := r - dd;

// 경우 1: dd <= r  →  dd <= r < 2·dd  →  감소 후 0 ≤ r < dd
// 경우 2: dd >  r  →  건너뜀         →        0 ≤ r < dd
// 두 경우 모두 0 ≤ r < dd 가 불변으로 유지된다

수학적 귀납법. 이것은 (반복 절로 표현될 수 있는) 루프와 재귀적 프로시저를 다룰 수 있게 하는 유일한 추론 패턴이다. 나는 "선형 검색 정리" — 수열에서 조건을 만족시키는 첫 값을 찾는 루프의 정확성 — 를 귀납으로 증명한다. 솔직히 말하면, 그 증명의 허세와 길이가 나를 화나게 한다. 그러나 나는 그것을 긴급한 조언으로 해석한다 — 정직하게 겸손하게 하고, 가능할 때마다 단순한 구조로 스스로를 제한하며, 모든 지적 겸손 속에서 전염병처럼 "영리한 구조들"을 피하라.

추상화. 이것은 주제 전체에 스며든다. 계산에서 시작하여, 알고리즘은 조작되는 특정 값에서 추상화했을 때 남는 것이다. "변수"의 개념은 현재 값에서의 추상화를 나타낸다. 누군가는 변수가 프로그래밍에 사용되는 방식을 일단 이해하면 프로그래밍의 정수를 이해한 것이라고 말했다. 우리는 추상화를 열거적 추론에 대한 요구를 줄이기 위한 우리의 주요 정신적 기법으로 인식해야 한다.

원문 · 04단계적 정제

나는 잘 구조화된 프로그램을 기성품으로 제시하는 대신, 그러한 프로그램의 구성 과정을 매우 상세히 기술하려 한다. 과제는 컴퓨터에 처음 천 개의 소수의 표를 인쇄하도록 지시하는 것이다.

나의 접근의 기본 패턴은 프로그램을 작은 단계로 구성하여, 매번 가능한 한 적게 결정하는 것이다. 프로그램의 가장 단순한 형태는 "처음 천 개의 소수를 인쇄하라"이다. 다음 정제에서 우리는 단일 변수 "table p"를 도입하고, 계산을 두 행동의 시간 연속으로 기술한다.

단계적 정제 — 설명 0 → 1 → 2
// 설명 0
begin "처음 천 개의 소수를 인쇄하라" end

// 설명 1 — 단일 변수 table p 도입
begin variable "table p";
      "table p를 처음 천 개의 소수로 채워라";
      "table p를 인쇄하라"
end

// 설명 2 — 표현 결정: integer array
1a = "integer array p[1:1000]"
1b = "k가 1..1000에 대해 p[k]를 k번째 소수로"
1c = "k가 1..1000에 대해 p[k]를 인쇄"

설명 1을 적어 내릴 때 우리의 원래 문제 진술이 얼마나 적게 고려되었는지를 강조하고 싶다. 출력 레이아웃의 요구 사항이나 "소수"라는 개념이 정확히 무엇을 의미하는지는 여전히 무관하다. 우리 원래 문제의 두 다소 독립적인 측면이 우리의 두 구성 행동 각각에 할당되었다. 이것은 "나누고 통치하라"는 황금 원칙을 적용하려는 우리의 노력에서 성공적이었음을 시사한다.

2b — "p[k]를 k번째 소수로 만들어라" — 의 정제를 계속하면, 우리는 j를 다음 소수까지 증가시키는 루프에 도달한다. 효율성을 위해 2를 따로 다루고 홀수 소수만 시도하며, 시도할 소수가 이미 배열 p의 채워진 부분에 있다는 사실을 이용한다. 결국 우리는 소수 인수의 배수들을 저장하는 배열 mult를 도입하며 — 이것이 우리의 계산을 에라토스테네스의 체의 구현에 가깝게 만들었다.

가장 두드러진 관찰은 매우 단순한 프로그램에 대한 우리의 처리가 매우 길어졌다는 것이다. 그러나 우리는 격려적인 경험도 했다. 불쌍한 프로그래머가 한꺼번에 모든 것을 결정할 수 없다는 사실을 인정하면서, 우리는 이 프로그램을 한 번에 하나의 결정씩 구축했고, 최종 결정이 어떻게 취해지든 이전 수준들의 코딩이 여전히 유효하다.

원문 · 05프로그램 가족과 계층

나는 프로그램을 고립된 객체가 아니라 "관련 프로그램들"의 가족의 구성원으로 간주하는 것을 선호한다. 큰 프로그램은 수명 동안 수정되어야 한다. 만약 프로그램이 두 버전으로 존재해야 한다면, 나는 한 프로그램을 다른 것의 수정으로 간주하지 않을 것이다. 두 버전이 공통 조상 — 두 버전이 공통으로 갖는 것을 구현하는 추상적 프로그램 — 의 다른 자식으로 간주될 수 있다면 훨씬 더 매력적이다. 그러면 두 버전은 가능한 한 정확성 증명을 공유하고, 같은 분해의 결과로서 같은 추상적 프로그램을 공유한다.

단계적 구성의 결과는 트리 구조를 갖는다. 이것은 여러 이점을 갖는다 — 명료성(어떤 수준에서든 기능적 구조가 직접 표현된다), 모듈성(분명한 인터페이스로 부분들이 독립적으로 개발·테스트된다), 수정 가능성, 유지보수성, 그리고 개념적 관리(프로그래머가 동시에 모든 세부사항을 생각할 필요가 없다).

프로그램이 분해에 의해 구성되면, 정확성 증명도 자연스럽게 분해에 의해 구성된다. 각 분해 단계에서 우리는 "만약 부품들이 올바르게 작동한다면, 전체가 올바르게 작동한다"를 증명한다. 이것이 증명을 관리 가능하게 만드는 관심사의 분리다.

노트의 결론 구조적 프로그래밍은 단순히 goto 문을 피하는 것이 아니다. 그것은 프로그램을 인간이 이해하고 추론할 수 있는 방식으로 구성하는 것에 관한 것이다. 우리의 주요 도구는 추상화이고, 우리의 주요 제약은 우리 자신의 지적 능력이다.

모션핵심 개념 — 추상화 계층의 단계적 정제

"처음 천 개의 소수를 인쇄하라"라는 하나의 추상적 명령이, 한 번에 한 결정씩 — 무엇을, 어떤 표현으로, 어떤 알고리즘으로 — 정제되어 구체적 코드의 트리로 자라난다. 각 수준에서 결정되는 것은 최소한이며, 위 수준은 아래 수준의 세부를 알 필요가 없다. 아래 모션은 다익스트라가 노트에서 실제로 밟은 정제 과정을 따라간다.

한 결정씩 — 추상에서 구체로 단계 01 / 5
스페이스: 재생 · ← → : 이동 · R: 리셋