デブサミ2020【13-F-6】「厳密な共通言語」としての形式手法 #devsumiF #devsumi

チェシャ猫[ProofCafe] https://event.shoeisha.jp/devsumi/20200213/session/2380/ Developers Summit 2020の講演資料・参加レポート一覧: https://codezine.jp/article/detail/11981
デブサミ2020 デブサミ devsumi
0
ikuodanaka @dora_e_m
チェシャ猫さん、声がチェシャ猫感ある #devsumiF pic.twitter.com/05JoUU1uMj
拡大
tsuemura @tsueeemura
テスターはほとんどブロッコリーさんの方に行ってしまったのかw #devsumif
SAKON @sakon310
3階奥だからか、最初は空いてたけど始まったら立見出てます。#devsumiF twitter.com/y_taka_23/stat…
しまむちゃん @shimamchan
TCCパターンだ。 T…Try C…Confirm C…Cancel #devsumi #devsumiF
SAKON @sakon310
テキトーな性分なので厳密性難しい。学ばねば。 #devsumiF event.shoeisha.jp/devsumi/202002…
ΗΙDΕΟ @_hideoyamada
分散コンピューティングの落とし穴 ・ネットワークは信頼できる ・レイテンシはゼロである ・帯域は無限である ・ネットワークはセキュアである ・ネットワークトポロジは不変である ・管理者は一人である ・トランポポートコストはゼロである ・ネットワークは均質である #devsumi #devsumiF
しまむちゃん @shimamchan
TLA+はDynamoDB,S3の検証、CockroachDBの並列コミット検証にも使われた。へー #devsumi #devsumiF
SAKON @sakon310
TLA+は学者のオモチャではない。DynamoDB/S3やCockroachDBでも取り入れられている。 #devsumiF pic.twitter.com/zGjIkEi0Ao
拡大
しまむちゃん @shimamchan
コンポーネントごとに記述する。合成はTLA+がやってくれる #devsumi #devsumiF
rin @rin60555258
これめっちゃ楽しいぞ?? #devsumiF
FJ @FJKei
#devsumiF 形式手法の話。TLA+をおすすめしてくれてる、数学の論理式をプログラムチックに書かせて、ロジックに穴がないことの証明をするらしい。ちょっと面白いぞ。
しまむちゃん @shimamchan
安全性と活性は必ず組みになっている #devsumi #devsumiF
tsuemura @tsueeemura
安全性と活性って初めて聞いたけどいい視点だな、テストとかQAとかやってるとつい安全性ばかり考えてしまう #devsumif
FJ @FJKei
#devsumiF 何もしないシステムは安全。でも役に立たない。役に立つには活性が不可欠。どんなシステムもこの2つを考える必要がある。なるほど。
しまむちゃん @shimamchan
時相論理はステート列に対して真偽を判定する #devsumi #devsumiF
しまむちゃん @shimamchan
このセッションちょ〜〜〜〜おもしろいんだが?????? #devsumi #devsumiF
FJ @FJKei
#devsumiF 時相論理って単語を初めて聞いた。
しまむちゃん @shimamchan
時相論理なら、テストじゃむずかしい「一連の振る舞い」を検査できるようになる。 #devsumi #devsumiF
iotas𓆡創作者向けアプリ運営中𓅬 @tRiaeZ1
故障のときどうするのかずっと気になってた! #devsumif
iotas𓆡創作者向けアプリ運営中𓅬 @tRiaeZ1
厳密な共通言語としての形式手法 性質のいいシステム順(上からマシなシステム) 1.故障したら止まる 2.故障したあともたまに復旧する 3.なんかよくわからない値を返す #devsumif
tsuemura @tsueeemura
TLA+面白かった。要件の組み合わせだったり、異常系だったりを数学的な表現で表して曖昧性を排除するのか。 #devsumif
しまむちゃん @shimamchan
自然言語、表現の柔軟さがあるかわりに曖昧さが多大に含まれるからね #devsumi #devsumiF
ΗΙDΕΟ @_hideoyamada
形式手法のまとめ ・自然言語による仕様は曖昧性を持つ ・形式手法によるモデリング ・より複雑な状況における解析の自動化 #devsumi #devsumiF
残りを読む(7)

コメント

コメントがまだありません。感想を最初に伝えてみませんか?

ログインして広告を非表示にする
ログインして広告を非表示にする