Google
ブログ(iiyu.asablo.jpの検索)
ホットコーナー内の検索
 でもASAHIネット(asahi-net.or.jp)全体の検索です。
 検索したい言葉のあとに、空白で区切ってki4s-nkmrを入れるといいかも。
 例 中村(show) ki4s-nkmr

ウェブ全体の検索

テスト駆動開発(TDD)より、フォーマルメソッド(Formal Methods, 形式手法、形式仕様記述)。Hillel Wayne「実践TLA+」は以前からなぜか40%ポイントのままだったけど、いま、翔泳社祭りで50%ポイント、急げ! Leslie Lamport「Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers」はほぼ倍の値段になってる(>_<)2023年02月21日 12時40分40秒

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

コメント

コメントをどうぞ

※メールアドレスとURLの入力は必須ではありません。 入力されたメールアドレスは記事に反映されず、ブログの管理者のみが参照できます。

※なお、送られたコメントはブログの管理者が確認するまで公開されません。

※投稿には管理者が設定した質問に答える必要があります。

名前:
メールアドレス:
URL:
次の質問に答えてください:
一富士、二鷹、三は? ひらがなで。

コメント:

トラックバック

_ ホットコーナー - 2023年04月01日 01時34分58秒

ASAHIネット(http://asahi-net.jp )のブログサービス、アサブロ(https://asahi-net.jp/asablo/ )を使っています。
---
 すみません。公私ともにいろいろあって、早く書かないから、次のKindle本が半額

_ ホットコーナー - 2023年04月30日 19時31分48秒

ASAHIネット(http://asahi-net.jp )のブログサービス、アサブロ(https://asahi-net.jp/asablo/ )を使っています。
---
 インプレスのKindle本ゴールデンウイークセール、紀伊國屋書店のKinoppyもすごい。