Chapter 2 Specifying a Simple Clock

2.1 Behaviors

「コンピュータシステムにおいて、状態の変化は非連続のステップで起こると仮定できるので、システムの実行をstatesのシーケンスと表すことができる。ここで、stateとはvalueをvariableにアサインすること。システムをpossible behaviorsの集合として定義する。」

まったく日本語になってないが、まあ、簡単にいえば、起こりえる状態変化を全部集めれば、それがシステムを表したことになるよ、ということだ。そしてそれが、これからTLA+をつかって挑むことだ。

2.2 An Hour Clock

デジタル時計の例がスタート。この時計は1 から 12までの時間を表示するだけだとする。hr が時間を表す変数ね。

[hr=11] -> [hr=12] -> [hr=1] -> [hr=2] -> ...

こんなふうに動いていく。2.1で述べたように、起こり得るすべてのbehaviorを書き出す必要がある。まずは初期値の定義。初期値は1から12まで、HCini と呼んで、以下のように定義する。ここで、== は、defined to equal。等しい、ではないので注意。（==は=の上に△.これはTexとも違うらしい。気まぐれだな。。）

HCini == hr \in {1, ..., 12}

まだ右の部分がTLA+記法になってない。次に、ある値と次の値の関係を表現する、HCnxtを定義しよう。hr'はhrの次の値、という意味とする。

HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1

(# はnot equalに使う記号）
こういう式をActionと呼ぶ。HCnxtを満たすstepをHCnxt stepと呼ぶ。このstepが起こった時、stepが実行された、と言いがちだけど、formulaはformulaであって実行されるわけじゃないので厳密には正しい言い回しではない。

さて、　HCiniとHCnxtの２つじゃなくて、ひとつの式で表したい。それには、[] (□, boxと読む)という記号を使う。[]FはFが常に正しいことをassertする。(assertってどう訳すのがいいのだろうか。）[]HCnxtは、HCnxtがすべてのstepにおいてTrueであることを示す。HCini /\ []HCnxt は、初期値がHCini で、すべてのstepがHCnxtを満たす、となって、この時計のSpecとしては良さそうだ。

もしも、その時計に温度計もついていて、まだ１時なのに温度が変わって表示が変わることがあるかもしれない。e.g. [1時22度] -> [1時23度] -> [2時23度]。って、いきなりな仮定が来たけど、ようするに、時間が変わらない、というstepも表現したい。この、hr'=hr となるstepを、stuttering stepという。よって、stepが HCnxt \/ (hr' = hr) であればよい。前述の[]を使ってSpecを書いてみると、

HCini /\ [](HCnxt \/ (hr' = hr))

面倒なので、HCnxt \/ (hr' = hr)のことを、[HCnxt]_hr と書くことにする。HCnxtだけど、hrは変わらないかもよ、というのをむりやり短くしてみたのだ。_hrは、hrは添字（ちっちゃく右下につく）という意味。

HCini /\ [][HCnxt]_hr

この時計は、ある時間で止まって進まないかもしれない。つまり、時計は進まなくて、stepは進む（ややこしい）。時計は必ず進むという前提をつけることもできて、それはChapter 8で扱う。

とりあえず、時計は以下の式で表された。

HC == HCini /\ [][HCnxt]_hr

2.3 A closer look at the specification

HCはtemopral formulaだ。temporal formulaのいい訳語がわからん。HCを満たすすべてのbehaviorについて、[]HCiniがTrueであるので、つまりそれは、HC implies []HCiniといえる。

HC => []HCini

temopral formula satisfied by every behavior はtheoremと呼ばれる。ので、上の式はTheoremといえる。はいそうですか、という感じだけど、このへん、微妙。数学の素養がないのでちょっときつい。

2.4 The Specification in TLA+

さて、いままでPseudo Codeでやってきたが、これをTLA+で書く日がやってきた。

まず、モジュール名から始める。

---- MODULE HourClock ----

なんと、TLA+では数字の足し算演算子"+"はbuiltinではない。それは、自然数モジュールで定義されている。EXTENDS文でモジュールをimportする。（python用語だけど）

EXTENDS Naturals

変数の定義は

VARIABLE hr

---- MODULE HourClock ----
EXTENDS Naturals
VARIABLE hr
HCini == hr \in (1 .. 12)
HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC == HCini /\ [][HCnxt]_hr
--------------------------
THEOREM HC => []HCini
==========================

---- や ====は、４文字以上ならいくつでもいい。..もoperatorで、Naturalsモジュールに定義されている。

THEOREMの前の区切り線は見た目を整えているだけ。で、問題のTHEOREMだが、これは、上の式によって表現された時計が、このTHEOREMを満たすことをチェックするために存在する。つまり、上の式が正しく定義されていれば、HCならばHCiniが常にTrueであるはずで、もしもそうでないならこのSpecには矛盾があります、と。上がSpecで、下がassert文みたいなもんね。すんげー大雑把な理解だけど、そのくらいじゃないと頭が簡単に爆発しそう。

上のSpecにおいて、時計を表すのがHCなのか、HCnxtなのか、HCiniなのかは、TLA+の知ったことではない。TLA+はあくまで数学上の表現であり、その解釈は利用者側に委ねられる。