Bメソッドによる形式仕様記述 ソフトウェアシステムのモデル化とその検証 トップエスイー実践講座1

中島震【監修】, 来間啓伸【著】

• 販売会社／発売会社: 近代科学社
• 発売年月日: 2007/12/25
• JAN: 9784764903470

商品レビュー

2011/06/15

抽象機械、変数の宣言、不変条件の宣言、変数の初期化、操作の定義、一般化代入の紹介がある。
抽象機械の整合性の検証として、最弱事前条件、不変条件の無矛盾性、初期化の整合性について説明がある。
集合論的に厳密に記述していくのがミソのようです。
Refinementという段階的詳細化をしていって実装までたどり着きます。各段階間の整合性を確認することによって、実装が抽象的に検討した性格を保っていることを保証します。
トップエスイー講座は受けにいけませんでした。

読者である北海道立工業試験場の堀さんに２度講習会を開いていただきました。