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

ウェブ全体の検索

Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers。テスト駆動開発(TDD)より、形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)。2021年02月01日 09時13分39秒

ASAHIネット(http://asahi-net.jp )のブログサービス、アサブロ(https://asahi-net.jp/asablo/ )を使っています。
---
 お買い上げありがとうございます。
 形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)の本です。

https://www.amazon.co.jp/exec/obidos/ASIN/032114306X/showshotcorne-22/
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers Paperback – Illustrated, July 19, 2002
by Leslie Lamport (著)
¥5,081

 詳しく書いている時間がないので、形式手法については、関連を読んでください。
 Suica(スイカ)やPasmo(パスモ)など、交通系ICカードを始め、様々なICカードに入っている、ソニーのフェリカネットワークスのFeliCaのチップは、形式手法を使って開発されました。
 まだ書いてない話は、もう5年くらい前になると思うが、Amazonも形式手法を使って、システムやサービスの開発をやってるんですよね。

 TLA+は、チューリング賞受賞者であるランポート(Leslie Lamport)先生が作った形式仕様記述言語。
 ランポート先生は、LaTexで馴染みがある人もいるだろうが、分散環境の研究、たとえば、ビザンチン・フォールト・トレランス(Byzantine fault tolerance, BFT)の研究でも有名。
 超一流の人は、何をやっても超一流ですね。

 そういえば、Javaは流行らなかったをはじめ、最近では、ブロックチェーンで、ITC技術の解説で大嘘やトンデモを書きまくり、しゃべりまくって、金儲けをしている経済学者の野口悠紀雄。
 ブロックチェーンで、改竄不可能、ビザンチン将軍問題が解けたなど、嘘、誇張を書いてたもんね。
 嘘や筋の悪い話を書いているのに、出版社の編集部が、科学リテラシー、技術リテラシーが低いから、出版しちゃうんだよね。
 こういう総体が、失われた10年が20年になり30年になってる要因の一つ。

https://en.wikipedia.org/wiki/TLA%2B

https://www.amazon.co.jp/exec/obidos/ASIN/1484238281/showshotcorne-22/
Practical TLA+: Planning Driven Development Paperback – October 12, 2018
by Hillel Wayne (著)
¥3,745

https://www.amazon.co.jp/exec/obidos/ASIN/B07FMHX7M2/showshotcorne-22/
Practical TLA+: Planning Driven Development (English Edition) 1st ed. Edition, Kindle Edition
by Hillel Wayne (著) Format: Kindle Edition
¥3,386

 Apressにある紹介。Apressでは、いま、3,431円ですが、この価格で、PDF, EPUBが入手できます。
 Apressはしばしばセールをやるので、急がない人は、メルマガ登録して、セールの告知があってから買ってもいいと思います。

https://www.apress.com/jp/book/9781484238288
Practical TLA+
Planning Driven Development
Authors: Wayne, Hillel
eBook¥3,431
price for Japan (gross)

関連:
http://iiyu.asablo.jp/blog/2018/10/30/8985607
テスト駆動開発(TDD)より、形式手法(フォーマルメソッド、形式仕様記述、Formal Methods)。九州大学(九大)の荒木啓二郎先生が、熊本高等専門学校(熊本高専)の校長に!記念、形式手法とネットワーク技術シンポジウム
http://iiyu.asablo.jp/blog/2017/11/01/8718707
ラムダノート(LamdaNote)社の新刊「Goならわかるシステムプログラミング」「定理証明手習い」。テスト駆動開発(TDD)の限界、Formal Methods(形式仕様記述、形式手法)のことも。
http://iiyu.asablo.jp/blog/2011/12/28/6266615
形式手法導入パイロット教育コース
http://iiyu.asablo.jp/blog/2011/09/19/6107007
文章が駄目ならシステムも駄目、形式仕様記述(フォーマルメソッド)のことも
http://iiyu.asablo.jp/blog/2011/02/04/5662037
仕様記述言語Alloy, Software Abstractionsの翻訳がオーム社から出そう\(^O^)/
http://iiyu.asablo.jp/blog/2010/09/18/5354010
関数プログラミングの楽しみ
http://iiyu.asablo.jp/blog/2010/07/29/5254545
VDM++によるオブジェクト指向システムの高品質設計と検証
http://iiyu.asablo.jp/blog/2010/07/29/5254556
フォーマルメソッド(形式仕様記述、Formal Methods)の教科書
http://iiyu.asablo.jp/blog/2006/08/20/491884
形式仕様記述(フォーマルメソッド、Formal Methods)
http://iiyu.asablo.jp/blog/2010/08/10/5277689
地球なう。おれのサンプルリターンは大成功\(^O^)/

コメント

コメントをどうぞ

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

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

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

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

コメント:

トラックバック

_ ホットコーナー - 2021年08月13日 10時12分57秒

ASAHIネット(http://asahi-net.jp )のブログサービス、アサブロ(https://asahi-net.jp/asablo/ )を使っています。
---
 Apressが、現地時間、8月20日まで、大セールをやってます。
https://twitter.com/shownakamu