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

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

内容

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

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

感想

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

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

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

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

メモ

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

TLA+の参考

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

この記事を書いた人

yoshikiito

都内でテストエンジニア&ブロガーをやっている@yoshikiitoです。

ソフトウェアエンジニアの学習方法や成長するための考え方、会社に依存せず自分の力で生きていけるエンジニアになる方法などについて興味があります。
こういった方法や考え方、自分が試したことなどをブログを通じて発信します。

仕事は主にソフトウェアテストやテスト自動化。
趣味は浦和レッズと読書と技術書を買って積むこと。

技術評論社から本を出すのが夢

この記事が気に入ったら
いいね!しよう

最新の情報をお届けします