第1章 論理で考える

1.1 形式手法の概要

1.1.1 高信頼化の総合技術

形式手法： 高信頼性への技術アプローチ

P.1下～

レビュー、テスト： 行う人による

P.2下～

形式仕様言語（こうなっているはず）
↓↑
プログラム・コード

1.1.2 複雑さと抽象化

テスト： バグを見つける

形式手法：バグがないことを示す

P.3下～

自然言語の仕様書はあいまい

↓

仕様を厳密に表すべき → 形式仕様言語

P.4中～

抽象化により複雑さを避ける

P.5上～

数理論理（厳密） + 抽象化モデリング

1.1.3 工学的な道具

形式仕様言語

↓↑人手で証明？

プログラム

P.5中～

手動証明： 使いものにならない

自動証明： 完全には無理

なので、ちょうどいい所を見つけなくてはならない。

[ex1-1] 最も属人性の低い作業を選んでください

[ex1-2] 最も厳密に表すべきものを選んでください

[ex1-3] 開発対象の機能を表すとき、最も抽象度が高い表現はどれですか

1.2 発展の経緯

1.2.1 形式手法の変遷

P.6下～

全体に適用 vs 部分的に適用
rigorous vs light

P.P.7～

仕様の表現力 vs 自動検証

1.2.2 設計方と形式手法

形式手法は設計方法論とセットである

P.8下～

アルゴリズム → Hoareロジック

P.9上～

構造化設計 → VDM, Z

P.9上～

リアクティブ(並列)システム → ロジック・モデル検査

P.9中～

UML → 要使い分け

P.9下～

オブジェクト指向 → 要使い分け

1.2.3 形式仕様言語の分類

• モデル規範型
  
• 性質規範型

[ex1-4] 次はどちらの使い方ですか： 正しく動作するコードの組み合わせでバグのないソフトウェアを目指す

[ex1-5] 次はどちらの使い方ですか： 利用可能な部分があればその部分に適用する

[ex1-6] テストと設計方法論と別物と考えられるが、形式手法と設計方法論はセットとなる理由は？

教科書（図はすべてこちらより引用）：
　中島震，「形式手法入門―ロジックによるソフトウェア設計―」，オーム社