Devin.KR

증명과 반례 - 맞다는 것을 어떻게 믿나

개발자KR 조회 1

이 장에서 배우는 것

앞 장에서 조건문이 어떤 입력에서 참이 되는지 살펴보았다. 이제는 한 걸음 더 나아가 “이 조건은 허용한 모든 입력에서 참인가”를 묻는다. 몇 번 실행해서 원하는 값이 나왔다는 사실과, 앞으로 만날 입력에서도 성립한다는 설명은 서로 다른 근거다. 개발할 때에는 두 근거를 함께 사용한다. 실행으로 실수를 찾고, 입력이 커져도 유지되는 이유를 설명한다.

이 장에서는 증명이라는 말을 코드 옆으로 가져온다. 증명은 어려운 기호를 길게 늘어놓는 일이 아니라, 정한 조건에서 결론이 따라오는 이유를 빠짐없이 연결하는 일이다. 실행 결과가 설명을 대신하지는 않지만, 설명의 빈틈을 찾는 데에는 작은 프로그램이 도움이 된다.

  • 직접 증명과 귀류법이 어떤 순서로 결론에 도달하는지 코드와 연결한다.
  • 수학적 귀납법의 시작 조건과 다음 단계 조건을 구분한다.
  • 모든 입력에 대한 주장을 무너뜨리는 작은 반례를 찾는다.
  • 예상값 몇 개 대신 입력과 출력 사이의 성질을 검사한다.
  • 1부터 n까지의 합 공식을 귀납 구조로 확인하고, 틀린 공식의 첫 반례를 출력한다.

문제 상황

작업 목록의 첫 번째 항목에는 점검 한 번, 두 번째 항목에는 두 번, 마지막 n번째 항목에는 n번이 필요하다고 하자. 실행 전에 전체 점검 횟수를 표시하려면 1부터 n까지 더해야 한다. 반복문으로 계산할 수 있지만, 팀원이 곱셈과 나눗셈만으로 계산하는 공식을 제안했다.

def proposed_total(n):
    return n * (n + 1) // 2

이 함수가 맞는지 확인하려고 n이 1, 2, 3일 때 실행했다. 결과는 각각 1, 3, 6이다. 손으로 더한 값과 같다. 여기에서 검토를 끝내도 될까. 다음 함수도 같은 세 입력에서는 같은 결과를 낸다.

def suspicious_total(n):
    return n * (n + 1) // 2 + n // 4

두 번째 함수는 n이 4가 되는 순간 11을 반환한다. 실제 합은 10이다. 앞선 세 번의 성공이 네 번째 입력의 성공까지 보장하지는 않았다. 검토해야 할 것은 성공 횟수만이 아니다. 검사가 어떤 범위를 다루었는지, 아직 실행하지 않은 입력에도 적용되는 이유가 있는지 확인해야 한다.

먼저 입력 범위를 정한다. 이 장에서 n은 0 이상의 정수다. n이 0이면 더할 항목이 없으며, 그 합을 0으로 정한다. 음수와 소수점이 있는 수는 이 장의 함수가 약속한 입력에 포함하지 않는다. 주장이 적용되는 입력의 범위를 전공 수업에서는 정의역이라고 부른다. 정의역을 정하지 않으면 “모든 입력에서 맞다”라는 말도 검사 기준이 되기 어렵다.

조건에서 결론으로 가는 두 가지 길

직접 증명: 가정을 계산 가능한 모양으로 바꾼다

출발 조건을 참이라고 놓고, 그 조건을 이용해 결론까지 이어 가는 방법을 직접 증명(direct proof)이라고 한다. 여기에서 가정은 증명하는 동안 출발점으로 받아들이는 조건이다. 결론은 그 조건으로부터 설명하려는 주장이다.

예를 들어 “짝수 두 개를 더하면 짝수다”를 살펴보자. 짝수는 어떤 정수에 2를 곱한 수다. 따라서 두 짝수를 a = 2 × r, b = 2 × s라고 쓸 수 있다. 두 수의 합은 a + b = 2 × (r + s)다. 정수 r과 s의 합도 정수이므로, 결과는 다시 정수에 2를 곱한 모양이다. 짝수라는 정의에 도착했으므로 설명이 끝난다.

