不具合はなぜ起こるのか

2020 T.Takeda

前提

古典コンピュータを対象とする
量子コンピュータは本議論に含まない

不具合とは何か

意図したとおりに動作しない状態
要求される機能を実行できない状態

💡品質や不具合に対する自分なりの考え方を見つけるヒントになれば幸いです。

不具合の形態

機械的に動かない
- →順に駆動部を目視で追うことで原因がわかる
電気的に動かない
- → 電気的な状態をテスターで観測することで原因がわかる
ソフトウェア的に動かない
- → プログラムの状態を観測することで原因がわかる

いずれも「動作」させることで動かないことがわかり、「観測」することで特定できる

ソフトウェアの不具合

機械より容易に複雑にできる（要因の多様化）
動作が圧倒的に高速（観測困難）
動作時の状態が複雑すぎて意図して補足しない限り、後から原因がわからないことがある（ログの必要性）
静的なコードに関しては履歴が残るため、いつからそうなっていたのかはわかる（追跡性）
履歴があるため「人によるエラー」と帰着されることが多いが、そもそも開発が「人による」ものなので、これは本質ではない（真因分析困難）

計算機のある世界

我々は当たり前に計算機が存在するため、経験的・直感的に計算機にできることを理解している

アナログ計算機などの変遷を目の当たりにしてきた人たちにとっては「計算できる」ということが当たり前ではなく、計算できるとはどういうことかを考える余地があった（もちろん我々にもある）

計算可能性理論

問題に対して計算可能性を考えるための理論分野
代表的なモデル
- チューリングマシン
- オートマトン
バベッジ、ラブレスに始まり、チューリング、ノイマンといった人々が代表的

チューリングマシン

集合、記号、入力、遷移函数、初期状態、受理状態などを持つ
入力に対して条件に応じて状態を遷移させることで動作する
実在の計算機はチューリングマシンと同じ原理
- ただし、実在の計算機リソースは有限である

チューリングマシン

ゲーデルの不完全性定理

ある性質を満たす自然数論の理論において決定不能な命題が存在することを示す（対角線論法で証明）

数学で証明できないことがないことを目指していた時代に、「自然数論を含む帰納的公理化可能な理論が、ω無矛盾であれば、証明も反証もできない命題が存在する」ことを明らかにした。

ゲーデル数

数学→計算機の世界に持ち込める
ゲーデル数の導入により、計算機と自然数を同一視できる
- 自然数の列に一対一に写像がとれる（符号化）

💡数学的にはそうでもないが、計算機的にはありがたい

数と符号の対応

チューリングの停止性問題

チューリングマシンが停止するかどうかを判定するチューリングマシンは構築できないことを示した

対角線論法で証明
- あるマシンは「判定マシンがYESのとき」停止しない
- あるマシンは「判定マシンがNOのとき」停止する
- 判定マシンはYESなら、あるマシンを停止する
- 判定マシンはNOなら、あるマシンを停止しない

チューリングの停止性問題

あるマシンが停止したとすると、判定マシンはNOを返す。判定マシンがNOのとき、「あるマシンは停止しない」ため、矛盾する。
あるマシンが停止しないとすると、判定マシンはYESを返す。判定マシンがYESのとき「あるマシンは停止する」ため、矛盾する。

ライスの定理

停止性問題を一般化した定理
「定められた性質Fを満たすかどうかを任意の部分計算可能関数について判定する方法は存在しない」
- ただし、性質Fが自明な場合を除く

わかりやすく言うと、

コンピュータにできることのために、コンピュータにできないことはないので、証明も反証もできないものが存在する

証明可能なことを仮定しても、性質的な矛盾をプログラムできる

ライスの定理

「定められた性質Fを満たすかどうかを任意の部分計算可能関数について判定する方法は存在しない」
- ただし、性質Fが自明な場合を除く

自明な性質F

任意の計算可能関数fに対して、fはFを満たす
任意の計算可能関数fに対して、fはFを満たさない

自明な性質Fの計算可能性

定められた自明な性質Fについて満たすかどうかを任意の部分計算可能関数について判定する方法は存在する

「定められた自明な性質F」とは？
1+1=2は自明か？
- 自明は相対的（自明でないことを自覚することは大事）

