이번 포스팅에서는 증명에 대해서 다룹니다. 그리고 컴퓨터공학 분야에서 반드시 필요한 프로그램 검증 기법에 대해서도 간단하게 다룹니다. 컴퓨터 공학 분야와 상관없는 사람이라면 프로그램 검증 파트는 건너뛰셔도 좋습니다. 오늘 포스팅은 [이산수학] - Theme 03. 논리적 추론 포스팅에 아주 많이 의존하기에 이 포스팅이 이해가 잘 가지 않는다면 이전 포스팅을 꼭 읽고 공부해주세요.
증명 기술
증명은 어떤 명제가 참인지 거짓인지를 논리적으로 풀어내 밝히는 과정을 말합니다. 그렇기에 앞서 알아본 논리적 추론과 밀접한 연관이 있습니다.
💡 (정의) 증명
가정에서 논리적 법칙을 이용하여 결론을 이끌어내는 것을 말한다. 추론이 참이면 진위 추론이라 하고, 추론이 거짓이면 허위 추론이라고 한다.
증명 문제는 논리 함축 $\text{P} \rightarrow \text{Q}$를 증명하는 것이 대부분인데, 증명하는 방법은 크게 “직접 증명”과 “간접 증명”으로 나뉩니다. 증명 방법은 직접 증명과 간접 증명을 포함하여 5가지로 나눌 수 있습니다.
$\text{P} \rightarrow \text{Q}$의 $\text{vacuous}$ 증명 방법
$\text{P}$가 거짓이라면 $\text{P} \rightarrow \text{Q}$는 항상 참이기에, $\text{P} \rightarrow \text{Q}$가 참이라는 것을 보이기 위해 $\text{P}$가 거짓이라는 것을 보이면 된다.
$\text{P} \rightarrow \text{Q}$의 $\text{trivial}$ 증명 방법
$\text{Q}$가 참이라면 $\text{P} \rightarrow \text{Q}$는 항상 참이기에, $\text{P} \rightarrow \text{Q}$가 참이라는 것을 보이기 위해 $\text{Q}$가 참이라는 것을 보이면 된다.
$\text{P} \rightarrow \text{Q}$의 직접 증명 방법
$\text{P}$가 참이라면 $\text{P} \rightarrow \text{Q}$가 참이기 위해서는, $\text{Q}$도 참이어야 한다.
$\text{P} \rightarrow \text{Q}$의 간접 증명 방법
가정으로부터 추론에 의해 결론에 직접적으로 도달되기 어려운 경우, 간접적으로 결론이 참임을 이끌어내는 방법입니다. 간접 증명 방법에는 대우를 이용하는 방법, 배리법, 존재 증명 방법 이렇게 3가지가 있습니다.
대우를 이용하는 방법
$\text{P} \rightarrow \text{Q}$와 $^\neg\text{Q} \rightarrow ^\neg \text{P}$가 논리적으로 동치이므로 $^\neg\text{Q} \rightarrow ^\neg \text{P}$가 참인 것을 보여줌으로 $\text{P} \rightarrow \text{Q}$가 참인 것을 보여주면 된다.
배리법(반증법)
$\text{P}$가 참인 것을 보이기 위해 $^\neg\text{P}$가 거짓임을 보이면 된다.
존재 증명 방법
$\text{P}(x)$를 $x$라는 변수를 갖는 명제라 하면, $\text{P}(x)$가 참이 되는 $x$가 존재함을 보이는 것이다. 즉, $\exists x, \ \text{P}(x)$이다.
반증을 이용하는 방법
반증을 이용하는 방법에는 반례에 의한 반증 방법과 모순에 의한 반증 방법이 있습니다.
반례에 의한 반증 방법
$\forall x, \ \text{P}(x)$의 형태를 가진 명제가 거짓임을 증명할 때 주로 쓰이는 방법으로, 명제의 부정인 $\exists x, \ ^\neg\text{P}(x)$가 참임을 보이면 된다. 이때, $x$를 반례라고 한다.
모순에 의한 반증 방법
주어진 명제가 거짓임을 보이기 위해 그 명제가 참이라 가정하여 이미 알고 있는 어떤 사실에 모순되는 결론을 유도하면 된다.
수학적 귀납법
새로운 결과를 얻기 위한 논증 방법으로 대표적으로 연역법과 귀납법이 있습니다. 연역법은 일반적 사실이나 원리들을 전제로 추론을 통해 구체적인 새로운 사실을 이끌어내는 방법입니다. 감각적인 경험이 아닌 순수한 논증을 통하여 사실을 이끌어내는 과정입니다. 귀납법은 연역법과는 달리 개별적 사실을 종합해 일반적 원리를 도출하는 것입니다. 관찰과 실험에 기반을 둔 가설을 귀납 추론을 통해 사실을 입증하는 것입니다.
수학적 귀납법은 명제가 참이라는 것을 증명하기 위해 사용하는 방법이며, 또한 객체들의 연속을 정의하기 위하여 사용됩니다.
💡 (정의) 수학적 귀납법
$k$를 임의의 정수라 하면, 어떤 명제 $\text{P}(n)$이 $k \leq n$ (단, $n \in Z$)인 모든 수에 대해 모두 참인 것을 보여주기 위한 방법이다. (이때, $Z$는 정수 체계 집합을 의미한다.)
- $\text{P}(k)$는 참이다. (기초 단계)
- $k \leq n$인 모든 정수 $n$에 대해 $\text{P}(n)$가 참이라 가정하면 $\text{P}(n+1)$도 참이다. (귀납적 단계) </aside>
수학적 귀납법에서 기초 단계에서는 명제 $\text{P}(n)$을 만족하는 가장 작은 조건 값에서 명제 $\text{P}(n)$이 성립하는 것을 보여주고, 귀납적 단계에서는 명제 $\text{P}(n)$이 참이라 할 때 명제 $\text{P}(n+1)$도 참이 되는 것을 보여주는 것입니다.
프로그램 검증
프로그래머들은 어떤 문제를 해결하기 위해 코드로 프로그램을 작성합니다. 그렇지만 작성한 프로그램이 항상 정확한 결과를 도출한다고 확신하는 것은 쉽지 않습니다. 또한 모든 프로그램의 정확성을 검증하는 방법은 존재하지 않습니다. 그렇지만 프로그래머 입장에서는 최대한 프로그램을 검증해야 합니다.
정확한 프로그램이 도기 위해서는 구문 에러(Syntax Error)를 포함하지 말아야 하고, 예상치 못한 종료가 일어나서는 안 되며, 주어진 입력에 대해 정확한 결과를 도출해야 합니다. 이렇게 정확한 결과를 내도록 프로그램을 검증하는 방법에는 정적인 방법과 동적인 방법이 있습니다.
정적인 방법
정적인 방법이란, 프로그램을 실행하지 않고 결함을 찾아내는 것입니다. 여러 참여자들이 모여 프로그램을 검토하여 결함을 찾는 것이며, 앞에서 언급한 추론 규칙과 증명 방법들을 사용합니다. 또한 프로그램을 세부적으로 나누어 각 세부 프로그램이 정확하다는 것을 보임으로 프로그램의 정확성을 증명하기도 합니다.
프로그램을 정적으로 검증하는 가장 기본 방법은 각각의 문장들에 대한 기본 흐름도가 잘 되어있는지 확인하는 것입니다. 일반적으로 다음의 3가지 구조를 검증합니다.
- 순차문: 명령들이 순차적으로 실행되는가?
- 조건문: 주어진 조건이 참인지 거짓인지에 따라 명령문을 선택하여 실행하는가?
- 반복문: 조건이 참인 동안 명령문을 반복 실행하는가?
또한 일반적으로 소스 프로그램을 검토할 때 검토할 체크 리스트는 다음과 같습니다.
- 요구사항 명세서에 기술된 기능은 충분히 코드에서 실행되는가?
- 요구사항 명세서에 기술되지 않은 부가 기능이 코드에서 실행되지는 않는가?
- 메소드 리턴값은 적절하게 사용되는가?
- 모든 지역/전역 변수가 사용 전에 초기화되었는가?
- 메소드는 정확하게 호출되었는가?
동적인 방법
동적인 방법이란, 소프트웨어를 실행하여 결함을 찾아내는 방법입니다. 시험 데이터를 통하여 테스팅하는 방법으로 결함을 찾아내는 것입니다. 크게 블랙박스 테스팅과 화이트박스 테스팅으로 나뉩니다.
- 블랙박스 테스팅: 로직은 신경쓰지 않고 단지, 입/출력값을 테스트하고, 주로 경계값을 테스트합니다.
- 화이트박스 테스팅: 모든 코드가 한 번은 실행되게 입력하는 문장의 범위, 분기, 조건들을 테스트합니다.
