【感想・ネタバレ】Bメソッドによる形式仕様記述のレビュー

本位田真一 / 中島震 / 来間啓伸

[ブクログ · ★★★★★]

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

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