구조화된 데이터

구조체

시퀀스(sequence)는 튜플(tuple)과 배열을 다룬다. 이제 문자열 해시맵을 표현할 무언가가 필요하다. TLA+에서는 구조체(struct)가 그 역할을 한다:

struct == [a |-> 1, b |-> {}]

구조체는 시퀀스와 같은 방식으로 인덱싱하므로 struct["a"] = 1이다. 대신 점을 써서 좀 더 “객체”처럼 쓸 수도 있다: struct.a = 1.

놀랄 것도 없이, 구조체는 주로 정리된 데이터 묶음을 표현하는 데 쓰인다. 예를 들어 BankTransaction은 계좌, 금액, 그리고 입금인지 출금인지로 구성될 수 있다.

시퀀스, 집합(set), 원시 값과 마찬가지로, 구조체의 집합을 생성할 방법도 필요하다. 그래야 타입 불변식(type invariant)에 넣을 수 있다. 방법은 이렇다:

\* Accounts is a set of model values
BankTransactionType == [acct: Accounts, amnt: 1..10, type: {"deposit", "withdraw"}]

이것은 s.acct \in Accounts, s.amnt \in 1..10 등을 만족하는 모든 구조체의 집합이다.

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

RangeStruct(struct) == {struct[key]: key \in DOMAIN struct}

>>> RangeStruct(<<"a", "b", "a">>)

{"a", "b"}

함수

우선, 프로그래밍에서 말하는 “함수”의 정의는 버려라. TLA+에서 프로그래밍의 함수에 가장 가까운 것은 연산자(operator)다. 함수는 수학적 정의, 즉 한 집합의 값을 다른 집합으로 대응시키는 사상(mapping)을 따른다.

F == [x \in S |-> expr]

대응의 출발점이 되는 집합 S는 함수의 정의역(domain)이며, DOMAIN F라고 써서 얻을 수 있다. 그래서 시퀀스와 구조체에도 DOMAIN을 쓸 수 있었던 것이다:

1. 시퀀스는 정의역이 1..n인 함수일 뿐이다.

2. 구조체는 정의역이 문자열의 집합인 함수일 뿐이다.

하지만 함수는 그보다 더 일반적이어서, 어떤 값의 집합이든 대응시킬 수 있다. 예를 들어 함수의 정의역에 숫자 쌍을 둘 수도 있다.

Prod ==
  LET S == 1..10 IN
  [p \in S \X S |-> p[1] * p[2]]

\* Prod[<<3, 5>>] = 15

나는 다양한 입력에 대한 식(expression)의 결과를 보여 주는 용도로 함수를 즐겨 쓴다. P와 Q가 어떤 값일 때 P => Q가 참일까?

TruthTable == [p, q \in BOOLEAN |-> p => q]

이것을 스크래치 파일에서 실행하면 결과가 나오는데, 형식이 좀 특이하다:

>>> TruthTable

( <<FALSE, FALSE>> :> TRUE @@
<<FALSE, TRUE>> :> TRUE @@
<<TRUE, FALSE>> :> FALSE @@
<<TRUE, TRUE>> :> TRUE )

이것은 “펼친 형태(expanded form)”다: x :> y는 x를 y로 대응시키는 단일 값 함수이고(즉 [s \in {x} |-> y]), @@는 두 함수를 병합한다. 두 함수가 키를 공유하면 @@는 왼쪽의 값을 유지한다.

이것으로 시퀀스와 구조체가 그저 함수일 뿐이라는 것을 확인할 수 있다:

>>> 1 :> "a" @@ 2 :> "b"
<<"a", "b">>

>>> "a" :> 1 @@ "b" :> 2
[a |-> 1, b |-> 2]

예제: Zip

Python에는 zip이라는 함수가 있다. 이 함수는 이터러블 두 개를 받아 시퀀스 하나를 반환하는데, 그 원소는 두 입력의 원소를 짝지은 쌍이다. 한쪽이 다른 쪽보다 길면 짧은 쪽의 길이까지만 처리한다.

>>> list(zip([1, 2], ["a", "b", "c"]))
[(1, 'a'), (2, 'b')]

보통 프로그래밍 언어는 zip을 반복이나 재귀로 구현한다. 여기서는 그럴 필요가 없다. 시퀀스 전체를 한 번에 “볼” 수 있기 때문이다.

Zip1(seq1, seq2) ==
  LET Min(a, b) == IF a < b THEN a ELSE b
      N == Min(Len(seq1), Len(seq2))
  IN
    [i \in 1..N |-> <<seq1[i], seq2[i]>>]

다르게 쓰는 방법은 교집합을 이용하는 것이다. 1..a와 1..b의 교집합이 1..Min(a,b)라는 점에 주목하면 된다. 그러면 Zip을 이렇게 단순화할 수 있다:

Zip2(seq1, seq2) ==
  LET N == (DOMAIN seq1) \intersect (DOMAIN seq2)
  IN
    [i \in N |-> <<seq1[i], seq2[i]>>]

한정자(quantifier)를 이용한 검사를 작성해서 두 정의가 동등한지 확인할 수 있다:

LET
  S == 1..4
  Input == (S \X S \X S) \union (S \X S)
IN
  \A s1, s2 \in Input:
    Zip1(s1, s2) = Zip2(s1, s2)

variables
  assignments = [t \in Tasks |-> {}]

