はじめに 私はテストを書くのは素人なので、「こいつなんにもわかってない」と思われるかもしれませんが、そういう人はスルーしていただければと思います。また、テスト駆動開発とか、アジャイルとか、いまいちわかっていません。この記事は、あくまでも分散…

結論から言うと、山火事問題はまだまだ荷が重い課題でした。これまでPlusCAL中心で来ていきなりTLA+の複雑な記述に挑むのは結構辛い。なので、一旦TLA+本に戻ります。Chapter 3です。送信機、受信機がval(値受け渡し用）、rdy(SYN用)、ack(ACK用）の３本の電…

前回２フェーズコミットを試した後、他の例として出てくるPaxosと、もう一つの問題（本件）がありました。PaxosはPlusCALで書かれていて記述自体はシンプルなものの、アルゴリズム自体が難しい点、pdf上にざっくりと載っているだけで、動くスペックにするの…

PlusCAL Manualは、実は読み終わったのですが、後半はわりとつまらないのでここには書きません。Hyperbook は時間があれば読み進める予定。iPadで読みにくいのが難点。さて、実践編その１としまして、AWSの人が書いた２フェーズコミットのブログ記事があるの…

Cマニュアル、意外によみやすいのでこのまま続けて読むことにした。3は言語仕様。 3.2.1 Assignment := はわかる。けど、-> と |-> の違いがいまいちわかってない。S->Tは写像（集合と集合のマッピング）と理解できそうだけど、それだけだとしっくりこない使…

Hyperbookの4.9に入ったら、Lamport先生我慢できなくなったのか、「でもやっぱり数学的証明も必要だよね」みたいなかんじで証明モードに入ったため、ややゲッソリして PlusCALのC Manualをつまみ食い。（PlusCALには、Cっぽい文法とPascalっぽい文法の２通り…

4.3 は、ユークリッド法での最大公約数の求め方。以前PlusCALを試してみよう - みょらみょらPython日記で同じことを試したのが、少しは役立っている。基本的にはテキストにそっていけばよいのだが、実行しても「エラーが起きない」だけで肝心の最大公約数は…

せっかく Chapter 1と Chapter 2を終わって動かしてみたものの、なんだかずいぶん進めにくいなー、と思って、ふとHyperbook (前回 TLA+の本、と紹介した横にあったもの。最初HTML形式のオンライン物だと思ってて、避けてた）を読んでみたら、なにこれわかり…

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

1.1 Propositional Logic /\ (and) => (implies、日本語だとなんだっけ？ならば、とか？) \/ (or) (is equivalent to) ~ (not) このへんはまだTLA+関係ないので余裕。 1.2 Sets 集合ね。。大学一年の時、集合と位相の授業で人生初の赤点をとった苦い記憶が蘇…

このブログはアメブロよりもさらに読者が少ないので、ひっそりと一人輪読（というかただの読書）のまとめをかいていくことにする。英語のままだと何回読んでも頭に入ってこない。TLA+の本 http://research.microsoft.com/en-us/um/people/lamport/tla/book.h…

こんな簡単な例でも、読んだだけでは「ふーん、そう」という感じで、いまいちわかってない。問題は、この本をずっと読み進めていっても、いつまでたっても実際の使い方にたどり着かないことだ。（PlusCALのマニュアルはその点、少しだけ親切。それをもとにPl…

ひさびさにこっちのブログ書いたら思い出したよ。そうそう、PlusCAL、やろうやろうと思ってるんだけどねー。MSR閉鎖されて、らんぱーとさんどうしてるのかねー。まだ働いてるみたいだけど。

これ、日本語になってないので、せっかくなので紹介。こういう翻訳系って勝手にやっていいもんなの？わかんないので、概要のみ意訳。 What kind of jobs do the software engineers who earn $500K a year do? http://www.aminariana.com/essays/million-dol…