定められた自明な性質F

自明性とは、証明済みということ
証明済みの自明な性質の組み合わせは自明になるはず
証明済みの定理を積み上げる数学の証明と同じ

ペアノの公理

1+1=2が自明かどうかはペアノの公理が自明かどうか
- 自然数0が存在する
- 任意の自然数aには後続の自然数a+1が存在する
- 0はいかなる自然数の後続でない
- 異なる自然数は異なる後続の値を持つ
- 0がある性質を満たし、aがある性質を満たせば、その後続a+1もその性質を満たすとき、すべての自然数はその性質を満たす（数学的帰納法）

(参考) なんで計算って出来るんだろう？

1+2+3+…
1*2*3*…
1+2*3+…

+と*は違う演算なのにどちらも数値の集合に対して適用できている
当たり前のように組み合わせて無限につなげられる in 代数の世界

+の世界

対象: ... -1, 0, 1, 2, 3, ...
演算子: +:a -> b -> c
単位元: 0: a = a + 0 = 0 + a
結合則: a + b = b + a

*の世界

対象: ... -1, 0, 1, 2, 3, ...
演算子:*: a -> b -> c
単位元: 1: a = a * 1 = 1 * a
結合則: a * b = b * a

何かの世界

対象: X, Y, Z ...
演算子: f: X -> Y
単位元: u
結合則: f.g = g.f

対応している何かの世界

対象: F(X), F(Y), F(Z) ...
演算子: F(f): F(X) -> F(Y)
単位元: F(u)
結合則: F.G = G.F

対応関係の抽象概念を定義できそうである

抽象概念を内包する抽象概念

圏論はここを定義した抽象概念

Pos圏
対象: 半順序集合
射: 単調写像

圏から見た具象圏

半順序集合A
反射性: a ≤ a
推移性: a ≤ b, b ≤ cならa ≤ c
反対称性: a ≤ b, b ≤ aならa=b

線形順序集合
実数Rでx ≤ y

カリー=ハワード同型対応

計算機プログラムと証明の対応関係のこと

P⇒Qの論理学の世界に持ち込める
プログラム=証明
型=命題

Haskell（=Curry）

圏論に根ざした設計
静的型付け（強力な型推論）
部分計算可能関数を構成できる
同じ関数に同じ入力を与えると同じ答えが返る
変数の値は不変である
無限リストを扱える
検証しやすい

💡「コンパイルが通るとロジカルに不具合がない言語」と言われる所以

定理証明支援系言語

Coqなど
OCaml（オブジェクト指向の関数型言語）実装
実用例
- 四色問題の証明
- OpenSSL脆弱性の発見

定理証明支援系の課題

学習コスト
- 関数型言語全般にもいえる
- 手続き型は人にわかりやすい（代わりに矛盾を生む）
証明可能な状態に落とし込む能力と労力
- 証明系と等価な言語でない場合にプログラミングと証明系の記述両方が必要になる
費用対効果が見合うか？
- 数年に一度問題が起こるレベルを許容して問題に対応する方にコストをかける考えもある

定理証明系の真価

証明済みモジュールの積み上げ
- OSSとしてみんなで持ち寄れば加速する
重要性、複雑性の高いものに部分適用する
- そこには仕様以外の不具合がないことを証明できる

証明系の実用例

交通系システム（車、電車、航空機）
航空宇宙
インフラ（電力、エレベーターなど）
金融
暗号、通信
組み込み（ICカード、自動販売機など）

型、設計、ユースケース

型はオブジェクトの要素の一つ
オブジェクトは設計により導出される要素
設計はユースケースからビジネスの言葉として表現される

ここまでのまとめ

計算可能性を数学的に捉える
型、関数を自明な性質Fとして構成することでテスト可能になる
証明(=テスト)を積み上げる
自明な性質F = 型 => オブジェクト => ユースケース
- 使われ方を定義し、テストすることの重要性

テストの必要性について

テストの意義

Program testing can be used to show the presence of bugs, but never to show their absence!(Prof.dr. Edsger W. Dijkstra, April 1970, EWD249)

テストに失敗することで「不具合があること」がわかる
テストが通る=不具合がない、ではない
さらにテストそのものに不具合があることもある