숫자 두 개를 골라 더하는 대신, 임의의 정수 r과 s를 끝까지 그대로 두었다는 점이 중요하다. 임의라는 말은 편한 숫자를 특별히 고르는 것이 아니라, 허용한 숫자 중 무엇을 골라도 같은 계산이 적용된다는 뜻이다. 다음 코드는 그 계산을 작은 범위에서 확인한다.

for r in range(-3, 4):
    for s in range(-3, 4):
        a = 2 * r
        b = 2 * s
        assert a + b == 2 * (r + s)
        assert (a + b) % 2 == 0
print("짝수 덧셈 확인 완료")

assert는 뒤에 놓인 조건이 참인지 확인하는 문장이다. 조건이 거짓이면 실행을 멈추고 AssertionError라는 오류를 알린다. 위 코드는 모든 검사를 통과하면 마지막 문장을 출력한다. %는 나머지를 구하므로, 2로 나눈 나머지가 0인지 검사하면 짝수인지 알 수 있다.

여기서 증명은 코드가 검사한 49쌍에 의존하지 않는다. 모든 정수에 적용되는 식의 변형이 근거다. 코드는 우리가 식을 프로그램으로 옮기는 과정에서 덧셈을 뺄셈으로 잘못 쓰거나 나머지 조건을 뒤집지 않았는지 확인하는 역할을 한다.

귀류법: 반대로 놓았을 때의 충돌을 찾는다

결론이 거짓이라고 가정한 뒤, 그 가정이 이미 받아들인 조건과 함께 성립할 수 없음을 보이는 방법을 귀류법(proof by contradiction)이라고 한다. 함께 참일 수 없는 두 주장에 도착하는 것을 모순이라고 부른다. 프로그램이 실행 중 오류를 냈다는 사실만으로 수학적 모순이 되는 것은 아니다. 어떤 조건끼리 충돌하는지 설명해야 한다.

“양의 짝수 중 가장 큰 수는 없다”를 살펴보자. 반대로 가장 큰 양의 짝수 m이 있다고 가정한다. m이 짝수이므로 m + 2도 짝수다. 또한 양수이며 m보다 크다. 그러면 m이 가장 크다는 가정과 m보다 큰 양의 짝수가 있다는 결론이 충돌한다. 따라서 가장 큰 양의 짝수가 있다는 가정을 유지할 수 없다.

candidate = 12
larger = candidate + 2

assert candidate > 0 and candidate % 2 == 0
assert larger > candidate
assert larger % 2 == 0
print(candidate, larger)

코드는 12를 후보로 골랐을 때 14를 만들어 출력한다. 12 하나를 검사한 것이 증명의 전부는 아니다. 설명에서는 어떤 양의 짝수 m을 후보로 내놓아도 m + 2를 만들 수 있다는 점을 사용했다. 코드는 이 구성을 손으로 만져 보는 작은 실험이다.

또한 이 주장은 양의 짝수 전체에 관한 말이다. “100 이하의 양의 짝수 중 가장 큰 수는 없다”로 범위를 바꾸면 틀린 주장이 된다. 후보 100에 2를 더한 수는 그 범위를 벗어나기 때문이다. 증명 과정에서 새로 만든 값이 약속한 입력 범위 안에 남는지 확인해야 한다.

같은 주장을 확인할 때 증명과 실행이 맡는 역할
방법진행 방식얻는 근거
직접 증명가정에서 식과 정의를 따라간다가정을 만족하는 임의의 입력에 적용되는 이유
귀류법결론을 부정하고 충돌을 찾는다반대 가정을 유지할 수 없는 이유
실행 검사구체적인 값을 넣고 결과를 비교한다실제로 검사한 입력에서의 동작

수학적 귀납법을 코드의 다음 단계로 읽기

0, 1, 2처럼 이어지는 정수에 관한 주장은 두 가지 확인으로 설명할 수 있다. 첫 값에서 성립함을 보이고, 어느 값에서 성립하면 바로 다음 값에서도 성립함을 보이는 방법이다. 전공 수업에서는 이를 수학적 귀납법(mathematical induction)이라고 부른다.

이름 때문에 여러 사례를 보고 규칙을 추측하는 일과 혼동하기 쉽다. 여기에서 필요한 것은 사례의 수가 아니라 연결이다. 첫 값에 닿을 수 있고, 어느 단계에서든 다음 단계로 옮겨 갈 수 있다면, 그 출발점 이후의 모든 정수에 같은 주장이 이어진다.

