연산자와 값

IF-THEN-ELSE

식을 구성하는 키워드는 세 가지다. LET 문, case 문, 그리고 조건문이다. 앞의 둘은 나중에 소개한다. LET 문은 기본적인 연산자를 몇 개 쓸 수 있게 된 뒤에야 훨씬 쓸모가 있고, case 문은 그리 자주 쓰이지 않는다. 그러면 조건문이 남는다.

Abs(x) == IF x < 0 THEN -x ELSE x

식은 언제나 무언가와 같아야 하므로, ELSE 분기가 반드시 있어야 한다. 그 점만 빼면 예상대로 동작한다.

뻔한 것들

정수와 문자열이다. 기본적인 덧셈 연산자를 쓰려면 EXTENDS Integers가 필요하다. 문자열은 “큰따옴표”를 써야 하며 작은따옴표는 쓸 수 없다. 문자열용 연산자는 =와 # 말고는 없다. 실제로 문자열은 불투명한 식별자로 쓰이는데, 일부 언어에 있는 :symbol 타입과 비슷하다. 시스템에서 문자열을 조작해야 한다면, 대신 문자열을 시퀀스에 담는다.

부동소수점(float) 타입은 없다는 점에 유의하자. 부동소수점은 의미론이 복잡해서 표현하기가 극도로 어렵다. 보통은 추상화해서 빼 버릴 수 있지만, 부동소수점이 정말로 꼭 필요하다면 TLA+는 그 일에 맞지 않는 도구다.

불리언

불리언(boolean)은 TRUE와 FALSE다.

그런데 왜 불리언에만 따로 절을 할애할까? 우선, 불리언 연산자는 프로그래밍 기호가 아니라 수학 기호처럼 생겼다. 다음과 같다.

간단한 암기법: ~는 뭔가를 뒤집는 작은 꼬부랑이니까 “not”이다. /\는 “A”처럼 생겼으니까 “and”다. \/는 남은 하나다. 이것들로 Xor 같은 다른 연산자를 만들 수 있다.

Xor(A, B) == A = ~B

눈여겨볼 불리언 연산자가 하나 더 있다. =>, 즉 “함의(implication)”다. A => B는 “B는 적어도 A만큼은 참이다”라는 뜻이다. A => B는 A가 참이고 B가 거짓이면 FALSE이고, 그 밖의 경우에는 참이다. 제어 흐름에는 거의 쓸모가 없어서 프로그래밍에서는 자주 볼 일이 없다. 하지만 어떤 종류의 스펙 작업에서든 극도로 중요하다. 이에 대해서는 나중에 더 자세히 다룬다.2

또 하나는 TLA+에 불리언 논리를 위한 “글머리표 표기법”이 있다는 점이다. A /\ (B \/ C) /\ (D \/ (E /\ F)) 같은 식이 필요하다고 해 보자. 정말 읽기 힘들다! 그래서 TLA+에서는 대신 이렇게 쓸 수 있다.

/\ A
/\ \/ B
   \/ C
/\ \/ D
   \/ /\ E
      /\ F

훨씬 명확해진다. A 앞에 /\가 하나 더 붙어 있다는 점에 주목하자. 꼭 필요하지는 않지만 모양이 더 보기 좋아서 그렇게 쓴다. 또한 이곳은 언어 전체에서 공백이 의미를 갖는 유일한 곳이다. 이를테면 내가 대신 이렇게 썼다고 하자.

/\ A
/\ \/ B
   \/ C
/\ \/ D
   \/ /\ E
/\ F

이러면 뜻이 달라진다! 이제는 A /\ (B \/ C) /\ (D \/ E) /\ F가 된다.

집합 연산자

x가 set의 원소인지 확인하려면 x \in set이라고 쓴다. \in은 연산자로만 쓰이는 게 아니라 다른 몇몇 곳에서 문법으로도 쓰인다. 그 역인 \notin도 있다. set1 \subseteq set2는 set1의 모든 원소가 set2의 원소이기도 한지 검사한다.

집합을 이리저리 자르고 쪼개는 방법도 있다.

• set1 \union set2는 set1 또는 set2(또는 둘 다)에 있는 모든 원소의 집합이다.

• set1 \intersect set2는 두 집합 모두에 있는 모든 원소의 집합이다.

• set1 \ set2, 즉 “차집합”은 set1에는 있지만 set2에는 없는 모든 원소의 집합이다.

>>> {1, 3} \union {1, 5}

{1, 3, 5}

>>> {1, 3} \intersect {1, 5}

{1}

>>> {1, 3} \ {1, 5}

{3}

EXTEND FiniteSets를 하면 Cardinality(set)도 쓸 수 있다. 집합에 있는 원소의 개수다.

값의 집합

이제 시계 값을 쓰는 스펙을 작성하는데, 시각을 더하는 연산자를 간단히 하나 만들고 싶다고 상상해 보자. 나라면 이렇게 쓸 것이다.

AddTimes(t1, t2) == <<t1[1] + t2[1], t1[2] + t2[2], t1[3] + t2[3]>>

그러면 AddTimes(<<2, 0, 1>>, <<1, 2, 3>>) = <<3, 2, 4>>이고, AddTimes(<<2, 0, 1>>, <<1, 2, 80>>) = <<3, 2, 81>>이다.