かつてのテストの立ち位置

計算リソースがPoorでプログラムがそれほど複雑ではなかった時代

テストは現実的ではない
完全なテストをやることはできない
テストをやる意味はない

💡「証明を行えばよい」というのは一つの解

今のテストの立ち位置

計算リソースが潤沢でプログラムが複雑な時代

部分的にでもテストした方がよい
自動的に大量のテストを流せる（CI/CD）
手続き型が主流でシステムが複雑になり証明が難しい

TDDの意義

×実装してから不具合を修正する
- 実装時点で不具合があると言うことは、最初から品質が低いものを作っていることになる
- そこからテストケースを作って品質を上げても「動く」ところで品質が止まる
○最初からテストして不具合を入れない
- TDDでは自明な性質を先に定義する
- 性質を満たす状態を維持して実装する
- 最初から品質高く生み出して維持する

💡TDDが本質ではなく、品質を高く生み出すことが重要

TDDでやっていること

テストケース	プログラム
1. ユースケースを定義	2.ユースケースを満たしていない状態
すべてのテスト失敗
4. テスト一部成功	3. 実装を進める
テスト一部失敗
5. すべてのテスト成功	6. 実装完了
	ユースケースを満たした
8. すべてのテスト成功	7. リファクタリング

💡TDDは不具合が起こりにくい状況で開発を進めるための一つの手法

これからのテストの立ち位置？

ユースケースに即したテストを実施
変更箇所に即したテストのみを自動実行
テストしやすいプログラミング言語の利用
検証しやすいプログラミング言語の利用

不具合とは何か

ユースケース通りに動作しない状態
ユースケースがない
- => 仕様か不具合かすら判断がつかない
ユーザーの使い方を列挙することの重要性

Right Software

完璧なソフトウェアは存在しない
でも、「不具合がないことを証明できない」と思い込まない
だからとテストを網羅的に拡充すればよいというものでもない
- イントラクタブル
  - a+bのテストを全値域のa,bについて網羅的にテストしない
  - ペアノの公理に乗っかる
  - コンパイラやインタプリタは検証済みで自明とする
ただし、マシンパワーで全数やるのも時としては手

数学ではなく工学

暗号化に利用している巨大素数は、おおよそ素数らしいもの
- 数学者から見れば素数ではない
- NP問題の一つ
四色定理
- コンピュータにより証明したが、初期には数学者からはプログラムの不具合が疑われた
ナイトツアー、N-queen、素数、円周率、ABC予想・・
- マシンパワーで探索できることもある
囲碁、チェス、将棋・・
- EXPTIME問題でも人類はそれなりの解を得ている

難しさの度合いは計算量で考える

P（多項式時間で解ける判定問題）
NP（非決定性多項式時間の問題）
- NP困難・・巡回セールスマン問題
- NP完全・・ハミルトン閉路
- co-NP・・素数判定
EXPTIME（指数関数時間で解ける決定問題）・・ボードゲームの形勢判定
BPP（確率的に多項式時間で解ける決定問題）・・ビュッフォンの針
BQP（量子コンピュータで確率的に多項式時間で解ける決定問題）

テストは必要か？

プログラム的な不具合はなくせる
仕様通りであることを数学的に証明できる
仕様が誤っていることはわからない
- 条件を満たした時に0なのか1なのか、それは人間が決めること
抜けがあることはわからない
- 「N秒以内に応答する」という要求がなければ無限時間で停止しなくてもよい？
脆弱性や未定義の動作はわからない
- これは不具合とは異なる観点

設計の観点から

設計の心得

要求をモデルに
モデルをシステムに

モデルは「ビジネスの言葉で表現する」
ダメな例
- 金額はUnsigned Integerで定義し、Yenクラスのメンバーとする
- → こんなことを書いてる間に実装した方がいい

抽象度と時代の変遷

抽象度と時代の変遷図

実装前に適切にモデリングする

別の機会に紹介

公理的設計

独立公理
- 設計行列を独立設計/準独立設計にする
- 要求機能が干渉せず、互いに独立した設計がよい
情報公理
- 情報量を最小化する=成功確率を最大化する
- 必要な情報量が少ない設計がよい
（公理=証明不要な真理）

