불변식 작성하기

불변식

지난 장에서 우리는 시퀀스(sequence)에서 중복을 찾는 간단한 명세(specification)를 작성했다. 그런데 이게 제대로 동작하는지 어떻게 알 수 있을까? 여기 중복을 찾는 또 다른 스펙이 있는데, 이것 역시 에러 없이 실행된다:

(*--algorithm find_duplicates
variables
  seq \in S \X S \X S \X S;
  is_unique = TRUE;
begin
  is_unique := FALSE;
end algorithm; *)

이건 그냥 모든 시퀀스 하나하나에 중복이 있다고 말할 뿐이다! 그러니 프로그래밍에서처럼, 이것이 올바른지 검증하는 일종의 자동화된 테스트를 작성하고 싶다.

TLA+에서 우리가 가진 기본적인 테스트는 불변식(invariant)이다. 불변식은 초기값이 무엇이든, 우리가 어디에 있든 상관없이 프로그램의 모든 스텝(step)에서 반드시 참이어야 하는 무언가다.

프로그래밍에서 우리가 가장 흔히 쓰는 불변식은 바로 정적 타입이다! 내가 boolean 타입의 변수를 갖고 있다면, 프로그램의 모든 지점에서 그 변수의 값은 항상 true 아니면 false이고, 절대 문자열이나 17이 아니라고 말하는 셈이다. 이것을 TLA+ 연산자(operator)로 쓸 수 있다:

TypeInvariant ==
  /\ is_unique \in BOOLEAN