잠깐, 81초? 우리 시계는 81초를 표시할 수 없다. 답은 <<3, 3, 21>>이어야 한다. <<0, 0, 0>>부터 <<23, 59, 59>>까지 유효한 시계 값들의 집합이 있고, AddTimes는 마치 타입 시그니처가 있는 것처럼 언제나 그 집합 안의 어떤 값을 반환해야 한다고 생각할 수 있다. TLA+에서 이것을 강제할 수 있지만, 그 전에 값으로부터 값의 집합을 만들어 내는 방법이 필요하다. 다행히 TLA+의 모든 값 타입에는 그 타입 값들의 집합을 만들어 내는 방법이 있다.1

가장 쉬운 것부터 시작하자. 모든 불리언의 집합을 얻으려면 그냥 BOOLEAN이라고 쓰면 된다. 이것은 {TRUE, FALSE} 집합이다. 정수의 경우, a..b는 {a, a+1, a+2, ... , b} 집합이다. 이것이 동작하려면 EXTENDS Integers가 필요하다.

이제 시퀀스 차례다. 두 집합 S와 T의 데카르트 곱(Cartesian product)은 첫 번째 원소가 S에 있고 두 번째 원소가 T에 있는 모든 시퀀스의 집합이다. \X로 쓴다. 예를 들어 누가 로그인하는지, 로그인을 시도한 시각, 그리고 성공했는지 여부를 담는 LoginAttempt를 생각해 보자. 가능한 모든 그런 값의 집합을 LoginAttempt == Person \X Time \X BOOLEAN으로 나타낼 수 있다.

Time 이야기가 나온 김에, \X와 ..를 조합하면 드디어 시계 타입을 얻을 수 있다.

ClockType == (0..23) \X (0..59) \X (0..59)

간단한 확인 삼아 스크래치 파일 만들기에서 Cardinality(ClockType)를 실행해 보라(EXTENDS FiniteSets가 필요하다는 것을 잊지 말자). 원소가 86400개임을 볼 수 있을 것이다. 이제 AddTimes에 대한 속성(property)에 한 걸음 더 다가갔다. 우리는 그 결과가 언제나 ClockType 안의 값이기를 원한다.

마지막으로, SUBSET S로 한 집합의 모든 부분집합을 얻을 수 있다. SUBSET ClockType은 시계 값을 여러 개 담은 모든 집합이 된다… 무려 2^86400개 전부. 이러지 마라.

\* Map
Squares == {x*x: x \in 1..4}

\* Filter
Evens == {x \in 1..4: x % 2 = 0 }

{t \in ClockType: t[2] >= 30 /\ t[3] = 0}

Range(seq) == {seq[i]: i \in 1..Len(seq)}

CHOOSE

시계 값에서 자정 이후 몇 초가 지났는지 구하는 것은 간단하다. 그렇다면 반대 방향은 어떨까? 초 단위 시간이 있으면 다음과 같이 시계 시각을 구할 수 있다.

1. 3600으로 내림 나눗셈을 해서 총 시간(hour)을 구한다.

2. 그 나머지를 다시 60으로 내림 나눗셈을 해서 총 분을 구한다.

3. 두 번째 나눗셈의 나머지를 초로 삼는다.

이 방법은 총 초에서 시계 값을 구성한다. 무언가를 하는 알고리즘을 구현하는 프로그래밍 언어에서라면 이렇게 할 것이다. 하지만 이 방법은 실수하기도 쉽다. 90,000을 넣으면 어떻게 될까? 그러면 <<25, 0, 0>>이 나온다. ClockType 바깥의 값이다.

이렇게 할 수도 있다.

1. 가능한 모든 시계 값의 집합을 가져온다.

2. 그 집합에서, 초로 변환했을 때 주어진 값이 되는 원소를 고른다.

우리가 이렇게 하지 않는 이유는 “가능한 모든 시계 값의 집합”이 원소가 80,000개가 넘고, 원소 80,000개짜리 리스트에서 검색하는 것은 자원 낭비이기 때문이다. 하지만 이 방법은 변환의 정의에 더 가깝게 들어맞아서 명세(specification)에는 더 유용하다. TLA+에서는 이 선택을 다음과 같이 쓸 수 있다.

ToClock(seconds) == CHOOSE x \in ClockType: ToSeconds(x) = seconds

CHOOSE x \in set: P(x)는 범용 “선택” 문법이다. 스크래치 파일 만들기에서 직접 해 보라.

CHOOSE는 집합에서 값을 하나 꺼내야 할 때면 언제든 유용하다.

그럼 ToClock(86401)이라고 쓰면 어떻게 될까? 86,401초에 해당하는 시계 시각은 없다. 이것을 시도하면 TLC가 에러를 낸다. 이는 엉터리 값을 내놓는 구현 방식의 해법과 대조적이다. 대응하는 집합 원소를 찾지 못한다면, 99%는 스펙의 버그, 즉 미처 고려하지 못한 엣지 케이스다. 연산자를 더 단단하게 만드는 편이 낫다.

ToClock(seconds) == CHOOSE x \in ClockType: ToSeconds(x) = seconds % 86400