논문 대담John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures (2002)Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), 55–74
한 메모리 칸을 바꿀 때, 떨어진 칸이 그대로임을 어떻게 증명할까요?
주소 100의 값을 바꾸면서 주소 200의 값이 그대로임을 어떻게 증명할까요? 레이놀즈의 분리 논리를 따라 힙을 겹치지 않는 조각으로 나누고, 프레임 규칙으로 건드리지 않은 조각을 보존하는 과정을 연결 목록 뒤집기까지 이어 읽습니다.
John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures (2002)
게시 2026-10-16해외 논리학 연구 해설 읽기 →





