한 메모리 칸을 바꿀 때, 떨어진 칸이 그대로임을 어떻게 증명할까요?

주소 변수 x가 100, y가 200을 가리키고 힙에 100↦10과 200↦20이 있다고 합시다. 명령 [x] := 11은 주소 100의 값만 바꿉니다. 우리가 원하는 결론은 100↦11과 200↦20입니다.

보통 논리의 문장만 나란히 적으면 x와 y가 같은 주소일 가능성을 따로 배제해야 합니다. 프로그램이 커질수록 “건드리지 않은 모든 주소”를 일일이 열거하는 증명은 빠르게 길어집니다. 논문은 이 확장성 문제에서 출발합니다.

원문의 상태는 저장소(store)와 힙(heap) 두 부분입니다. 저장소 s는 x·y 같은 프로그램 변수를 값에 대응시키고, 힙 h는 실제 주소를 그 주소에 든 값에 대응시킵니다.

예에서 s(x)=100, s(y)=200이고 h(100)=10, h(200)=20입니다. [x] := 11은 저장소에서 x의 값을 바꾸는 명령이 아니라, x가 가리키는 힙 주소 100의 내용을 11로 바꿉니다.

논문의 points-to 주장 x↦10은 현재 힙이 정확히 한 칸으로 이루어지고, 그 주소가 s(x)이며 내용이 10이라는 뜻입니다. 큰 힙 어딘가에 그 칸이 있다는 느슨한 표기가 아닙니다.

emp는 힙이 비어 있다는 주장입니다. 이 엄격한 의미 덕분에 작은 힙 조각의 모양을 정확히 말하고, 뒤에서 분리곱으로 조각들을 합칠 수 있습니다.

분리곱으로 100↦10 ∗ 200↦20이라고 쓰려면 전체 힙을 서로 겹치지 않는 두 부분으로 나눌 수 있어야 합니다. 주소 100과 200은 다르므로 왼쪽 한 칸과 오른쪽 한 칸이 각각의 주장을 만족합니다.

두 변수가 모두 주소 100을 가리키면 같은 칸을 두 조각에 동시에 넣어야 합니다. 겹치지 않는 분할이 없으므로 x↦10 ∗ y↦10은 거짓입니다. 아래 활동은 이 의미 정의만 계산하는 교육용 비교입니다.

P ∗ Q는 어떤 힙 h₀와 h₁이 존재해 주소 영역이 겹치지 않고, 두 힙을 합치면 전체 힙이 되며, h₀에서 P가 참이고 h₁에서 Q가 참이라고 주장합니다.

따라서 ∗는 단순한 “그리고”가 아닙니다. 존재하는 분할과 서로소성, 각 조각의 만족, 전체 힙의 복원까지 네 조건을 함께 묶습니다. 어느 분할이든 이 네 조건을 만족하면 됩니다.

원문은 {x↦−} [x] := 4 {x↦4}에 y↦3을 보통의 ∧로 덧붙인 상수 규칙이 안전하지 않다고 보입니다. x와 y가 같은 주소일 수 있기 때문입니다.

x=y라면 명령이 y가 가리키는 바로 그 칸을 4로 바꿉니다. “y 값은 3으로 남는다”는 결론이 깨집니다. ∧는 두 주장이 같은 힙에서 참이라고 말할 뿐, 서로 다른 힙 조각을 맡긴다는 조건을 주지 않습니다.

지역 명세 {P} C {Q}가 증명되어 있고, R에 자유롭게 나타나는 변수를 C가 대입으로 바꾸지 않는다고 합시다. 프레임 규칙은 {P ∗ R} C {Q ∗ R}을 이끌어 냅니다.

우리 예에서는 P가 x↦10, Q가 x↦11, R이 y↦20입니다. ∗가 x와 y의 힙 조각을 분리하므로 C=[x]:=11은 P 조각만 접근합니다. R의 프로그램 변수 y도 명령에서 대입되지 않아 200↦20이 보존됩니다.

지역 갱신 규칙은 {x↦−} [x] := 11 {x↦11}입니다. 여기에 R=(y↦20)을 프레임으로 붙이면 {(x↦−) ∗ (y↦20)} [x] := 11 {(x↦11) ∗ (y↦20)}이 됩니다.

시작 힙이 {100↦10, 200↦20}이면 P 조각 {100↦10}에서 갱신이 실행되고 {100↦11}이 됩니다. R 조각 {200↦20}은 실행 전후 동일합니다. 전제가 힙 분할을 보장하므로 “우연히 안 건드렸다”가 아니라 규칙으로 보존을 얻습니다.