시작값의 확인과 임의의 단계에서 다음 단계로 가는 설명이 함께 있어야 귀납법이 이어진다

1부터 n까지의 합을 S(n), 제안한 공식을 F(n)이라고 쓰자. S와 F는 각각 입력에 값을 대응시키는 함수의 이름이다. 이 장의 목표는 모든 0 이상의 정수 n에 대해 S(n) = F(n)임을 설명하는 것이다.

합 공식의 증명에 사용하는 값과 식
이름뜻식 또는 값
S(n)1부터 n까지 차례로 더한 합S(0) = 0
F(n)확인하려는 합 공식n × (n + 1) / 2
다음 합기존 합에 새 항목 하나를 더한 값S(k + 1) = S(k) + (k + 1)

시작을 확인한다

먼저 n이 0일 때 S(0)은 정의에 따라 0이다. F(0)도 0 × 1 / 2이므로 0이다. 두 값이 같다. 이 출발점 확인을 기초 단계라고 부른다. 시작을 1로 정해 증명할 수도 있지만, 이 장은 빈 작업 목록까지 다루기 위해 0에서 출발한다.

def formula(n):
    return n * (n + 1) // 2

assert formula(0) == 0

수학의 식에는 / 2라고 쓰고 Python 코드에는 // 2라고 쓴다. //는 정수 나눗셈에서 몫을 구한다. 연속된 두 정수 n과 n + 1 중 하나는 짝수이므로 곱은 2로 나누어떨어진다. 따라서 여기에서는 버려지는 나머지가 없고, 수학의 식과 같은 정숫값을 얻는다.

임의의 단계에서 다음 단계로 옮겨 간다

이제 어떤 0 이상의 정수 k에서 S(k) = k × (k + 1) / 2가 성립한다고 가정한다. 이것을 귀납 가정이라고 부른다. 이 가정은 증명하려는 전체 결론을 미리 참으로 선언하는 것이 아니다. “k에서 참이면 k + 1에서도 참이다”라는 연결을 설명하기 위해 잠시 받아들이는 조건이다.

다음 합은 S(k)에 k + 1을 더한 값이다. 귀납 가정을 대입하면 S(k + 1) = k × (k + 1) / 2 + (k + 1)이다. 뒤의 항을 2 × (k + 1) / 2로 바꾸어 더하면 (k + 1) × (k + 2) / 2가 된다. 이것은 F(k + 1)과 같다.

따라서 k에서 공식이 맞는다는 조건 아래 k + 1에서도 맞는다. 기초 단계와 이 연결을 함께 사용하면 모든 0 이상의 정수에 대한 설명이 된다. 다음 코드는 연결에 사용한 등식을 여러 k에서 확인한다.

for k in range(8):
    next_from_previous = formula(k) + (k + 1)
    next_from_formula = formula(k + 1)
    assert next_from_previous == next_from_formula
print("다음 단계 등식 확인 완료")

반복문의 종료값을 아무리 크게 올려도 이 코드 자체가 무한한 정수 전체를 검사하지는 않는다. 전체에 대한 근거는 k의 특정 값에 의존하지 않는 식의 변형이다. 완성 코드에서는 이 구조를 실행 가능한 검사로 옮기되, 출력에 검사 범위를 명시한다.

반례와 성질을 검사하는 코드

“모든 입력에서 성립한다”라는 주장이 틀렸음을 보이려면, 허용한 입력 중 주장이 성립하지 않는 값 하나면 충분하다. 이 값을 반례(counterexample)라고 한다. 반례는 단순히 프로그램을 멈추게 한 입력이 아니다. 약속한 조건을 만족하면서 결론을 어기는 입력이어야 한다.

예를 들어 n이 0 이상의 정수라는 약속에서 음수를 넣어 이상한 결과를 얻었다면, 그것만으로 합 공식의 반례가 되지는 않는다. 반대로 n이 4일 때 틀린 공식이 11을 돌려준다면, 4는 약속한 범위 안에 있고 실제 합 10과 다르므로 반례다.

