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^)／