원문은 list α(i,k)를 i에서 k까지 이어진 목록 구간이 수열 α를 나타낸다는 뜻으로 정의합니다. 빈 수열이면 emp와 i=k가 필요합니다. α가 a·β이면 어떤 다음 주소 j가 존재해 i의 레코드가 값 a와 j를 담고, 그 조각과 list β(j,k)가 분리되어야 합니다.

예를 들어 주소 100에 (A,120), 120에 (B,140), 140에 (C,nil)이 있으면 list [A,B,C](100,nil)입니다. 각 레코드 조각을 ∗로 묶으므로 100·120·140은 서로 다른 시작 주소가 됩니다.

처음에는 i=100이 [A,B,C]의 시작이고 j=nil입니다. 첫 명령 k := [i+1]은 100번 레코드의 다음 주소 120을 읽습니다. 이어 [i+1] := j가 그 다음 칸을 nil로 바꿉니다.

마지막으로 j := i, i := k를 실행하면 i=120은 남은 [B,C]를, j=100은 뒤집힌 [A]를 가리킵니다. 아래 버튼은 원문의 명령 순서를 같은 주소 예로 펼친 교육용 단계 보기입니다.

초기 수열을 α₀=[A,B,C]라고 합시다. 반복 중 남은 목록의 수열을 α, 이미 뒤집힌 목록의 수열을 β라 두면 두 목록 조각이 분리되어 있고 reverse(α₀)=reverse(α)·β라는 관계를 유지합니다.

첫 단계 뒤에는 α=[B,C], β=[A]입니다. reverse([B,C])·[A]=[C,B,A]이므로 reverse([A,B,C])와 같습니다. 분리곱은 두 목록이 겹치지 않음을, 수열 등식은 값의 순서를 잃지 않았음을 각각 맡습니다.

tree τ(i)는 루트 레코드와 두 하위 트리 조각을 ∗로 묶어 내부 공유를 금지합니다. dag τ(i)는 같은 추상값을 나타내면서도 하위 구조를 여러 경로에서 공유할 수 있도록 더 일반적인 주장을 사용합니다.

따라서 ∗가 언제나 모든 공유를 금지한다는 요약은 정확하지 않습니다. 한 분리곱으로 직접 나눈 조각끼리의 겹침을 금지하며, DAG를 표현할 때는 공유 관계를 허용하는 별도 술어와 불변식이 필요합니다.

무제한 주소 산술을 허용하면 서로 다른 레코드가 일부 칸을 비스듬히 겹치는 문제가 생길 수 있습니다. 서로 다른 레코드가 겹치지 않고 주소가 레코드의 첫 필드를 가리킨다는 조건을 따로 표현하기 어려워집니다.

가비지 수집도 일반적으로 자동 보존되지 않습니다. 힙에 고립된 두 칸이 있다는 주장은 수집기가 그 칸을 회수하면 거짓이 될 수 있습니다. 어떤 관찰을 보존해야 하는지에 맞춘 별도 논리가 필요하다고 논문은 설명합니다.

논문은 Schorr–Waite 알고리즘의 증명을 중요한 성과로 소개하면서도, 당시 논리가 이론적으로도 실용적으로도 불완전하다고 분명히 적습니다. 실제 증명에서 의미론적으로 타당하지만 알려진 규칙만으로 잘 나오지 않는 주장들이 남았습니다.

공유 구조를 같은 모양으로 복사하는 프로그램, 여러 레코드 형식, 코드 포인터, 형 체계와의 관계도 미래 과제로 제시됩니다. 2002년 논문의 성과는 국소 추론의 강력한 틀과 실제 적용을 보여 준 데 있으며 이후 발전 전체를 이미 완성했다는 뜻은 아닙니다.

주소 100의 지역 명세를 먼저 증명하고, 주소 200이 맡은 힙 조각을 분리곱으로 프레임에 넣으면 됩니다. 프레임 규칙은 100번 칸의 갱신 뒤에도 200↦20이 유지된다는 전체 명세를 만듭니다.

이 결론은 두 조각이 실제로 분리되고 프레임의 자유 변수를 명령이 대입으로 바꾸지 않는다는 전제에서 성립합니다. 아래 활동은 주장 범위를 구분하는 학습용 점검이며 실제 프로그램 검증기를 실행하지 않습니다.