검사를 만들 때는 예상 출력 몇 개만 적을 수도 있고, 여러 입력에 공통으로 적용되는 관계를 적을 수도 있다. 입력과 출력이 만족해야 할 관계를 성질(property)이라고 한다. 이런 성질을 여러 입력에서 검사하는 접근을 성질 기반 테스트(property-based testing)라고 부른다. 외부 도구 없이도 반복문으로 그 생각을 구현할 수 있다.

  • 빈 범위의 합은 0이어야 한다.
  • n까지의 합은 n - 1까지의 합보다 정확히 n만큼 커야 한다.
  • 공식으로 구한 값은 반복해서 더한 값과 같아야 한다.

각 성질은 서로 다른 실수를 잡는다. 다음 단계와의 차이만 확인하면 모든 결과에 같은 상수가 더해진 오류를 놓칠 수 있다. 예를 들어 항상 5를 더한 공식도 이웃한 결과의 차이는 n이다. 그래서 시작값과 다음 단계 조건을 함께 확인한다. 기초 단계와 귀납 단계가 모두 필요하다는 설명이 테스트 설계에도 그대로 이어진다.

작은 입력부터 비교하면 틀린 공식이 처음 어긋나는 입력 4를 재현할 수 있다

실무에서 만나는 곳

반복문 안에서 계속 유지되어야 하는 조건을 전공 수업에서는 루프 불변식(loop invariant)이라고 부른다. 불변이라는 말은 변수의 값이 바뀌지 않는다는 뜻이 아니다. 변수는 바뀌어도 그 변수들 사이의 관계가 유지된다는 뜻이다. 합을 누적하는 반복문에서는 “현재 누적값은 지금까지 처리한 수들의 합이다”가 그런 관계다.

예를 들어 처리한 항목 수와 누적 점검 횟수를 함께 갱신한다면, 시작 전에 두 값이 모두 0인지 확인한다. 새 항목을 처리할 때는 항목 수를 하나 늘리고 그 번호만큼 누적값을 늘린다. 반복이 끝났을 때 항목 수가 n이라면, 유지된 관계를 이용해 누적값이 S(n)이라고 설명할 수 있다.

이 사고방식은 묶음 처리에서도 쓰인다. “완료 목록의 길이는 성공적으로 처리한 항목 수와 같다”라는 성질을 세우면, 실패한 항목까지 완료 수에 포함한 실수를 찾을 수 있다. 다만 그 성질만으로 각 항목의 처리 내용까지 맞았다고 결론 내리지는 않는다. 검사가 보장하는 결론을 성질의 범위 안에서 읽어야 한다.

반례를 발견하면 입력과 실제값, 기대값을 함께 남기는 것이 좋다. 입력 범위를 줄여도 같은 실패가 나는지 확인하면 원인을 읽기 쉬워진다. 이후에도 그 입력을 다시 검사하도록 남겨, 이미 고친 오류가 되살아나는지 확인하는 검사를 회귀 테스트라고 부른다.

완성 코드

다음 내용을 main.py로 저장한다. 프로그램은 0부터 100까지 올바른 공식을 귀납 구조에 맞춰 검사하고, 0부터 20까지 틀린 공식의 첫 반례를 찾는다. 입력은 작은 수부터 차례로 만들므로 난수가 필요 없고 실행 결과도 일정하다. 함수의 입력은 설명한 정의역을 따른다고 가정한다.

def sum_formula(n):
    return n * (n + 1) // 2


def wrong_formula(n):
    return n * (n + 1) // 2 + n // 4


def sum_by_loop(n):
    total = 0
    for value in range(1, n + 1):
        total += value
    return total


def verify_induction_structure(limit):
    accumulated = 0
    assert sum_formula(0) == accumulated, "기초 단계 실패"

    for k in range(limit):
        assert accumulated == sum_formula(k), "현재 단계 실패"
        next_sum = accumulated + (k + 1)
        assert next_sum == sum_formula(k + 1), "다음 단계 실패"
        accumulated = next_sum

    return accumulated


def find_first_counterexample(limit):
    for n in range(limit + 1):
        expected = sum_by_loop(n)
        actual = wrong_formula(n)
        if actual != expected:
            return n, expected, actual
    return None


def main():
    limit = 100
    total = verify_induction_structure(limit)
    print(f"귀납 구조 검사 범위: 0부터 {limit}까지")
    print(f"기초 단계: S(0) = {sum_formula(0)}")
    print(f"다음 단계 검사: {limit}회 통과")
    print(f"S({limit}) = {total}")

    search_limit = 20
    result = find_first_counterexample(search_limit)
    print(f"틀린 공식 탐색 범위: 0부터 {search_limit}까지")

    if result is None:
        print("검사 범위에서 반례를 찾지 못함")
    else:
        n, expected, actual = result
        print(f"첫 반례: n = {n}")
        print(f"반복 합: {expected}")
        print(f"틀린 공식: {actual}")