OnlyOneTaskPerCpu ==
  \A t1, t2 \in Tasks, c \in CPU:
    /\ (t1 # t2)
    /\ c \in assignments[t1]
    => c \notin assignments[t2]

OnlyOneTaskPerCpu ==
  \A t1, t2 \in Tasks:
    (t1 # t2)
    => assignments[t1] \intersect assignments[t2] = {}

TypeInvariant ==
  \* ...
  /\ assignments \in
    LET LeqTwoCPUs == {set \in SUBSET CPUs: Cardinality(set) <= 2}
    IN [Tasks -> LeqTwoCPUs]

TypeInvariant ==
  /\ assignments \in [Tasks -> SUBSET CPUs]

AnotherInvariant ==
  \A t \in Tasks: Cardinality(assignments[t]) <= 2

IsSorted(seq) ==
  \A i, j \in 1..Len(seq):
    i < j => seq[i] <= seq[j]

Sort(seq) ==
  <<>>

Range(f) == {f[x] : x \in DOMAIN f}

Sort(seq) ==
  CHOOSE sorted \in [DOMAIN seq -> Range(seq)]:
    /\ \* sorted has the same number of each element as seq
    /\ IsSorted(sorted)

CountMatching(f, val) ==
  Cardinality({key \in DOMAIN f: f[key] = val})

Sort(seq) ==
  CHOOSE sorted \in [DOMAIN seq -> Range(seq)]:
    /\ \A i \in DOMAIN seq:
      CountMatching(seq, seq[i]) = CountMatching(sorted, seq[i])
    /\ IsSorted(sorted)

>>> Sort(<<8, 2, 7, 4, 3, 1, 3>>)
<<1, 2, 3, 3, 4, 7, 8>>

다시, 중복 검사기

이번이 마지막이다, 약속한다.

중복 검사기의 지난 버전은 다음과 같았다:

---- MODULE duplicates ----
EXTENDS Integers, Sequences, TLC, FiniteSets
CONSTANT S
ASSUME Cardinality(S) >= 4

(*--algorithm dup
  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
    
  IsUnique(s) == 
    \A i, j \in 1..Len(s): 
      i # j => seq[i] # seq[j] 

  IsCorrect == pc = "Done" => is_unique = IsUnique(seq)
end define; 

begin
  Iterate:
    while index <= Len(seq) do
      if seq[index] \notin seen then
        seen := seen \union {seq[index]};
      else
        is_unique := FALSE;
      end if;
      index := index + 1;
    end while;
end algorithm; *)
====

현재 S의 값은 모델마다 제어할 수 있는데, seq의 길이도 제어할 수 있으면 좋겠다. 그러면 원소 2개짜리 시퀀스와 20개짜리 시퀀스를 모두 테스트할 수 있다. 하지만 지금은 길이가 우리가 쓴 \X 곱의 개수로 하드코딩되어 있다.

함수 집합을 쓰면 이것을 단순화할 수 있다. S \X S \X S는 3-튜플의 집합이 된다. 이제 우리는 3-튜플이 정의역이 1..3인 함수라는 것을 안다. 그러면 [1..3 -> S] = S \X S \X S이다: 각 튜플의 모든 원소가 S의 값인 모든 3-튜플의 집합이다.

여기서부터 다섯 원소짜리 시퀀스로 확장하는 것은 간단하다:

 ASSUME Cardinality(S) >= 4
 
 (*--algorithm dup
-  variable seq \in S \X S \X S \X S;
+variable
+  seq \in [1..5 -> S];
   index = 1;
   seen = {};
   is_unique = TRUE;

S \X S \X S는 길이가 하드코딩되어 있지만 [1..3 -> S]는 값 — 정의역 집합의 크기 — 에 기반한다는 점에 주목하자. 이는 이것을 상수(constant)로 빼낼 수 있다는 뜻이다!

 ---- MODULE duplicates ----
 EXTENDS Integers, Sequences, TLC, FiniteSets
-CONSTANT S
+CONSTANT S, Size
 ASSUME Cardinality(S) >= 4
+ASSUME Size > 0
 
 (*--algorithm dup
 variable
-  seq \in [1..5 -> S];
+  seq \in [1..Size -> S];
   index = 1;
   seen = {};
   is_unique = TRUE;

 
 (*--algorithm dup
 variable
-  seq \in [1..Size -> S];
+  n \in 1..Size;
+  seq \in [1..n -> S];
   index = 1;
   seen = {};
   is_unique = TRUE;

요약

• 함수는 값의 집합을 다른 값의 집합으로 대응시킨다. [x \in set |-> Expr(x)]로 쓰고 f[value]로 호출한다.

  • 함수는 [x, y \in Set1, z \in Set2 |-> P(x, y, z)]처럼 쓰고 f[a, b, c](또는 f[<<a, b, c>>])로 호출할 수도 있다.

• 함수의 정의역, 즉 대응의 출발점이 되는 집합은 DOMAIN f다.

  • a :> b는 함수 [x \in {a} |-> b]다.

  • f @@ g는 f와 g를 병합하며, f의 키를 우선한다.

• 시퀀스는 정의역이 1..n인 특별한 종류의 함수일 뿐이다.

• 구조체는 또 다른 특별한 종류의 함수로, [key1 |-> val1, key2 |-> val2]로 쓴다. struct["key1"](또는 struct.key1)로 호출한다.

• 함수와 구조체는 둘 다 전용 집합 문법이 있다. 구조체는 [key1: set1]이다. 함수는 [A -> B]다.

1

T를 “공역(codomain)”이라고 부르기도 한다.