ASAHIネット(http://asahi-net.jp )のブログサービス、アサブロ(https://asahi-net.jp/asablo/ )を使っています。
---
http://iiyu.asablo.jp/blog/2021/09/29/9427965
テスト駆動開発(TDD)より、形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)。ランポート先生(Leslie Lamport)のTLA+, 実践TLA+、Suica, Pasmoも、Amazon AWSも、FINAL FANTASY XV POCKET EDITIONもフォーマルメソッド
などでも、紹介しているHillel Wayne「実践TLA+」。
　翔泳社で売っているPDF版は、他のPDF版がポイント10%還元のときも、なぜか、ずっと40%ポイント還元だった。何かの間違いだろうと思っていて、早くお知らせしようと思っていたが、例によって書けずにいたら、また翔泳社祭りが始まって、50%ポイント還元になって、実践TLA+も50%還元になっていた。
　2023/02/23までだから、急げ！
　でも、それが終わっても、以前みたいに40%ポイント還元に戻るのかな。どうなるのかな。

https://ja.wikipedia.org/wiki/TLA%2B
TLA+
には、以前紹介した、AWSで使った例のほか、Microsoftも使っている例が出てますね。
　これ、書いたと思うけど、また書くが、AWSの例では、プログラマたちに数学だというと拒否反応が出るだろうから、網羅的なテストツールだといって使ってもらえるようにした話があって、いかにもというエピソードだと思いました。

　TDD(テスト駆動開発)を全面否定するわけではないけど、所詮、テストケースは人間が思いついたものしかなく、数学的に正しさを証明してるわけではないので、どうしても漏れが出る。
　特に、並列処理や分散環境の世界だと、単体テストはOKでも、テストを実行している瞬間のマシンの状態、ネットワークの状態などによって、タイミングの問題で結果がOKだったりNGだったりするので、テストにならないことが多い。
　そういう世界は、モデルを数学的に正しいかどうかチェックしないとだめ。
　これも書いたかどうか。Sunにいたハードウェアの技術者が、Googleに転職して(おそらく、SunがOracleに買収されたから？)、ソフトウェア開発の世界で、モデル検査をやらないのに驚いた話を書いていた。
　ハードは実際に物を作る前に、設計段階で徹底的にモデル検査をしてバグがないことを証明しないと、現物を作ってバグがありましたじゃ、損害が大きいから、仕様を記述してモデルを検査するのは当たり前。
　ソフト屋はそういう厳密な製品開発をしてないので、驚いたという話。

https://www.seshop.com/product/detail/24750
実践TLA+【PDF版】
Hillel Wayne（著） , 株式会社クイープ（翻訳） , 株式会社クイープ（監修）

https://www.amazon.co.jp/exec/obidos/ASIN/4798169161/showshotcorne-22/
実践TLA+ 単行本（ソフトカバー） – 2021/9/15
Hillel Wayne (著), 株式会社クイープ (翻訳, 監修)

https://www.amazon.co.jp/exec/obidos/ASIN/B09BJ44451/showshotcorne-22/
実践TLA+ Kindle版
Hillel Wayne (著), 株式会社クイープ (翻訳, 監修) 形式: Kindle版

　以前、お買い上げがあったのが、ランポート先生御自らの著書。
https://www.amazon.co.jp/exec/obidos/ASIN/032114306X/showshotcorne-22/
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers ペーパーバック – イラスト付き, 2002/7/19
英語版 Leslie Lamport (著)
￥9,174
　ぎゃー、以前紹介したときは、¥5,081だったのに。円安だから？

関連：
http://iiyu.asablo.jp/blog/2021/09/29/9427965
テスト駆動開発(TDD)より、形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)。ランポート先生(Leslie Lamport)のTLA+, 実践TLA+、Suica, Pasmoも、Amazon AWSも、FINAL FANTASY XV POCKET EDITIONもフォーマルメソッド
http://iiyu.asablo.jp/blog/2021/02/01/9343037
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers。テスト駆動開発(TDD)より、形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)。
http://iiyu.asablo.jp/blog/2018/10/30/8985607
テスト駆動開発(TDD)より、形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)。九州大学(九大)の荒木啓二郎先生が、熊本高等専門学校(熊本高専)の校長に！記念、形式手法とネットワーク技術シンポジウム

NHKのデタラメな番組について：
応援してくださる方は、これ↓のリツートをお願いします。
https://twitter.com/shownakamura/status/1527835631699005440
NHK「ノーナレ」、仮名漢字変換の歴史、浮川夫妻が発明は大嘘。管理工学研究所の我々が先。あのノーナレは歴史を改竄、捏造した歴史修正主義トンデモ悪質番組
https://iiyu.asablo.jp/blog/2022/05/18/9491639