덮어쓴 입력의 처음 값🔗

단언은 상태 하나를 기술한다. 최종 상태의 x만으로는 “처음 값보다 1 크다”의 처음 값을 가리킬 수 없다. 명령에 자유로 나타나지 않는 이름 x₀를 명세에 두면 두 상태를 연결할 수 있다. 이것이 유령 변수(ghost variable)다(p.74).

[x = x₀]  x := x + 1  [x = x₀ + 1]

여기서는 x와 x₀가 서로 다른 변수 이름이다. 시작 상태가 x = x₀ = 4라면 끝에서는 x = 5, x₀ = 4다. 프로그램에 x₀ := x를 추가할 필요는 없다. 사전조건이 두 값을 같게 놓고, 프로그램에 x₀가 자유로 나타나지 않는다는 사실이 그 값을 보존한다. 책은 같은 방법으로 입력 지수를 덮어쓰는 빠른 거듭제곱을 설명한다.

이 저장소에서도 유령 변수는 다른 변수와 같은 타입 V를 쓴다. 책의 조건은 x₀ ∉ FV(c)다. 상수 규칙에서 값의 보존만 보일 때 쓰는 x₀ ∉ FA(c)와 구별한다. 예를 들어 y := x₀는 x₀에 대입하지 않으므로 그 값을 보존하지만, 결과 y가 그 값에 의존한다. 책에서 유령 변수는 실행에 영향을 주지도 않는 이름이다.

음수 나눗셈의 두 답🔗

-7을 2로 나눌 때, 0 쪽으로 자르는 몫은 -3이고 나머지는 -1이다. 유클리드 나눗셈의 몫은 -4이고 나머지는 1이다. 두 쌍 모두 피제수 = 몫 × 제수 + 나머지를 만족한다(pp.74–75).

-7 = (-3) × 2 + (-1)
-7 = (-4) × 2 + 1

제수가 양수일 때도 “나머지는 0 이상”이라는 법칙은 첫 모델에서 성립하지 않는다. 두 모델을 모두 허용하는 명세를 증명하려면 양쪽에서 성립하는 법칙만 가정해야 한다. 책에서 말하는 약한 논리는 이런 식으로 허용할 산술 모델의 범위를 넓힌다.

현재 IntOp.denote는 Lean의 Int.ediv와 Int.emod를 사용한다. §2.7 산술 오류의 코드에서 다음 계산을 확인할 수 있다.

오버플로를 검사하지 않는 구현도 모델 선택의 문제가 된다. 표현 가능한 구간 안에서만 수학적 정수 연산과 일치한다고 가정하면, 구간 밖의 결과에 정수 산술의 모든 법칙을 그대로 적용할 수 없다. 이 저장소의 Int 의미론에는 고정 비트 폭이나 오버플로가 없다.

0 나누기도 값을 돌려준다는 가정🔗

책의 술어 논리에서는 식의 연산이 전함수(total function)다. 0 나누기의 값을 특정하지 않아도 각 입력에는 정수 결과가 있어야 한다. 한 모델 안에서 같은 입력으로 연산하면 같은 결과가 나온다는 조건도 포함된다(p.75).

y := x ÷ 0; y := 9

첫 대입이 어떤 정수 r을 저장하든 두 번째 대입은 그 값을 9로 덮어쓴다. 따라서 이 모델에서 명령은 종료하며 최종 y는 9다. 반면 두 번째 대입을 y := y + 9로 바꾸면 최종 값은 r + 9여서 첫 선택을 관찰한다. §2.7의 ZeroDivision과 AComm.eval_assign_overwrite가 이 차이를 다룬다.

현재 Lean의 선택은 다음과 같다. 이것은 저장소가 택한 모델의 계산 결과이며, 모든 언어 구현에 적용되는 0 나누기 법칙은 아니다.

오류가 실행을 멈춘다면🔗

0 나누기를 검사해 즉시 중단하는 언어에서는 위 명령이 y := 9에 도달하지 않는다. 책은 오류 중단을 비종료처럼 취급하면 부분 정확성을 계속 사용할 수 있다고 설명한다 (pp.75–76). 부분 정확성은 정상 종료한 실행의 사후조건만 묻기 때문이다. 그 해석에서 부분 정확성을 증명했다고 해서 오류가 없다는 보장을 얻지는 않는다.

전체 정확성은 정상 종료까지 요구하므로 사정이 다르다. 식의 평가도 오류나 비종료를 낳을 수 있는 언어를 다루려면 그 결과를 표현할 의미론과 논리가 필요하다. 현재 IntExp.eval은 정수를 돌려주는 전함수이고 Comm.eval의 Flat.none은 명령의 비종료를 나타낸다. 별도의 산술 오류 결과나 검사되는 연산은 구현되어 있지 않다. 기존 전체 정확성 정리를 오류를 검사하는 다른 언어의 정리로 바로 옮길 수 없는 이유다.

명세 자체를 맞게 쓰는 일🔗

피보나치나 거듭제곱은 기대 결과를 수학 함수로 짧게 적을 수 있다. 책은 텍스트 조판이나 세금 계산처럼 복잡한 영역에서는 명세도 프로그램만큼 잘못되기 쉽다고 지적한다(p.76). 증명이 확인하는 것은 주어진 명세와 프로그램의 관계다. 그 명세가 실제 요구를 빠짐없이 옮겼는지는 따로 검토해야 한다.

예를 들어 “음수 입력에서는 오류를 알린다”가 요구사항인데 사전조건을 n ≥ 0으로 두었다면, 그 명세는 음수 입력을 다루지 않는다. 해당 정확성 정리를 완전히 증명해도 오류 처리 요구는 남는다. 이 장의 예제를 읽을 때도 사후조건과 함께 사전조건이 제외하는 입력, 사용한 산술 모델, 정상 종료의 뜻을 확인할 수 있다.