独立設計

FR・・要求機能
DP・・設計解
X/0・・要求と設計の関係

$$ \tiny{ \begin{Bmatrix} FR_1 \\ FR_2 \\ FR_3 \\ \vdots \\ FR_n \\ \end{Bmatrix} = \begin{bmatrix} X & & \dots & 0 & 0 \\ & X & & & 0 \\ \vdots & & \ddots \\ 0 & & & X & \\ 0 & 0 & \dots & & X \end{bmatrix} \begin{Bmatrix} DP_1 \\ DP_2 \\ DP_3 \\ \vdots \\ DP_n \\ \end{Bmatrix} } $$

Xが変更された時は対応するDPのみを修正すればよい

準独立設計

FR・・要求機能
DP・・設計解
X/0・・要求と設計の関係

$$ \tiny{ \begin{Bmatrix} FR_1 \\ FR_2 \\ FR_3 \\ \vdots \\ FR_n \\ \end{Bmatrix} = \begin{bmatrix} X & & \dots & 0 & 0 \\ & X & & & 0 \\ \vdots & & \ddots \\ X & & & X & \\ X & X & \dots & & X \end{bmatrix} \begin{Bmatrix} DP_1 \\ DP_2 \\ DP_3 \\ \vdots \\ DP_n \\ \end{Bmatrix} } $$

$\small{DP_1, DP_2, \dots, DP_n}$と順に解決可能
Xが変更された場合はそれ以降のみ影響

干渉設計

FR・・要求機能
DP・・設計解
X/0・・要求と設計の関係

$$ \tiny{ \begin{Bmatrix} FR_1 \\ FR_2 \\ FR_3 \\ \vdots \\ FR_n \\ \end{Bmatrix} = \begin{bmatrix} X & & \dots & X & X \\ & X & & & X \\ \vdots & & \ddots \\ X & & & X & \\ X & X & \dots & & X \end{bmatrix} \begin{Bmatrix} DP_1 \\ DP_2 \\ DP_3 \\ \vdots \\ DP_n \\ \end{Bmatrix} } $$

$\small{\begin{Bmatrix}FR\end{Bmatrix}=A\cdot\begin{Bmatrix}DP\end{Bmatrix}}$より$\small{\begin{Bmatrix}DP\end{Bmatrix}=A^{-1}\cdot\begin{Bmatrix}FR\end{Bmatrix}}$
$\small{DP}$を求めるためには逆行列を計算する必要がある
一つでもXが変更されると再計算が必要 = 再設計

日本に多い設計

元来「すりあわせ」が得意で、ずれを補正して作り上げていく
- 手続き型と相性はよい
作りあげる時はよいが、変更する時のことを考慮できていない場合がある

独立公理の重要性

干渉 = 変更を加えると別の要求機能に影響が出て、その要求機能を直すと別の要求機能に影響する状態

設計が独立しておらず、テスト範囲も干渉すべてに及ぶため、一般に開発要員:検査要員=1:1くらいの体制が必要になる

MECEに設計する

性質や機能、モデルについて抜け漏れ、重複なく全体をカバーする設計を目指す
残念ながら、何度でもMECEにできる人は4割程度
- ヒントをもらうとMECEになる人が4割程度
- → 一人で考えないだけで8割程度の人はMECEにできる
- MECEに考えて、完璧を目指さない

設計時の確認観点

主従関係
階層関係
要求機能か設計解か
機能か効果か

主従関係

主が満たされると従属は連鎖的に満たされる

主従関係

階層関係

上位の対策が変わると下位は検討不要になるか別のものとなる

階層関係

要求機能か設計解か

社員の能力を高めたい
eラーニングを実施する

設計解

機能か効果か

社員の能力を高めたい
eラーニングを配信する
効果計測を行う

設計は段階的

段階的

不具合も段階的

不具合の段階

混入フェーズ

要求 ← ユースケースをしっかりと確認

設計 ← 性質、モデリングをMECEに

実装 ← ツールで防ぐ、スキル向上で防ぐ

テスト ← ここは設計がしっかりしていれば防ぎやすい

運用 ← 手順書、SLA、チェックリスト、分析で対応

