デブサミ2020【13-F-6】「厳密な共通言語」としての形式手法 #devsumiF #devsumi
-
- いいね！0
しまむ
@sh1mamchan
次は @y_taka_23 さんのセッション聞くー twitter.com/y_taka_23/stat… #devsumi #devsumiF
2020-02-13 15:09:11
チェシャ猫
@y_taka_23
本日 Developer Summit 2020 の登壇資料です。#devsumi #devsumiF 現実のシステムには、目に見えない仕様や暗黙の仮定が大量に存在します。そんな複雑なものを厳密に扱いたいなら、厳密な「言葉」を使ってみるのはいかがでしょうか？ 「厳密な共通言語」としての形式手法 speakerdeck.com/ytaka23/develo…
2020-02-13 14:47:39
いくお/IkuOODA
@dora_e_m
チェシャ猫さん、声がチェシャ猫感ある #devsumiF pic.twitter.com/05JoUU1uMj
2020-02-13 15:16:21
拡大
SAKON
@sakon310
3階奥だからか、最初は空いてたけど始まったら立見出てます。#devsumiF twitter.com/y_taka_23/stat…
2020-02-13 15:19:11
SAKON
@sakon310
テキトーな性分なので厳密性難しい。学ばねば。 #devsumiF event.shoeisha.jp/devsumi/202002…
2020-02-13 15:26:04
ΗΙＤΕΟ
@_hideoyamada
分散コンピューティングの落とし穴 ・ネットワークは信頼できる ・レイテンシはゼロである ・帯域は無限である ・ネットワークはセキュアである ・ネットワークトポロジは不変である ・管理者は一人である ・トランポポートコストはゼロである ・ネットワークは均質である #devsumi #devsumiF
2020-02-13 15:28:59
しまむ
@sh1mamchan
The TLA+ Home Page lamport.azurewebsites.net/tla/tla.html #devsumi #devsumiF
2020-02-13 15:32:19
しまむ
@sh1mamchan
TLA+はDynamoDB,S3の検証、CockroachDBの並列コミット検証にも使われた。へー #devsumi #devsumiF
2020-02-13 15:33:33
SAKON
@sakon310
TLA+は学者のオモチャではない。DynamoDB/S3やCockroachDBでも取り入れられている。 #devsumiF pic.twitter.com/zGjIkEi0Ao
2020-02-13 15:34:31
拡大
FJ
@FJKei
#devsumiF 形式手法の話。TLA+をおすすめしてくれてる、数学の論理式をプログラムチックに書かせて、ロジックに穴がないことの証明をするらしい。ちょっと面白いぞ。
2020-02-13 15:43:39
tsuemura
@tsueeemura
安全性と活性って初めて聞いたけどいい視点だな、テストとかQAとかやってるとつい安全性ばかり考えてしまう #devsumif
2020-02-13 15:45:33
FJ
@FJKei
#devsumiF 何もしないシステムは安全。でも役に立たない。役に立つには活性が不可欠。どんなシステムもこの2つを考える必要がある。なるほど。
2020-02-13 15:46:38
iotas@創作+エンジニアリング
@tRiaeZ1
厳密な共通言語としての形式手法 性質のいいシステム順（上からマシなシステム） 1.故障したら止まる 2.故障したあともたまに復旧する 3.なんかよくわからない値を返す #devsumif
2020-02-13 15:53:39
tsuemura
@tsueeemura
TLA+面白かった。要件の組み合わせだったり、異常系だったりを数学的な表現で表して曖昧性を排除するのか。 #devsumif
2020-02-13 15:57:26
ΗΙＤΕΟ
@_hideoyamada
形式手法のまとめ ・自然言語による仕様は曖昧性を持つ ・形式手法によるモデリング ・より複雑な状況における解析の自動化 #devsumi #devsumiF
2020-02-13 15:59:03