모듈

모듈(module)을 마지막에 다루는 이유는, 모듈이 코드를 정리할 때만큼 스펙을 정리할 때 중요하지는 않기 때문이다. 스펙은 대부분 300줄 남짓을 넘지 않으니, 별 어려움 없이 파일 하나에 전부 담아 둘 수 있다.

그렇긴 해도 LinkedLists 같은 추상 라이브러리를 만들고 싶을 때가 있고, 불변식(invariant)을 별도 파일에 두기를 좋아하는 사람들도 있다. 그러니 스펙을 모듈화하는 방법을 알아보자.

모듈

공유하는 TLA+ 파일은 스펙과 같은 폴더에 두어야 한다.

팁

툴박스에는 공유 디렉터리에서 모듈을 읽어 오는 설정 옵션(TLA+ Preferences > TLA+ Library Path Functions)이 있다. 이 디렉터리에 있는 모듈은 어느 것이든 모든 스펙에서 쓸 수 있다.

모듈이 준비됐다면 어떻게 임포트할까? 방법이 두어 가지 있다:

EXTENDS

지금까지 우리가 써 온 방식이다. EXTENDS 줄에 있는 것은 전부 여러분 파일과 같은 네임스페이스(namespace)에 통째로 쏟아진다. Sequences가 Append 연산자(operator)를 정의한다면, EXTEND Sequences는 Append를 여러분의 스펙에 떨궈 넣는다.

다만 연산자가 LOCAL이면 얘기가 다르다. 다음과 같이 쓰면

LOCAL Op == "definition"

모듈을 EXTENDS할 때 Op는 임포트되지 않는다.

확장(extension)에 대해 할 말은 이게 전부다! 이제 훨씬 더 흥미로운 모듈 메커니즘인 인스턴스(instance)에 대해 이야기해 보자.

INSTANCE

이 절은 더 큰 제목을 달 자격이 있다. INSTANCE가 EXTENDS보다 훨씬 흥미롭기 때문이다. 다음과 같이 쓰면

INSTANCE Sequences

앞에서와 똑같이 Sequences가 파일 네임스페이스에 쏟아져 들어간다. 그렇다면 이걸 왜 쓰고 싶을까? INSTANCE와 EXTENDS 사이에는 사소한 차이가 두어 가지 있다:

INSTANCE 줄은 한 스펙에 여러 개 둘 수 있는 반면, EXTENDS는 전부 같은 줄에 있어야 한다.
LOCAL INSTANCE로 인스턴스를 “지역적으로” 임포트할 수 있다. 그러면 임포트한 모듈은 쓸 수 있지만, 임포트된 연산자가 다른 스펙에까지 전이적으로 포함되지는 않는다.

(Sequences.tla에서 이 방식이 쓰이는 것을 볼 수 있다. 이 파일은 Naturals를 지역적으로 임포트한다.)

그리고 중요한 차이도 두어 가지 있다.

네임스페이스

Python이나 C++, 혹은 이름을 한정하지 않는 임포트(unqualified import)를 허용하는 무엇이든 다뤄 본 사람이라면 누구나 알듯이, 모든 것을 파일 네임스페이스에 쏟아붓는 건 정말 피하고 싶은 일이다. 다들 열받는다! 인스턴스의 연산자들에는 다음과 같이 네임스페이스를 씌울 수 있다:

Foo == INSTANCE Sequences

네임스페이스 조회는 !로 한다. 그래서 Append(seq, 1) 대신 Foo!Append(seq, 1)라고 쓴다.

팁

그렇다, LET 한가운데서도 모듈을 임포트할 수 있다.

LET Foo == INSTANCE Sequences
IN Foo!Append(seq, 1)

사실 같은 모듈을 서로 다른 이름으로 여러 번 임포트할 수도 있다:

Foo == INSTANCE Sequences
Bar == INSTANCE Sequences

왜 그러고 싶을까? 글쎄, 표준 라이브러리 함수로는 쓸모가 없겠지만, 임포트한 모듈에 상수(constant)가 좀 있다면… 음, 바로 거기서부터 흥미로워진다.

매개변수화된 모듈

새 모듈을 하나 보자:

---- MODULE Point ----
LOCAL INSTANCE Integers
CONSTANTS X, Y
ASSUME X \in Int /\ Y \in Int

Repr == <<X, Y>>
Add(x, y) == <<X + x, Y + y>>
====

지금까지 본 모듈들과 달리 이 모듈에는 상수가 들어 있다. 이 모듈을 임포트할 때는 WITH로 그 상수들이 무엇인지 정의해 줘야 한다. 이렇게 한다:

Origin == INSTANCE Point WITH X <- 0, Y <- 0

이렇게 하면 사실상 Point의 모든 연산자가 넘겨받은 값을 쓰도록 “다시 쓰인다”. 이제 Origin!Add(x, y) == <<0 + x, 0 + y>>이다.

팁

임포트하는 모듈에 자식 모듈과 같은 이름의 상수가 있으면, 그 상수가 기본으로 임포트된다. 예를 들어 두 모듈 모두 DEBUG 상수를 갖고 있다면, 다음 둘은 동등하다:

M == INSTANCE Module WITH DEBUG <- DEBUG
M == INSTANCE Module

(물론 여전히 WITH에서 직접 값을 지정해 오버라이드(override)할 수 있다.)

부분 매개변수화

이렇게 쓸 수도 있다:

XAxis(X) == INSTANCE Point WITH Y <- 0

이제 XAxis!Add(x, y) 대신 XAxis(v)!Add(x, y)라고 쓰는데, 이것이 X 상수가 런타임에 “무엇이어야 하는지”를 정의한다. 예를 들면 XAxis(2)!Add(x, y) == <<2 + x, 0 + y>>이다.

노트

아직 제대로 된 주제 페이지로 옮기지는 못했지만, 내가 쓴 이 글에서 부분 매개변수화(partial parameterization)가 유용한 여러 기법을 다룬다.

요약

EXTENDS는 앞에 LOCAL이 붙은 연산자는 어느 것도 임포트하지 않는다.
INSTANCE는 EXTEND와 비슷하지만, 네임스페이스를 붙일 수 있다는 점이 다르다. 네임스페이스가 붙은 연산자는 I!operator로 호출한다.
상수가 있는 모듈은 인스턴스화할 때 그 상수들의 값을 넘겨줄 수 있다. 모듈을 부분적으로 인스턴스화한 뒤, 나머지 값은 연산자를 호출할 때 넘길 수도 있다.