JaSST19Tokyo チュートリアル2：「TLA＋で学ぶ仕様の書き方とデバッグの仕方」を受講した

チュートリアル２：「TLA+で学ぶ仕様の書き方とデバッグの仕方」に参加しました。

内容

TLA+という形式言語を実際に触って学びました。AWSの検証でも使われているそうです。

EclipseベースのIDEがあるので事前にインストールし、チュートリアル中に説明→練習問題→解説→・・・というスタイル。

普段テストはやっているものの形式検証はやっていないので、面白かったです。（一応大学時代にモデル検査とかそっちの勉強をしていたので、全く無知からの受講ではありませんでした）

受講前の想像だと、モデルを書いて、仕様を書くと、モデルが仕様を満たすかどうか検査してくれるものだと思っていたものの、若干違う？（←まだ理解しきれていない）

状態遷移の部分やinvariantが仕様に相当？また資料みたり自分で調べたりしてもう少し考えてみます。

チュートリアル自体はというと、ウォシュレットを検証してみようという例がとてもイメージしやすくてよかったです。

今回は初歩的なものを紹介
- 続きは自分で学べるようになっているはず
わかること
- 仕様の書き方
- デバッグの仕方
- 何ができるのか
今回の題材
- マッサージ機能付きウォシュレット
TLA+は Amazon なんかも取り入れている
Tex で出力して PDF にできるので、そのまま仕様書にすることもできる
- なのでコメントは書いておくがよい
Q:述語とは
- 条件のようなもの
- 「ｘを与えると命題となるようなものを、ｘの述語という」
TLA+は型のない言語だけど、仕様書いてる人は型相当のものを想定することが多い
Invariant
Q:宣言した変数に対して、全状態変化のときに「変わらない」と宣言しなければいけない？
- A:はい。実際に仕様書を書くときと一緒で、「変化しない」ことを明示しないといけない。
specifying systems (参考文献に書いてある)にが参考になる

チュートリアル受講後に自分で調べて出てきたので、参考。