中島震のレビュー一覧
-
抽象機械、変数の宣言、不変条件の宣言、変数の初期化、操作の定義、一般化代入の紹介がある。
抽象機械の整合性の検証として、最弱事前条件、不変条件の無矛盾性、初期化の整合性について説明がある。
集合論的に厳密に記述していくのがミソのようです。
Refinementという段階的詳細化をしていって実装...続きを読むPosted by ブクログ -
▪️サービス化
"As a service"と呼ばれるビジネスモデルでは、メーカーが機器をアセットとして保有し、ユーザーに貸し出す。ユーザーは初期投資を削減できる。メーカーは機器の所有権を保有しているため、ソフトウェアのアップデートや機器からの情報収集を容易に行える。一例として、KUKAは"Robo...続きを読むPosted by ブクログ -
初心者向けSPINの実用書です。
SPINとは、"Simple Promela Interpreter"の略で、"Promela"は、Gerard J. Holzmannが作った並列処理を伴う状態遷移(オートマトン)を記述できる形式仕様記述言語のことです。
この本は、実例(Promelaプログ...続きを読むPosted by ブクログ