if __name__ == "__main__":
    main()

줄별 해설

sum_formula는 증명한 식을 그대로 계산한다. wrong_formula는 반례 탐색을 위해 일부러 n // 4를 더한다. 두 함수 모두 0부터 3까지는 같은 값을 내므로, 처음 몇 개의 성공만 확인하는 검사의 한계를 보여 준다.

sum_by_loop는 공식을 사용하지 않고 1부터 n까지 직접 더한다. range(1, n + 1)은 끝값 n + 1을 포함하지 않으므로 마지막으로 더하는 값은 n이다. n이 0이면 반복할 값이 없어서 초기값 0을 반환한다. 비교 기준을 다른 계산 방법으로 만들면 같은 오타를 두 곳에 복사할 위험을 줄일 수 있다. 물론 비교 기준의 코드도 검토해야 한다.

verify_induction_structure의 accumulated = 0은 아직 아무것도 더하지 않은 상태다. 바로 다음 assert는 기초 단계다. 반복문에 들어가기 전부터 출발점이 맞는지 확인한다. 이 검사를 반복문 밖에 두었기 때문에 검사 한도가 0이어도 시작값은 확인한다.

for k in range(limit)에서 k는 0부터 limit - 1까지 움직인다. 반복문 본문의 첫 assert는 현재 누적값이 F(k)와 같은지 검사한다. next_sum은 그 누적값에 새 항 k + 1을 더한 값이다. 이어지는 assert는 새 값이 F(k + 1)과 같은지 검사한다. 마지막 대입으로 다음 반복을 준비한다.

반복문을 도는 동안 유지하려는 관계는 accumulated == sum_formula(k)다. 한 번의 반복을 마치면 다음 k에 맞는 누적값이 준비된다. limit이 100이면 0에서 1로 가는 연결부터 99에서 100으로 가는 연결까지 100번 검사한다. 끝에서 돌려주는 누적값은 S(100)이다.

find_first_counterexample은 0부터 탐색 한도까지 입력을 하나씩 만든다. expected는 기준이 되는 반복 합이고, actual은 검사 대상인 틀린 공식의 결과다. 두 값이 다르면 즉시 입력과 두 결과를 반환한다. 작은 순서로 탐색했으므로 반환한 입력은 검사 범위에서 가장 작은 반례다.

return n, expected, actual은 여러 값을 튜플(tuple)이라는 묶음으로 반환한다. 뒤의 n, expected, actual = result는 그 묶음을 세 변수에 나누어 담는다. 차이를 발견하지 못하면 None을 반환한다. None은 여기에서 “발견한 반례 정보가 없다”를 나타내는 특별한 값이다.

main은 검사 범위와 결과를 출력한다. if result is None일 때도 “공식이 참이다”라고 출력하지 않는다. 검사한 범위에 반례가 없었다는 사실만 말한다. 마지막 조건은 파일을 직접 실행했을 때 main 함수를 호출하는 Python의 실행 진입점이다.

assert는 개발 중 가정을 점검하는 용도다. Python을 최적화 옵션인 -O와 함께 실행하면 assert 검사가 생략될 수 있다. 이 장에서는 지정한 명령인 python3 main.py로 실행한다. 서비스에서 사용자의 잘못된 입력을 거절하는 처리는 assert에 맡기지 않는다.

실행 결과

macOS 또는 Linux의 터미널에서 main.py가 있는 디렉터리로 이동한 뒤 실행한다. Python 3.12 이상에서 별도 패키지 없이 실행되고, 결과를 출력한 뒤 종료한다.

python3 main.py
귀납 구조 검사 범위: 0부터 100까지
기초 단계: S(0) = 0
다음 단계 검사: 100회 통과
S(100) = 5050
틀린 공식 탐색 범위: 0부터 20까지
첫 반례: n = 4
반복 합: 10
틀린 공식: 11

