pdfファイル

情報社会の将来
情報科学概論
z
ソフトウェアの論理
目に見える変化
z
z
z
亀山 幸義
http://logic.is.tsukuba.ac.jp/~kam
2003.09.26
z
z
コンピュータのハードウェアは日進月歩
様々な新しい情報機器の登場
家電の情報化
10年先どころか5年先も予想が難しい
情報社会の鍵は？
z
ソフトウェア
z
z
z
ソフトウェアの高機能化、高性能化、使いやすさの向上
あらゆる機器が情報化（知能化）される
情報社会の弱点は？
z
ソフトウェア
1
ソフトウェアがひきおこした
社会的問題
z
ソフトウェア科学とは
枚挙に暇がない
z
z
z
z
z
z
z
2
z
Y2K(西暦２０００年）問題
スペースシャトルの打上げ延期
銀行ＡＴＭのダウン
航空券発券システムのダウン
携帯電話（電話機）の回収
Windowsシステムを狙ったウィルス
etc. etc. etc.
ソフトウェアに対する2つの立場
z
z
z
ソフトウェアを使って様々な対象領域の問題を解く
ソフトウェア自身を研究対象とする
ソフトウェア科学の目指すもの
z
z
z
高機能、高性能ソフトウェアの構成方法
使いやすいソフトウェアの構成方法
安定して、高い信頼性をもつソフトウェアの構成方法
3
4
高信頼ソフトウェアへ向けて
z
今週：正しいソフトウェアとは何か？
z
z
z
ソフトウェアの正しさ
形式化と論理
ソフトウェアの仕様と正当性
来週：ソフトウェアの正しさを保証するにはどうし
たらよいか？
z
厳密な方法；定理証明、Hoare論理
z
近似による方法；型システム、抽象解釈
有限の場合の方法；モデル検査、時相論理
z
5
6
1
未来社会とソフトウェア科学
z
未来の社会
z
z
z
z
int foo (int x, int y) {
int w = x;
int z = 0;
while (w >= y) {
z = z + 1;
w = w – y;
}
return z;
}
社会の隅々に情報機器、情報システムがゆきわたる
社会の隅々にソフトウェアがゆきわたる
社会の隅々に不安定要因がゆきわたる
従来 （つい最近まで）
z
z
z
C言語で書いたプログラム
高信頼化の対象は、人命のかかるシステムなどの safety
critical software
e.g. 自動車のエンジン制御のソフトウェア
現在、近い将来
z
z
問題発生時の社会的、経済的損失の増大
あらかじめソフトウェアを作る段階で、時間とコストをかけて信
頼性を高める方が結局は得策
このプログラムは「正しい」だ
ろうか？
z
C言語のコンパイラを通る（コ
ンパイルエラーがない）
実行時にエラーで止まること
がない
意図した通りに動く
z
z
7
C言語で書いたプログラム
int foo (int x, int y) {
int w = x;
int z = 0;
while (w >= y) {
z = z + 1;
w = w – y;
}
return z;
}
z
8
C言語で書いたプログラム
何はともあれ、実行してみよう
x=5, y=3
w=5, z=0
w >=y … 真
z=1
w=2
w >=y … 偽
foo(5,3)の答えは 1
int foo (int x, int y) {
int w = x;
int z = 0;
while (w >= y) {
z = z + 1;
w = w – y;
}
return z;
}
「foo (x, y) は x を ｙ で
割った商を返す関数であ
る」という仮説を立てられ
そうだ
本当にそうだろうか？
9
C言語で書いたプログラム
int foo (int x, int y) {
int w = x;
int z = 0;
while (w >= y) {
z = z + 1;
w = w – y;
}
return z;
}
10
C言語で書いたプログラム
「どんな整数 x と整数 ｙ に対
しても foo(x, y) は x を ｙ
で割った商を返す関数で
ある」
NO! これは正しくない
foo (3, -2)
を計算すると
止まらない！
負の数のことを考えていなかっ
た！
11
int foo (int x, int y) {
int w = x;
int z = 0;
while (w >= y) {
z = z + 1;
w = w – y;
}
return z;
}
では、このプログラムは｢正しく
ない」のだろうか？
必ずしもそうではない
「どんな整数 x と ｙ に対しても
foo (x, y) は x を ｙ で割った
商を返す関数」は誤りだが
「どんな正の整数 x と ｙ に対し
ても foo(x, y) は x を ｙ で
割った商を返す関数」は正し
い
12
2
正しいプログラムとは？
z
z
プログラムだけを見て、正しいかどうかを判断するこ
とはできない。
｢プログラムがどのように動作してほしいか」という性
質(条件）を、プログラムの仕様 (specification)とい
う。
z
z
z
仕様１｢すべての整数 x, y に対して。。。」
仕様２｢すべての正の整数 x, y に対して。。。」
｢正しさ｣の定義
z
z
プログラムが仕様を満たすとき、そのプログラムはその仕
様に関して正しい(その仕様の正しい実現である）という。
関数 foo は、仕様1を満たさないが、仕様2を満たす。 13
仕様２(正の整数に対する割り算）に関して、先
のプログラムfooが正しいことを厳密に保証する
ことはできるだろうか？
z
z
z
z
割り算をするプログラムの仕様は？
z
z
｢正の整数」とは何か？｢商｣とは何か？｢割る」とは何
か？
仕様を自然言語（日本語や英語）で書いている
限り、｢厳密な（確実な）保証」はができない。
z
14
形式仕様 (formal specification)
仕様
z
ソフトウェアの仕様
z
z
自然言語： 意味があいまいなことがある
形式言語： 意味がきちんと（一意的に）定まっている。
入力(input) は、正の整数 x と y
出力(output)は、０以上の整数 z と w
x, y, z, w の関係（入出力関係）を論理式で書く
x = y * z + w ...これでは条件が不足している
(x = y * z + w) かつ (0 ≦ w < y) ...これが正解
形式仕様：
形式言語（通常は論理式）を使って記述した
仕様
15
ソフトウェアの開発過程
論理による形式化
(頭の体操）
（x=y*z+w)かつ...
Validation
形式仕様
16
Verification
要求
『割り算のプログ
ラムが欲しい』
プログラム
p
int foo (int x, …) { … }
本講義では、これ以降、Verification（検証）のみを扱う。
17
18
3
定義可能数
z
z
定義可能数
日本語の文により、一意的に値が定まる自然数
を、「定義可能数」あるいは「D数」と呼ぼう。
(D...definable)
z
z
z
Ｄ数の例
z
z
z
z
最大のＤ数はあるか？
Ｎ文字以下の日本語で定義可能な最大のＤ数はある
か？
z
１００＋３００＊２
９９９９９９９９９９
富士山の高さをメートル単位で表したもの（小数点以
下は切り捨て）
２００３年１月１日午前０時に宇宙にある分子数
NO. いくらでも大きなＤ数が定義できる
z
z
z
z
YES
日本語で使う文字の種類は有限個（高々、数千、数万）
有限個の文字をＮ文字以下並べてできる文字列は有限個
そのうち自然数を一意的に定義しているものは有限個
有限個の自然数の集合は最大値を持つ
19
20
逆理（paradox)
最大の定義可能数
「２７文字以下で定義可能な最大の
自然数」をＸとする
このようなＸは一意的に存在する
z
正しい(正しそうな）推論を積み重ねることによっ
ていつの間にか矛盾(contradiction)が生じる
z
有名な例
z
「２７文字以下で定義可能な最大の
自然数に１を足した自然数」をＹとする
素朴な集合論におけるＲｕｓｓｅｌlの逆理「x ∈xでないx
をすべて集めた集合」を考えると矛盾する
z
z
このようなＹも一意的に存在する
⇒ Ｙ＝Ｘ＋1 かつ Ｘ≧Ｙ
現代集合論が発生する契機となった
正しそうに見える推論過程（あるいは正しいと
思っていた仮定)のどこかに誤りがある
z
｢大体正しい」という議論に対する戒めでもある
21
最大のＤ数の逆理
z
z
z
z
z
まともな定義
推論過程をふりかえろう
z
z
z
z
このような定義は「まとも」である
z
z
どんな日本語の文を与えられても、それが自然数を一意的に
定義しているかどうかを判定することは（おそらく）できない
z
z
０ と １ はＤ式である
ｘ と y がＤ式であるとき、(ｘ＋ｙ) と (ｘ＊ｙ) はＤ式である
ｘ がＤ式であるとき、(ｘ！) はＤ式である
z
１．Ｄ数の定義：日本語の文により、一意的に値が定まる自然
数
２．２７文字以下で定義できるＤ数のうち最大のものが存在
３．この数に１を足した数が２７文字以下で一意的に定義できて
しまう
実は、２，３でなく、1が問題
｢日本語の文により、一意的に定まる」とは？
z
22
z
「奇数の完全数のうち最小のもの」
「四色で塗りわけられない最小の地図のサイズ」etc.
定義になっていないものから出発したのがいけなかった。
z
23
どんな文字列を与えられても、それがＤ式であるかどうかは機
械的に判定できる。
基本的な場合から始め、次のものを作り出す場合を有限回適
用して構成されるもの全体がきちんと定まる。
このような定義を帰納的定義（inductive definition)という。
24
4
天国へ行く道、地獄へ行く道
z
２つの扉
z
z
z
z
z
z
z
z
z
天国へ行く道への扉か、
地獄へ行く道につながる扉
見た目では区別できない
z
「左の扉が天国行きですか？」
正しいとき
z
z
１人の人に質問できる
z
z
天国へ行く道、地獄へ行く道
z
何でも知っている
天使か悪魔
天使はいつでも真実を言う
悪魔はいつでも嘘をつく
正しくないとき
z
z
z
z
z
天使なら「ＮＯ」
悪魔なら「ＹＥＳ」
回答がＹＥＳであったとしよう
z
質問は YES / NO で回答で
きるもの１つだけ
どのような質問をすれば、左右
のどちらの扉が天国への扉か
を知ることができるか？
天使なら「ＹＥＳ」
悪魔なら「ＮＯ」
｢この人が天使で、かつ、左が
天国」か｢この人が悪魔で、右
が天国」のどちらかである
どちらであるかはわからない
失敗
25
天国へ行く道、地獄へ行く道
z
z
z
z
z
26
条件を整理して記述してみよう
「あなたは天使ですか？」
天使なら「ＹＥＳ」
悪魔なら「ＹＥＳ」
回答は常にＹＥＳ
失敗
z
扉についての条件
z
z
z
天使・悪魔についての条件
z
z
z
z
z
ＬＥＦＴ...「左の扉が天国への扉である」ことを意味
「ＬＥＦＴ」か「ＬＥＦＴでない」かいずれかが成立する
〇Ａ...「質問Ａにその人が ＹＥＳ と答える」
天使なら「どんなＡに対しても (Ａ ⇔ 〇Ａ)」
悪魔なら「どんなＡに対しても (Ａ ⇔ （〇Ａでない）)」
天使か悪魔のいずれか一方のみ成立
問題： ＬＥＦＴ ⇔ 〇B となる質問Bは何か？
27
z
z
天国と地獄の解答
記号論理による形式化
条件
z
形式化は問題を解くのに不可欠か？
z
ＬＥＦＴ または ＬＥＦＴでない
z
z
「任意のＡに対して(Ａ⇔〇Ａ)」
または 「任意のＡに対して(Ａ⇔（〇Ａでない）)」
z
問題
z
z
28
ＬＥＦＴ⇔〇B となるＢはなにか？
Bとして○ＬＥＦＴをとればよい
z
z
z
天使なら LEFT⇔○LEFT かつ ○LEFT⇔○○LEFT
悪魔なら LEFT⇔（○LEFTでない） かつ
○LEFT⇔(○○LEFTでない）
「あなたは、左の扉は天国への道ですか、と聞かれたらYESと答え
29
ますか？」
z
ＮＯ
同じことを頭の中で(非形式的に）考えることもできる
形式化は問題を解くのに役に立ったか？
z
z
z
ＹＥＳ
問題の条件を整理することができた
解ける問題かどうかが客観的に判定できるようになっ
た
z
z
解の候補を系統的に調べることができる
解のない問題である場合には、そのことが示せる
30
5
形式化ということ
z
z
z
記号列に対する機械的な操作で定義にあてはまるか
どうかのチェックができる。
z
まとめ
z
形式的体系の必要性
z
z
今週はここまで
形式的定義
z
誰が見ても正しいかどうかが判定できなければ厳密
な推論はできない
z
形式的体系を使うメリット
z
z
推論自体が正しいかどうかコンピュータでチェックでき
る
場合によってはコンピュータにより自動的に推論がで
きる
31
ソフトウェアの信頼性向上は、社会的に重大な関心
事となりつつある
ソフトウェアの正しさを保証するためには、仕様を形
式的に記述することが必要である
形式仕様の記述とソフトウェアの正しさの保証には、
形式的体系(形式論理）を使う。
32
6