不具合が問題になるとき

サービス提供できていないときに問題となる
市場不具合のあるサービスは価値提供できていないと考える
- いくら追加開発しても無駄な状態
- バグ、即、斬

💡「不具合をゼロにする」のではなく、「価値提供できているか」がポイント
💡使われない機能に不具合があってもよい。永遠に顕在化しない。

段階的な設計

ユースケース定義（これを満たす性質を明らかにする）
モデリング（ビジネスの言葉で本質を表現）
実装設計（値域、データ量、システム制約）
環境設計（時間制約、空間制約、コスト、脆弱性）

落ち着いて設計を

エンジニアの特性として、
- 実装のための設計になりがち
- 実装に入るのを急ぎがち
実装できるのはわかっているので、そこは急がない
- 設計がきちんと終わってからでよい

（参考）モデリングレベル

レベル	状態
Lv.0	モデルなし
Lv.1	文言のみ
Lv.2	文言+図
Lv.3	図+文言
Lv.4	詳細な図+文言
Lv.5	図のみ

ER図からDBが生成される
UML図からコードが生成される
ような世界を目指している

Wrap-up

不具合とは何か

性質を満たさない状態のこと
性質を定義しない限り、不具合というものは存在しない
- すべて未検討、仕様外ということになる

人類はどこを目指すか

プログラミングは手段でしかなく、サービスを提供したい
設計がそのままサービスになるのであれば、それに超したことはない
ビジネスとしての関心事に注力したい
- クラウド化、マネージドサービスの活用も同じ目的

ユースケースは不変の関心事

モデルは「ビジネスの言葉」でユーザーのために書く
洗練されたモデルであれば50年後に同じサービスが作れる
- サーバーがオンプレでもクラウドでも変わらない
- プログラミング言語がPythonでもHaskellでも変わらない
- 利用環境がWindowsでもUbuntuでも変わらない
裏を返すと、
- 言語依存の設計、環境依存の設計、OS依存の設計は分離すべき関心事

まとめ

ユースケースを定義する
モデリングする（MECEに考える）
モデル、実装、環境の観点で設計を見直す（繰り返す）
ユースケースを満たすテストケースを書く
テストケースの示す性質を満たす実装をする
テストが成功する状態でリファクタリングする

もっとまとめる

ユースケースから満たすべき性質を明確にする
性質に応じたテストを行う
品質高く生み出して維持する

不具合はなぜ起こるのか

2020 T.Takeda

前提

関連する分野

不具合とは何か

不具合の形態

ソフトウェアの不具合

計算機のある世界

計算可能性理論

チューリングマシン

ゲーデルの不完全性定理

ゲーデル数

チューリングの停止性問題

チューリングの停止性問題

ライスの定理

わかりやすく言うと、

ライスの定理

自明な性質F

自明な性質Fの計算可能性

定められた自明な性質F

ペアノの公理

(参考) なんで計算って出来るんだろう？

+の世界

*の世界

何かの世界

対応している何かの世界

抽象概念を内包する抽象概念

圏論はここを定義した抽象概念

圏から見た具象圏

カリー=ハワード同型対応

Haskell（=Curry）

定理証明支援系言語

定理証明支援系の課題

定理証明系の真価

証明系の実用例

型、設計、ユースケース

ここまでのまとめ

テストの必要性について

テストの意義

かつてのテストの立ち位置

今のテストの立ち位置

TDDの意義

TDDでやっていること

これからのテストの立ち位置？

不具合とは何か

Right Software

数学ではなく工学

難しさの度合いは計算量で考える

テストは必要か？

設計の観点から

設計の心得

抽象度と時代の変遷

実装前に適切にモデリングする

公理的設計

独立設計

準独立設計

干渉設計

日本に多い設計

独立公理の重要性

MECEに設計する

設計時の確認観点

主従関係

階層関係

要求機能か設計解か

機能か効果か

設計は段階的

不具合も段階的

混入フェーズ

不具合が問題になるとき

段階的な設計

落ち着いて設計を

（参考）モデリングレベル

Wrap-up

不具合とは何か

人類はどこを目指すか

ユースケースは不変の関心事

まとめ

もっとまとめる