앞의 네 줄은 유한한 범위의 실행 검사 결과다. 모든 0 이상의 정수에 대한 공식의 근거는 앞서 설명한 기초 단계와 임의의 k에 대한 식의 변형이다. 뒤의 결과에서 n = 4 하나만으로 틀린 공식의 전체 주장은 반박된다. 모든 입력에 대한 주장을 뒷받침하는 일과 무너뜨리는 일에 필요한 근거는 이렇게 다르다.

실무에서 자주 틀리는 것

몇 개의 성공을 전체의 성공으로 출력한다

다음 코드는 실행한 범위보다 넓은 결론을 출력한다. 틀린 공식도 0부터 3까지는 통과한다.

for n in range(4):
    assert wrong_formula(n) == sum_by_loop(n)
print("모든 정수에서 맞음")

검사 범위를 넓히고, 출력 문장도 관찰한 사실로 제한한다. 범위를 넓히는 일만으로 증명이 되지는 않는다. 다음 수정에서는 반례를 발견하면 assert가 멈추므로 성공 문장까지 도달하지 않는다.

limit = 20
for n in range(limit + 1):
    assert wrong_formula(n) == sum_by_loop(n)
print(f"0부터 {limit}까지 일치")

차이가 일정하면 시작값도 맞다고 생각한다

다음 함수는 올바른 합보다 항상 5만큼 크다. 이웃한 두 값의 차이만 검사하면 오류를 찾지 못한다.

def shifted_formula(n):
    return n * (n + 1) // 2 + 5

for n in range(1, 11):
    assert shifted_formula(n) - shifted_formula(n - 1) == n

시작값 검사를 추가한다. 수정한 코드는 첫 assert에서 멈춰 잘못된 출발점을 드러낸다. 검사 코드의 목적은 대상 함수를 무조건 통과시키는 것이 아니라, 약속이 어긋나면 알리는 데 있다.

assert shifted_formula(0) == 0
for n in range(1, 11):
    assert shifted_formula(n) - shifted_formula(n - 1) == n

검사 대상과 같은 공식을 기대값으로 쓴다

기대값도 잘못된 식으로 만들면 두 값은 함께 틀린다. 아래 검사는 n이 4여도 차이를 발견하지 못한다.

n = 4
expected = n * (n + 1) // 2 + n // 4
actual = wrong_formula(n)
assert actual == expected

이미 알고 있는 작은 결과나 다른 계산 과정을 기준으로 쓴다. 다음 코드는 반복 덧셈을 사용하며, 두 값이 다르므로 의도대로 실패한다.

n = 4
expected = sum_by_loop(n)
actual = wrong_formula(n)
assert actual == expected

끝값을 빠뜨려 반례 바로 앞에서 멈춘다

range의 끝값은 포함되지 않는다. “4까지 검사한다”는 의도로 다음 코드를 쓰면 실제로는 3까지만 검사한다.

limit = 4
for n in range(limit):
    assert wrong_formula(n) == sum_by_loop(n)

상한을 포함하는 약속이라면 1을 더한다. 수정한 코드는 n이 4일 때 반례를 발견한다. 함수 이름과 출력에서도 상한을 포함하는지 일관되게 표현하는 것이 좋다.

limit = 4
for n in range(limit + 1):
    assert wrong_formula(n) == sum_by_loop(n)

한눈에 보기

증명 방법과 테스트를 코드 검토에서 구분하는 기준
개념핵심 질문코드에서 확인할 것
직접 증명가정으로부터 결론이 이어지는가정의에 맞게 값을 구성했는가
귀류법반대 가정이 어떤 조건과 충돌하는가만든 값이 약속한 범위에 속하는가
수학적 귀납법시작과 다음 단계의 연결이 있는가초기값과 갱신 관계가 모두 맞는가
반례허용한 입력에서 결론이 깨지는가입력·기대값·실제값을 재현할 수 있는가
성질 기반 테스트여러 입력에 적용할 관계는 무엇인가어떤 성질과 범위를 검사했는가

증명은 실행하지 않은 입력에도 적용되는 이유를 설명한다. 테스트는 실제로 작성한 코드가 선택한 입력에서 어떤 동작을 하는지 보여 준다. 식을 증명했더라도 코드를 잘못 옮길 수 있고, 코드가 많은 입력을 통과하더라도 설명에 빈틈이 있을 수 있다. 두 활동을 함께 사용하면 주장과 구현을 각각 검토할 수 있다.

