증명

데이크스트라라는 사람은 goto 문이 작은 단위로 분해하는 과정에 방해가 되는 경우가 있다는 사실을 발견했으며 , 모듈을 분해할 수 없다면 합리적으로 증명할 때 필수적인 기법인 분할 정복 접근법을 사용할 수 없게 된다. ( 음.. 알고리즘을 푸는 방법 중 하나인 분할 정복 접근법…‣ 방통대 수업에 나왔었네 아무튼 goto 문이 방해가 된다고 한다. )

그래서 데이크스트라는 goto 문을 ‘좋은’ 사용 방식은 분기와 반복이라는 단순한 제어 구조에 해당한다는 사실을 발견하여 , 모듈이 이러한 종류의 제어 구조만을 사용하면 증명 가능한 단위로까지 모듈을 재귀적으로 세분화하는 것이 가능해 보였다고 한다. ( goto 문이 잘 못했네! )

이러한 제어 구조와 순차 실행과 결합했을때 작성한 모든 프로그램은 순차 , 분기 , 반복 이라는 세 가지 구조만으로 표현할 수 있다는 사실을 증명했으며 해당 사실은 매우 놀라웠다고 한다. ( 놀랍..다..!? 난 아직 잘 모르겠다.. 그러나 확실한 건 모든 프로그램은 순차 분기 반복으로 구성되어 있는 것은 알겠다. 게임 또한 무한한 업데이트를 계속해서 이루고 있으며 플레이어의 IO 값에 따라서 분기가 나뉘어 지며 해당 분기에 따른 작업을 수행한다 그리고 이걸 또 순차적으로 , 반복하지! )

그래서 이런 발견들로 인해 해당 기법을 사용하면 프로그래머는 대규모 시스템을 모듈과 컴포넌트로 나눌 수 있고 , 더 나아가 모듈과 컴포넌트는 입증할 수 있는 아주 작은 기능들로 세분화할 수 있으며 이걸 바로 구조적 프로그래밍이라 한다.

해로운 성명서

데이크스트라라는 사람이 goto 문은 해롭다고 자신의 의견을 피력했으며 오랜시간이 지나오면서 컴퓨터 언어는 진화를 거듭했고 goto 문장은 계속 뒤편으로 밀려나 거의 사라졌다.

기능적 분해

구조적 프로그래밍을 통해 모듈을 증명 가능한 더 작은 단위로 재귀적으로 분해할 수 있게 되었고 , 이는 결국 모듈을 기능적으로 분해할 수 있음을 뜻했다. ( 음.. 사실 작은 단위로 분해한다는 뜻이 잘 와닿지 않는다. )

과학이 구출하다

위의 사실이 옮바름을 끝내 증명을 하지는 않았다. 대개의 프로그래머들은 세세한 기능 하나하나를 엄밀히 증명하려 하지 않았다. ( 아 ㅋㅋ 잘 돌아가기만 하면 된다고 ㅋㅋ )

수학적으로 증명이란 증명가능한 서술이 참임을 입증하는 원리이지만 , 과학에서의 증명은 서술된 내용이 사실이 아니라 서술이 틀렸음을 증명하는 방식으로 동작한다고 한다. 각고의 노력으로도 반례를 들 수 없는 서술이 있다면 목표에 부합할 만큼은 참이라고 본다. ( 오호..! 즉 문제가 없으면 정답이다..! 잘 돌아가기만 하면 옳다..!?)

테스트

프로그램이 잘못되었음을 테스트를 통해 증명할 수는 있지만 , 프로그램이 맞다고 증명할 수는 없다..! ( 키야..! 정말 좋은 문장인 것 같다… 어쩜 말을 이리 잘할까 )

이 같은 사실은 소프트웨어 개발은 수학적인 시도가 아니며 오히려 소프트웨어는 과학과 같다. 최선을 다하더라도 올바르지 않음을 증명하는 데 실패함으로써 올바름을 보여주기 때문이다.

이러한 부정확함에 대한 증명은 입증 가능한 프로그램에만 적용할 수 있으며 제약 없는 goto 문을 사용하는 등의 이유로 입증이 불가능한 프로그램은 테스트를 아무리 많이 수행하더라도 절대로 올바르다고 볼 수 없다. 결국은 goto 문의 좋은 점들만 가져와서 활용해 증명 가능한 더 작은 단위로 분해할 수 있게 되었으며 이를 통해서 우리는 과학적인 프로그래밍이 가능해졌다.. 가 맞을까