https://yujiorama.hatenablog.com/entry/2022/04/23/160737

英語のドキュメントを読んだけどあまり理解できてなかったので日本語で再挑戦する会。

進捗

前回
- 「6章時相論理」を読んだり試したり
- 「7章アルゴリズム」を読んでいちゃもん書いたり
今回 2022.4 実践TLA+もくもく会 - connpass
- 「7章アルゴリズム」を読んだり試したり
- 「8章データ構造」を読み始めた
次回 2022.5 実践TLA+もくもく会 - connpass
- 「8章データ構造」を読む（何周かしないと意味が分からなそう）

7.4 アルゴリズムの特性

二分探索を例に、性能や境界条件を検査する。

補助関数
- OrderedSeqOf(set, n)
  - set を値域とする要素数 n のシーケンスのうち、すべて昇順になっているシーケンスを生成する
- Range(f) == { f[x] : x \in DOMAIN f }
  - DOMAIN f は f の取り得るすべての入力
    - f がシーケンスならすべての添え字になる
  - つまり f のすべての値を返すようになっている
  - 途中でいきなり PT!Range(f) に置き換えられている…
入力
- found_index
  - 初期値の 0 は要素が見つからないとき
出力?
- if target \in Range(seq) がわからない
- なんで if target \in seq じゃないんだろう
- → \in に渡せるのは集合だけど、seq はシーケンスだから
  - 型変換しているだけだったというオチだった
時間計算量の検証
- 二分探索の時間計算量は O(log(n)) になるはず
- 逆にループ回数を計測して 2^n < length(n) で判断することもできる
  - 実際には 2^{n-1} で判断する
二分探索アルゴリズムの有名なバグ
- (low + hight) \div 2 は MaxInt + 1 になってしまう場合がある
- Google AI Blog: Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken
- 値域が有限の変数があるときは、不変条件にオーバーフローのチェックを入れた方がよい

---------------------------- MODULE binarysearch ----------------------------
EXTENDS TLC, Integers, Sequences

PT == INSTANCE PT

\* set を値域とする要素数 n のシーケンスのうち、すべて昇順になっているシーケンスを生成する
OrderedSeqOf(set, n) ==
    { seq \in PT!SeqOf(set, n):
        \A x \in 2..Len(seq):
            seq[x] >= seq[x-1] }

MaxInt == 7

(*--algorithm binarysearch
variables
    seq \in OrderedSeqOf(1..MaxInt, MaxInt),
    low = 1,
    high = Len(seq),
    target \in 1..MaxInt,
    found_index = 0,
    counter = 0,
    m = 0,
    lh = 0;

define
    Pow2(n) ==
        LET f[x \in 0..n] ==
            IF x = 0
            THEN 1
            ELSE 2 * f[x-1]
        IN f[n]

    NoOverflows ==
        \A x \in {m, lh, low, high}:
            x <= MaxInt
end define;

begin
    Search:
        while low <= high do
            counter := counter + 1;
            lh := high - low;
            m := high - (lh \div 2);
            if seq[m] = target then
                found_index := m;
                goto Result;
            elsif seq[m] < target /\ m < high then
                low := m + 1;
            else
                high := m - 1;
            end if;
        end while;
    Result:
        \* 計算量を評価
        if Len(seq) > 0 then
            assert Pow2(counter - 1) <= Len(seq);
        end if;
        \* 結果を評価
        if target \in PT!Range(seq) then
            assert seq[found_index] = target;
        else
            assert found_index = 0;
        end if;
end algorithm; *)

7.5 マルチプロセスアルゴリズム

すべてのプロセスが終了する前にアサーションを検査する
- ハードコードするのではなく、活性要件（不変条件と違う？）として記述する
- <>[] でアルゴリズムが確実に終了することを検査する
ステップを Get と Increment に分けると検査が失敗する
- 複数のプロセスが同時に Increment へ進入すると、いずれかのプロセスによる counter の更新が上書きされてしまう
- Get と Increment を統合するか、クリティカルセクションを設けるしかない

counter: 0
goal: 3
pc: <<"Get", "Get", "Get">>
----
counter: 0
goal: 3
pc: <<"Increment", "Get", "Get">>
----
counter: 1
goal: 3
pc: <<"Done", "Get", "Get">>
----
counter: 1
goal: 3
pc: <<"Done", "Get", "Increment">>
----
counter: 2
goal: 3
pc: <<"Done", "Done", "Increment">>
----
----
counter: 2
goal: 3
pc: <<"Done", "Done", "Done">>
----

8.1 リンクリスト

ユースケース
- 循環を持つリンクリストをアルゴリズムが生成しないようにする。
  - 検証したいのはアルゴリズムで、リンクリストを部品として使用するっぽい
- 循環を見つけ出すアルゴリズムを記述する。
  - リンクリスト自体を検証したいっぽい
- 循環を持つリンクリストが与えられてもシステムが正しく動作するようにする。
  - 検証したいのはシステムで、リンクリストを部品として使用するっぽい
データ構造は関数、構造体として表すのが一般的
- データ構造の名前と同じ演算子を定義する慣例になっている LinkedLists(Nodes)
Nodes はメモリアドレスの集合である なんでいきなりメモリの話してるの？
リンクリストは関数集合 [ Nodes -> Nodes ] の集合になる 構造体の表記を関数と呼んでいる？

TLA+に再挑戦（2022.4）

進捗

7.4 アルゴリズムの特性

7.5 マルチプロセスアルゴリズム

8.1 リンクリスト

参考リンク