연습 문제

  1. 어떤 함수 G(n)가 모든 양의 정수 n에서 G(n) - G(n - 1) = n을 만족한다. 이 조건만으로 G(n)가 1부터 n까지의 합이라고 결론 내릴 수 있는지 설명하라. 결론을 내릴 수 없다면 반례 함수를 코드로 작성하라.

  2. 완성 코드의 틀린 공식을 n * (n + 1) // 2 + n // 7로 바꾸라. 0부터 20까지 탐색할 때 첫 반례의 입력, 기대값, 실제값을 먼저 예상한 뒤 실행으로 확인하라.

  3. “홀수 두 개를 더하면 짝수다”를 직접 증명하라. 두 홀수를 2 × r + 1과 2 × s + 1로 놓고 설명한 뒤, r과 s가 각각 -2부터 2까지일 때 검사하는 코드를 작성하라.

  4. verify_induction_structure(0)은 무엇을 반환하는가. 이 호출에서 기초 단계와 다음 단계가 각각 몇 번 검사되는지 설명하고 코드로 확인하라.

정답과 해설

1. 다음 단계의 차이만으로 시작값을 정할 수 없다

결론을 내릴 수 없다. 올바른 합에 같은 상수를 더하면 이웃한 값의 차이에서는 그 상수가 사라진다. 아래 함수는 모든 0 이상의 정수에서 합보다 2만큼 크지만, 양의 정수에서 차이 조건을 만족한다.

def g(n):
    return n * (n + 1) // 2 + 2

assert g(0) != 0
for n in range(1, 21):
    assert g(n) - g(n - 1) == n
print("차이는 맞지만 시작값은 다름")

전체에 대한 차이 조건은 식에서도 확인할 수 있다. G(n)과 G(n - 1)을 빼면 더해 둔 2가 사라지고 n이 남는다. 합을 결정하려면 G(0) = 0이라는 시작 조건도 필요하다.

2. 첫 반례는 7이다

0부터 6까지는 n // 7이 0이고, 7에서 처음 1이 된다. 따라서 첫 반례는 n = 7, 기대값은 28, 실제값은 29다. 완성 코드의 wrong_formula 본문을 바꾼 뒤 실행하면 해당 세 값이 출력된다.

def wrong_formula(n):
    return n * (n + 1) // 2 + n // 7

assert sum_by_loop(7) == 28
assert wrong_formula(7) == 29
assert find_first_counterexample(20) == (7, 28, 29)
print("첫 반례 확인 완료")

이 코드는 완성 코드의 나머지 함수들과 함께 실행한다. 탐색 한도를 6으로 줄이면 None을 반환한다. 이는 반례를 찾지 못했다는 뜻이며, 바꾼 공식이 참이라는 뜻은 아니다.

3. 홀수 두 개의 합을 2의 배수로 정리한다

합은 (2 × r + 1) + (2 × s + 1) = 2 × (r + s + 1)이다. r + s + 1은 정수이므로 합은 짝수다. 음의 정수도 같은 계산을 따르므로 검사 범위에 음수를 포함할 수 있다.

for r in range(-2, 3):
    for s in range(-2, 3):
        a = 2 * r + 1
        b = 2 * s + 1
        assert a + b == 2 * (r + s + 1)
        assert (a + b) % 2 == 0
print("홀수 덧셈 25쌍 확인 완료")

25쌍의 실행은 코드 확인이고, 임의의 r과 s로 정리한 식은 전체 정수에 대한 설명이다. 두 근거의 범위를 구분해서 읽는다.

4. 기초 단계만 검사하고 0을 반환한다

기초 단계는 한 번 검사한다. range(0)에는 반복할 값이 없으므로 다음 단계는 한 번도 검사하지 않는다. accumulated는 초기값 0을 유지한다.

result = verify_induction_structure(0)
assert result == 0
print(result)

출력은 0이다. 검사 한도가 0이어도 실행이 끝나고 시작 조건을 확인한다는 점은 경계 입력을 설계할 때 유용하다. 경계 입력은 0이나 상한처럼 처리 범위의 끝에 놓인 입력을 뜻한다. 다음 장에서는 이런 명확한 조건을 바탕으로, 여러 값을 모아 다루는 집합을 살펴본다.

댓글 0

아직 댓글이 없습니다. 첫 댓글을 남겨 보세요.

댓글을 남기려면 로그인이 필요합니다.