최근 Alloy로 작업을 많이 하면서 흔한 명세 작성의 함정 하나에 대해 생각하게 됐다. 본문에 있는 내용은 모든 형식 명세에 해당하고, 드롭다운 안에 있는 내용은 숙련된 Alloy 사용자를 위한 것이다.

간단한 의존성 트리 모델을 생각해 보자. 프로그램에는 최상위 의존성 집합이 있고, 그 의존성들은 또 각각 자신의 의존성을 가지는 식이다. Alloy에서는 이렇게 모델링할 수 있다:

sig Package {
  , depends_on: set Package
}

run {some depends_on}

abstract sig Package {
  , depends_on: set Package
}

lone sig A, B extends Package {}

run {some depends_on}

생성된 예시들을 살펴보면 뭔가 이상한 점을 발견할 수 있다. 패키지가 자기 자신에게 의존할 수 있다는 것이다!

명세를 작성하다 보면 이런 말도 안 되는 상황이 자주 생긴다. 시스템이 어떠해야 한다는 의도는 있지만 그걸 명시적으로 인코딩하지 않기 때문이다. 이럴 때는 이를 방지하기 위해 추가적인 제약을 넣어야 한다. 그래서 Alloy에는 특별한 “fact” 키워드가 있다:¹

fact no_self_deps {
    all p: Package {
       p not in p.depends_on 
    }
}

fact {
    no depends_on & iden
}

Alloy는 fact를 위반하는 모델은 전혀 생성하지 않으며, 그런 모델에서 불변식 위반을 찾지도 않는다. fact는 “현실의 사실”이며 전혀 탐색할 필요가 없는 것이다.

fact의 함정

“자기 의존 금지”는 fact의 좋은 예시처럼 보인다. 동시에 끔찍한 fact의 예시이기도 하다. 초보자들은 종종 fact를 이용해 시스템을 모델링하려다 금방 문제에 부딪히곤 한다.

잠깐 명세가 아니라 실제 시스템을 생각해 보자. 패키지 매니저의 의존성은 어디서 오는가? 보통 package.json이나 Cargo.toml 같은 텍스트 파일이다. 만약 누군가 그 파일에 수동으로 자기 자신에 대한 의존성을 넣는다면 어떻게 될까? 아마 패키지 매니저가 그 자기 의존성을 감지해 오류로 입력을 거부하길 바랄 것이다. 그 오류 처리가 제대로 동작한다는 걸 어떻게 알 수 있을까? 체커가 유효한 매니페스트는 받아들이고 자기 순환(self-loop)이 있는 매니페스트는 거부한다는 것을 검증하게 하면 된다.

하지만 우리는 체커에게 자기 의존성을 전혀 생성하지 말라고 했기 때문에, 그 거부를 테스트할 수 없다. 우리의 fact가 자기 의존성을 표현조차 불가능하게 만들어 버렸기 때문이다.

보통 프로그래밍 언어에서는 “불법적인 상태를 표현 불가능하게 만들기”(MISU)가 좋은 것으로 여겨진다(1 2 3 4). 하지만 명세는 당신이 작성하는 소프트웨어뿐 아니라 그 소프트웨어가 동작하는 환경, 즉 기계와 세계까지 모두 다룬다. 불법적인 상태를 표현할 수 없으면, 소프트웨어가 처리해야 할 불법적인 상태를 세계가 만들어내는 상황 자체를 표현할 수 없게 된다.

fact 대신 술어를 써야 한다. 그러면 술어가 참인 경우를 테스트하거나, 다른 속성을 얻기 위해 그 술어가 필요한지 검사할 수 있다. 제약을 암시적이 아니라 명시적으로 만드는 것이다.

// instead of

fact no_self_deps {/*body*/}

run {some_case}
check {some_property}

// do

pred no_cycles {/*body*/}

run {
  no_cycles and some_case
}

check {no_cycles implies some_property}

술어는 “지역적으로 스코프가 지정된다”는 추가적인 장점도 있다. fact가 세 개 있는데 그중 두 개만 적용한 모델을 검사하고 싶다면, 세 번째 fact를 주석 처리해야 한다.

