**직관: 어떤 프로그램이 y=f(x)라는 성질을 가지고 있으면 입력을 많이 생성해봐서 출력=f(입력)을 정말로 만족하는지 확인하는 것** 예를 들어, 프로그램 P1은 array를 merge sort를 통해 정렬하는 프로그램, 프로그램 P2는 array를 quick sort를 통해 정렬하는 프로그램이라면, 어쨌든 P1과 P2는 "입력 받은 array를 정렬한다"는 동일한 의미를 갖는 구현체이기 때문에 어떤 입력에 따라 동일하게 정렬된 array를 만들어내야 합니다. 그런데 만약에 P1의 출력과 P2의 출력이 서로 다르면, 누가 틀렸는진 모르겠지만 적어도 하나는 틀렸단 거겠죠?