TLA+に再挑戦(2022.4)
英語のドキュメント を読んだけどあまり理解できてなかったので 日本語 で再挑戦する会。
進捗
- 前回
- 「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 ] の集合になる
構造体の表記を関数と呼んでいる?
参考リンク
- Practical TLA+ | SpringerLink
- 原著
- 実践TLA+ 電子書籍|翔泳社の本
- 翻訳
- The TLA+ Home Page
- TLA+ の総本山的なWebページ