언제 fact를 사용해야 할까

그렇다면 fact는 어디에 써야 할까? 모델을 약화시킬 수도 있는데도 제약을 보편적으로 강제하는 게 언제 의미가 있을까?

첫째, fact는 문제의 범위를 좁히는 데 유용하다. 패키지 인스톨러만 명세하고 매니페스트 검증은 다른 무언가가 담당한다면, “자기 의존 금지”는 완벽하게 합리적인 fact다. 이를 fact로 작성하면 우리가 매니페스트를 검증할 필요가 없다는 점이 독자에게 명확해진다. 즉, 그 가정이 거짓일 경우에는 아무런 보장도 하지 않는다는 뜻이다.

둘째, fact는 근본적으로 흥미롭지 않은 경우를 배제한다. 연결 리스트를 모델링한다고 해 보자:

sig Node {
  next: lone Node //lone: 0 or 1
}

이 모델은 일반적인 리스트와 사이클이 있는 리스트를 모두 생성하는데, 둘 다 나에게는 흥미로운 경우다. 어느 쪽도 제약으로 없애고 싶지 않다. 하지만 두 개의 서로 분리된 리스트를 가진 모델도 생성한다. 단일 연결 리스트에만 관심이 있다면 fact로 불필요한 리스트를 제거할 수 있다:

fact one_list {
    some root: Node | root.*next = Node
}

open util/graph[Node]

fact {
    weaklyConnected[next]
}

비슷하게, fact를 이용해 불필요한 세부사항을 없앨 수도 있다. 사용자와 그룹을 모델링한다면 빈 그룹은 원하지 않을 것이다. Users.groups = Group 같은 fact를 추가하면 된다.

셋째, 느린 모델을 최적화하기 위해 제약을 사용할 수 있다. 보통 대칭성 제거(symmetry breaking)를 통해서다.

마지막으로, Alloy에서 네이티브로 표현할 수 없는 필요한 관계를 정의하기 위해 fact를 사용할 수 있다. 내가 작업했던 프로젝트에서는 그래프에 Red와 Blue 노드가 있었다. Red 노드는 다른 노드로 가는 간선이 적어도 하나 있었고, Blue 노드는 최대 하나였다. 처음에는 이렇게 작성했다:

abstract sig Node {
}

sig Red extends Node {
  edge: some Node
}

sig Blue extends Node {
  edge: lone Node
}

하지만 이렇게 하니 edge를 사용하는 노드에 대한 일반적인 술어를 작성할 수 없었다. Alloy가 이를 타입 오류로 취급했기 때문이다. 대신 fact를 이용해 이렇게 작성했다:

abstract sig Node {
  edge: set Node
}

sig Blue, Red extends Node {}

fact {
  all r: Red  | some r.edge
  all r: Blue | lone r.edge
}

module main

// spec

check {spec => always (prop1)}
check {spec => always (prop2)}

// etc

open main

fact {spec}

check {always (prop1)}
check {always (prop2)}
// etc

결론

제약은 위험하다. 프로그램이 오류 상태를 피한다는 것을 검사하려면 오류 상태 자체가 필요하기 때문이다.

Alloy에 대해 더 배우고 싶다면, 좋은 책이 여기에 있고 내가 관리하는 레퍼런스 문서도 있다. 나는 지금 새로운 Alloy 워크숍도 준비 중이다. 지난달에 알파 테스트를 진행했고 올여름 말에 베타 테스트를 진행할 예정이다. 업데이트를 받고 싶다면 내 뉴스레터를 구독하라!

Jay Parlar와 Lorin Hochstein에게 피드백에 감사한다. 이 글이 마음에 들었다면 내 뉴스레터에 가입해 달라! 매주 새로운 에세이를 올리고 있다.

나는 기업을 대상으로 형식 기법 교육을 하며, 소프트웨어 개발을 더 빠르고, 더 저렴하고, 더 안전하게 만든다. 더 자세한 내용은 여기에서 확인하라.

1. 다른 명세 언어에서는 보통 런타임 제약(예: TLA+에서처럼)이거나 시스템 명세 자체를 직접 수정하는 방식이다. [return]