ソフトウェア設計とテスト

情報科学学部無料 6 章有料 0 章

ソフトウェアが「仕様どおりに動く」ことを、設計（契約と不変条件）・テスト（網羅基準・性質ベーステスト）・ビルド（依存グラフ）・継続的インテグレーションの 4 つの層で保証する方法を、

想定読者: 大学生（理系）・社会人、プログラムは書けるが、設計・テスト・ビルド・CI を根拠をもって選べるようになりたい人

前提テーマ:ソフトウェア開発

このテーマの 100 本ノック（50 問）

目次

1. 第 1 章契約による設計：事前条件・事後条件・不変条件と Hoare 論理無料モジュールの仕様を事前条件・事後条件・不変条件の契約として書き、小さな命令型言語の上で Hoare 論理の健全性、最弱事前条件の性質、変量による停止性、表現不変条件の帰納法、振る舞いの部分型の置換原則を証明する。表明を入れた Python の実行例も示す。
2. 第 2 章テストの理論：網羅基準・同値分割と境界値・突然変異テスト無料テストが示せることと示せないことを定理として整理する。有限のテストの不完全性、網羅基準の包含関係と検出力の違い、MC/DC に要るテストの数、境界値テストが検出を保証する誤りのモデル、ペアワイズ網羅の大きさの上下界、突然変異テストを証明し、pytest と coverage.py の実行例で確かめる。
3. 第 3 章性質ベーステスト：性質の書き方・生成・縮約と検出確率無料入力を人が選ぶ代わりに、仕様を性質として書き入力を無作為に生成するテストを扱う。検出確率と必要な試行回数、境界値を混ぜた生成の効果、再帰的な生成器の大きさ、縮約の停止性、差分デバッグ ddmin の 1-最小性と実行回数、変成関係とモデルベーステストを証明し、Hypothesis の実行例を示す。
4. 第 4 章ビルドと依存関係：依存グラフ・増分ビルドの正しさ・版の解決無料ビルドを入力から成果物への関数とみて、トポロジカル順の存在、増分ビルドとクリーンビルドの一致、早期打ち切り、並列ビルドの時間の上下界、キャッシュのキーの健全性、版の解決の NP 完全性を証明し、最小のビルド系の実行例で確かめる。
5. 第 5 章継続的インテグレーション：パイプライン・不安定なテスト・二分探索とまとめ検査無料主ブランチの先頭が常に全検査に合格しているという不変条件を軸に、意味的な衝突とマージキュー、不安定なテストと再実行の損得、回帰の二分探索、まとめ検査の最適な大きさ、段階の並べ方、冪等なデプロイを確率と帰納法で証明し、実行例で確かめる。
6. 第 6 章事例研究：教科書サイトの検査系を読む（相互参照・依存の閉包・決定的な生成）無料定理に識別子を付けて相互参照する教科書サイトの検査を題材に、参照の解決の一意性、根拠のある命題の最小不動点としての特徴づけと線形時間の計算、採番の決定性、検査の健全性と完全性の限界、公開の不変条件を証明し、最小の実装と性質ベーステストで確かめる。