이 연산자는 is_unique 변수를 알아야 하므로, PlusCal에서 그 정의 뒤에 둬야 한다. 변수 정의와 알고리즘 본체 사이에 넣을 수 있는 특별한 블록, define 블록이 있다. define 블록에는 순수한 TLA+ 연산자가 들어가고, 이 연산자들은 PlusCal 변수의 값을 참조할 수 있다.

 S == 1..10
 
 (*--algorithm dup
-  variable seq \in S \X S \X S \X S;
+variable 
+  seq \in S \X S \X S \X S;
   index = 1;
   seen = {};
   is_unique = TRUE;
+
+define
+  TypeInvariant ==
+    /\ is_unique \in BOOLEAN
+    /\ seen \subseteq S
+    /\ index \in 1..Len(seq)+1
+    
+end define; 
 
 begin
   Iterate:

이것을 검사하려면 불변식으로 추가한다. TLC는 가능한 모든 상태(state)에서 이것을 검사한다. 불변식이 전부 통과하는 모습은 불변식이 아예 없을 때와 똑같아 보인다 — TLC는 불변식이 실패할 때만 뭔가 흥미로운 일을 한다. 대신 불변식을 is_unique = TRUE로 바꾸면 이렇게 된다:

이 화면은 초기 상태(initial state)에서 시작하는 일련의 스텝을 보여준다. 위쪽 상자는 어떤 불변식이 위반됐는지 보여주고(불변식이 여러 개일 때 유용하다), 아래쪽 상자는 불변식 위반으로 이어진 스텝의 시퀀스다. 처음 두 상태를 더 자세히 살펴보자:

1. 이 상자는 그 스텝에서 일어난 액션(action)을 보여준다. 첫 번째 스텝에서는 아무 액션도 일어나지 않았으므로, 대신 <Initial Predicate>라고 표시된다.

2. 이것은 액션이 일어난 뒤 각 변수의 값이다. <Initial Predicate>의 경우 이 값들은 에러 트레이스(error trace)의 시작 값이다. seq가 이제 고정된 값, 즉 가질 수 있다고 우리가 말한 집합(set) 속 값 중 하나가 되었다는 점에 주목하자.

3. pc는 우리가 어느 레이블(label)에 있는지 추적하려고 변환기가 만드는 추가 변수다. 이에 대해서는 조금 뒤에 이야기하겠다.

4. Iterate 액션이 일어난다. 이 액션은 index와 seen의 값을 바꾼다. 스텝에서 바뀐 값은 빨간색으로 표시된다.

5. 불변식이 실패하면, 마지막 스텝이 바로 불변식이 실패한 스텝이다. 여기서는 두 번째 원소를 검사한 뒤 is_unique가 false가 되어 불변식을 깨뜨리는 것을 볼 수 있다.

(에러 트레이스로 할 수 있는 일이 조금 더 있다. 여기를 보라.)

그럼 다시 불변식의 본질로 돌아가자. 우리는 is_unique가 모든 불리언(boolean)의 집합의 원소라고 적음으로써 그것이 불리언 타입이라고 말한다. TLA+에서 “타입”은 그저 값들의 임의의 집합일 뿐이다. i가 정수라고 말할 수도 있지만, 그보다 훨씬 더 정확하게 말할 수 있다. 우리는 그것이 seq의 인덱스 또는 시퀀스 길이보다 하나 큰 값을 나타낸다는 것을 안다. 그 “타입”은 집합 1..Len(seq)+1이다. 마찬가지로, seen에는 S에 없는 값이 들어 있을 수 없다는 것도 안다. 타입 불변식(type invariant)을 확장하면 이렇다:

TypeInvariant ==
  /\ is_unique \in BOOLEAN
  /\ seen \subseteq S
  /\ index \in 1..Len(seq)+1

불변식 소개는 이 정도면 충분할 것 같다. 이제 우리 알고리즘이 올바르다는 것을 증명하는 불변식을 작성해 보자.

IsCorrect == IF is_unique THEN IsUnique(seq) ELSE ~IsUnique(seq)

IsCorrect == is_unique = IsUnique(seq)

IsUnique(s) == Cardinality(seen) = Len(s)

IsCorrect == IF pc = "Done" THEN is_unique = IsUnique(seq) ELSE TRUE

IsCorrect == pc = "Done" => is_unique = IsUnique(seq)

/\ A
/\ B
 => C

한정자

현재 버전의 IsUnique는 이렇다.

IsUnique(s) == Cardinality(seen) = Len(s)

앞에서 이것이 엉터리 방식이라고 했다. 이유는 세 가지다. 첫째, 이것은 고유성의 정의를 변수인 seen에 묶어 둔다. 시퀀스가 고유한지 아닌지는 우리의 실제 행동(behavior)과 무관해야 한다. 고유하거나, 고유하지 않거나 둘 중 하나다. IsUnique 연산자는 s의 값에만 의존해야 하고, 그 밖의 어떤 것에도 의존해서는 안 된다.

둘째, 이것은 사실 고유성의 정의가 아니다. 그저 집합의 기수를 이용한 영리한 요령을 쓰고 있을 뿐이다. 우연히 고유성과 똑같아지는 이상한 우회로를 쓰기보다는, 연산자가 고유성의 의미 자체를 담아내는 편이 낫다.

마지막으로, 이 방식으로는 더 나아갈 곳이 없다. 고유성은 이렇게 표현할 수 있겠지만, 이를테면 정렬 여부는 어떻게 할 것인가?

이 모든 이유로, 이제 한정자(quantifier)를 소개할 때다. 한정자는 집합의 원소에 대한 명제다. 한정자는 두 가지다: \A, 즉 “forall”은 어떤 명제가 집합의 모든 원소에 대해 참인지 검사한다. \E, 즉 “exists”는 그것이 적어도 하나의 원소에 대해 참인지 검사한다. 내가 다음과 같이 쓴다면

\A x \in {1, 2, 3}: x < 2

이는 “집합의 모든 원소가 2보다 작다”와 동등하며, 이것은 거짓이다. 만약 \E x \in {1, 2, 3}: x < 3이라고 썼다면, 이번엔 참이 된다.

같은 한정자에서 여러 원소를 뽑을 수 있다. 예: 합성수는 1과 자기 자신 외의 수로 나누어떨어진다. IsComposite는 이렇게 쓸 수 있다

IsComposite(num) ==
  \E m, n \in 2..num:
    m * n = num

m과 n이 같은 수일 수 있다는 점에 주목하자: IsComposite(9) = TRUE가 되는 것은 m = n = 3을 골랐을 때다.

시퀀스는 집합이 아니므로 시퀀스에는 한정자를 쓸 수 없다. 하지만 시퀀스의 인덱스에는 쓸 수 있다.

Contains(seq, elem) ==
  \E i \in 1..Len(seq):
    seq[i] = elem

그렇다면 IsUnique를 이렇게 쓸 수 있겠다

IsUnique(s) ==
\* Warning, this is wrong!
\* We'll see why in the next part.
  \A i, j \in 1..Len(s):
    s[i] # s[j]

 ---- MODULE duplicates ----
-EXTENDS Integers, Sequences, TLC, FiniteSets
+EXTENDS Integers, Sequences, TLC
 
 S == 1..10
 
@@ -16,7 +16,9 @@
     /\ seen \subseteq S
     /\ index \in 1..Len(seq)+1
     
-  IsUnique(s) == Cardinality(seen) = Len(s)
+  IsUnique(s) == 
+    \A i, j \in 1..Len(s): 
+      s[i] # s[j]
 
   IsCorrect == pc = "Done" => is_unique = IsUnique(seq)
 end define; 

Test == LET
  seq == <<1, 2, 3, 4>>
  s == 1..4
IN
  CHOOSE p \in s \X s: seq[p[1]] = seq[p[2]]

>>> Test
<<1, 1>>

IsUnique(s) ==
  \A i, j \in 1..Len(s):
    i # j => s[i] # s[j]

     
   IsUnique(s) == 
     \A i, j \in 1..Len(s): 
-      s[i] # s[j]
+      i # j => s[i] # s[j]
 
   IsCorrect == pc = "Done" => is_unique = IsUnique(seq)
 end define; 

HasDuplicates(seq) ==
  \E i, j \in 1..Len(seq):
    i # j => seq[i] = seq[j]

HasDuplicates(seq) ==
  \E i, j \in 1..Len(seq):
    i # j /\ seq[i] = seq[j]

요약

• 불변식은 명세의 모든 상태에서 반드시 참이어야 하는 무언가다.

  • 흔한 불변식으로 타입 불변식이 있는데, 모든 변수의 값이 엄격하게 정한 집합에 속하는지 검사한다.

• 스펙이 불변식을 위반하면, TLC는 위반을 재현하는 방법을 보여주는 스텝별 에러 트레이스를 만들어 낸다.

• 한정자는 집합에 대해 술어(predicate)를 검사한다. \A는 어떤 것이 모든 원소에 대해 참인지 검사하고, \E는 적어도 하나의 원소에 대해 참인지 검사한다.

• 함의(implication)를 써서 불변식에 “끝에 도달했을 때만 이것을 검사하라” 같은 “전제 조건”을 붙일 수 있다.