ソフトウェア科学入門 - Programming Logic Group

情報化社会
情報科学概論Ⅰ
ソフトウェア科学入門
z
コンピュータの進歩は日進月歩
z
ハードウェアの進歩
z
ドッグイヤー
ムーアの法則
様々な新しい情報機器の登場
z 家電の情報化
z 10年先どころか5年先も予想が難しい
情報化社会の鍵は？
z ソフトウェア
z
z
亀山 幸義
http://logic.cs.tsukuba.ac.jp/~kam
z
z
z
z
ソフトウェアの高機能化、高性能化、使いやすさの向上
あらゆる機器が情報化（知能化）される
情報化社会の弱点は？
z ソフトウェア
1
ソフトウェアがひきおこした
社会問題
z
2
インターネットを通じたソフトウェアの取得
枚挙に暇がない
z
z
z
z
z
z
z
Y2K(西暦２０００年）問題
スペースシャトルの打上げ延期
銀行のオンラインシステム（ATM）のダウン
航空券の発券システムのダウン
携帯電話のたび重なる回収
Windowsシステムを狙ったウィルス
株取引の誤発注
インターネットで見つけたソフトウェアを使ったら、
自分のコンピュータがフリーズした。
3
ソフトウェア科学入門
「プログラムの論理」講義予定
ソフトウェア科学とは
z
ソフトウェアに対する2つの立場
z
z
z
z
z
アルゴリズム、ソフトウェア実装方式の研究
ソフトウェア検証、情報セキュリティの研究
仕様と正しさ
ソフトウェアの検証
3. プログラミング・パラダイム
ユーザインタフェースの研究
z
安定して、高い信頼性をもつソフトウェアの構成法
z
ソフトウェア作法
構造化プログラミング
ソフトウェアの正しさ
z
使いやすいソフトウェアの構成法
z
z
2.
高機能・高性能ソフトウェアの構成法
z
z
ソフトウェアの作り方に関する研究⇒ソフトウェア科学
ソフトウェア科学の目指すもの
z
動けばいいプログラムから良いプログラムへ
1.
ソフトウェアを作成し利用して、対象領域の問題を解く
ソフトウェア自身を研究対象とする
z
z
4
5
様々なプログラミング・スタイル
6
1
「普通」のプログラミング教育
「動けばいいプログラム」から
「良いプログラム」へ
z
習うこと
z
z
z
z
プログラム言語の構文、制御構造、データ構造
いろいろなアルゴリズム
とにかく指定された計算をするプログラムを書く技
あまり習わないこと
z
z
同じ問題を解くのにも、良いプログラムと悪いプログラ
ムがあること
良いプログラム、美しいプログラムを書く技
7
8
大昔に開発されたプログラムの一部
笑い話 ではない
[プログラミング作法より引用]
/* 国がシンガポールかブルネイか
ポーランドなら、現在の時間はオフフック時ではなく
応答時。。。
*/
、、、
}
z
携帯電話機の大量回収騒ぎの原因と噂されて
いる
9
プログラムには、
『良い』書き方がある！
良いプログラムとは？
z
「良いプログラム」のいろいろな定義
z
z
z
z
z
z
10
z
書けばいいってものではない
動けばいいってものでもない
z
どうすればよいか？
z
プログラムがしやすい。簡単に書ける。
実行速度が速い、実行時のメモリ使用量が少ない。
バグを見つけやすい
変更がしやすく拡張性に富む。
（ライバル会社にとって）わかりにくい。
定義1：読みやすいプログラムが良いプログラムである。
z
読みやすい＝プログラムの動作が、プログラマ本人以外の人
にとって理解しやすい
11
12
2
参考図書
プログラミング・スタイルの第一歩
「プログラミング作法」
変数名や関数名のつけかた
z グローバルにはわかりやすい名前を、ローカル
には短い名前を
B. W. Kernighan, R. Pike著 福崎訳
アスキー、2000年
原題は “Practice of Programming”
Kernighan & Pike, Addison-Wesley,
1999.
ｃｆ. ｢ソフトウェア作法」
Kernighan, Planger, 共立出版、１９７６
13
z
統一しよう
z
z
式と文
z プログラムの構造がわかるようにインデント（段
付け）しよう プログラムを美しく書こう！
関連のあるものには関連ある名前をつけよう
関数には能動的な名前を
z
z
14
ただし、真偽値を返す関数は戻り値を明確に表す名
前を
名前は的確に
z
間違った名前をつけるとバグの原因となる
15
z
自然な形の式を使おう
z
z
16
z
複雑な式は分解しよう
z
明快に書こう
z
副作用に注意
自分で音読するつもりで書こう。
かっこを使って、あいまいさを解消しよう。
17
18
3
コメント
z
その他（一般原則）
z
当たり前のことをコメントとして書くな
z
z
z
z
z
ちょっとした効率化より、読みやすさを重視せよ。
効率化は後ですればよい。
関数やグローバル変数には、コメントを書け
悪いプログラムにコメントを書くな。書き直せ。
コードと矛盾させるな。
19
20
プログラミング作法の効用
z
スタイルを守って書かれたプログラムは
z 読みやすく、理解しやすい
z プログラムのサイズも小さい
z
ソフトウェアの寿命
z
プログラミング作法の先へ
z
z
定義1：読みやすいプログラムが良いプログラム。
このプログラムはあと数年しか使わないと思っていても、その前提はく
つがえる。（cf 西暦2000年問題）
z
プログラミング・スタイルは自習できる
z
一度習得すれば、その後はほとんど時間はいらない
コード規約
z 多くのソフトウェア開発部隊（企業など）では、ある一定のパターンに従っ
てプログラミングをしなければいけない、という規約を定めている。
z
z
z
z
プログラミング作法だけで良いプログラムが書け
るか？
Edsger Dijkstra の定義
z
定義２：正しさを示しやすいプログラムが良いプログラ
ムである。
例： if 文のテスト部では、＝による代入は使わない。
「動きさえすればよいプログラム」では、製品として認められない。
21
構造化されていないプログラムと
構造化プログラム
構造化プログラミング
z
構造化プログラミング
“Structured Programming”
by Dahl, Dijkstra, Hoare, 1972.
z
プログラミング言語論、プログラミング方法論の
源流
プログラムの構造化
データ構造化
階層的プログラミング
22
機械語(アセンブラ）のプログラム
のよう！
23
24
4
C言語で書いたプログラム
このプログラム（関数）は、
正しいだろうか？
「foo (x, y) は整数xを整数y
で割った商である」
正しいプログラムとは
NO!
foo (3, -2) の計算は止まら
ない
25
正しいソフトウェア（プログラム）とは
C言語で書いたプログラム
仕様
26
では、このプログラムは｢正しく
ない」のだろうか？
ＮＯ！
「どんな整数 x と ｙ に対しても
foo (x, y) は x を ｙ で割っ
た商」は誤り
「どんな正の整数 x と ｙ に対
しても foo(x, y) は x を ｙ
で割った商」は正しい
z
z
z
プログラムだけをもってきて、正しいかどうかを判定する
ことはできない。
プログラムと（きちんとした）仕様が与えられれば、正し
いかどうかを判定することができる。
プログラムの仕様 (Specification)
プログラムに関する何らかの性質（成立することが期待される
性質）
例. 「正の整数 x を正の整数 y で割った商を返す」
参考. パソコンの「スペック」とは少し違う
Pentium 2GHz, Memory 512MB, etc.
z
27
プログラムの検証
z
28
プログラム検証に対する２大要求
プログラムが仕様に関して正しいことを厳密に保
証（証明）すること
z
厳密であること
「おおむね正しい」ことには意味がない
例：９９％の入力値に対して正しく動作するプログラムは、
１ページに数十か所の誤植がある文章と同じ
z
z
できる限り自動的（機械的）であること
z
z
29
プログラムは次々と生産される
１０年しか使われないプログラムの検証に１０年を要
していたら…
30
5
形式仕様 (formal specification)
z
z
ソフトウェアの開発過程
（x=y*d+r)∧...
形式仕様：
形式言語（論理式）を使って記述した仕様
プログラム ｄ = foo(x,y) の仕様は？
z
z
z
形式仕様
入力(input) は、正の整数 x と y
出力(output)は、０以上の整数 d
x, y, d の関係（入出力関係）を論理式で書く
Verification
要求
Validation
x = y×d + r
(x = y×d + r) ∧ (0 ≦ r < y)
∀x>0.∀y>0.∃d.∃r.
((x = y×d + r) ∧ (0 ≦ r < y))
プログラム
『割り算のプログ
ラムが欲しい』
int foo (int x, …) { … }
31
32
ソフトウェアへの信頼性向上への道
z
z
テストと検証は違う
z
テスト: いくつかのテストデータを入力して出力を
z
調べる
検証: どんな入力に対しても、ソフトウェアが与えら
れた仕様を満たすこと（正しいこと）を保証する
プログラムの検証
比較
z
z
z
｢信頼性｣に関しては｢検証」アプローチが優れている
｢コスト｣については「テスト｣アプローチが優れている
ソフトウェアの信頼性に対する要求が高まるにつれ、
｢検証｣アプローチの比重が少しずつ高まっている
33
w=x;
z=0;
34
仕様Ｓ１:
どんな正の整数x,yに対しても
ある整数 r に対して、
NO
x = y×foo(x,y)＋r
かつ 0≦r＜ y
w>=y ?
YES
仕様Ｓ２：
Ａにおいてx＞０,y＞０ ならば
Ｅにおいて
z=z+1;
w=w-y;
x = y×z＋w かつ 0≦w＜ y
return z;
35
実は、Ｓ２からＳ１はいえない
(このことは、とりあえず、無視）
36
6
まずは素朴に…
発想を変えて
A: x>0, y>0
B: x>0, y>0, w=x, z=0
(1) もし、x<y ならば
whileループを実行しているときに
変わらない性質を考えてみよう。
E: x>0, y>0, w=x, z=0, x<y OK
ループを１回まわるごとに z が 1
増えて, w が y 減っている
⇒ z×y + w の値は変わらない
(2) もし、x≧y ならば
C: x>0, y>0, w=x, z=0, w≧y
D: x>0, y>0, w=x-y, z=1
(2-1) もし x-y < y ならば
ループを何回まわろうが、常に、
z×y + w = x が成立
E: x>0, y>0, w=x-y, z=1, x-y<y
OK
(2-2) もし、x-y ≧ y ならば‥
終わらない!
（ループ不変条件）
37
38
A
w=x;
z=0;
発想を変えて（２）
B
仮説： プログラムの制御がB, C, D,
E にあるときは、いつでも、
YES
C
証明: 以下の場合に上式が成立する
かチェックすればよい
z
z
z
z
z
初めてBに到達したとき
BからCに到達したとき
CからDに到達したとき
DからBに到達したとき
BからEに到達したとき
z×y+w=x
が
A,B,C,D,E
で成立
NO
w>=y ?
x = z ×y + w が成立する
z=z+1;
w=w-y;
E
D
return z;
39
発想を変えて（３）
B, C, D, E では、いつでも、
z×y + w = x が成立する
さらに Eへ到達したら w < y である。
40
残る問題：停止性
z
z
以上の事から、
E では、必ず、
z×y + w = x かつ w < y
を導くことができた。
(仕様Ｓ２の検証終了）
なんと、A で x>0, ｙ>0という条件を使わ
41
ずに証明できた！（おかしい）
仕様Ｓ２：｢プログラムの制御がEに行くならば○○○が
満たされる」ことは証明できた。
「プログラムの制御がいつか必ずEに行く」保証は、まだ
得られていない。
z
z
z
whileループは必ず終了するとは限らない。
実際、仕様Ｓ２の証明では、y>0という条件を使わなかったが、
この条件を使わないと、ループが終了することはいえない。
言葉
z
z
｢停止するならば、正しい｣と言う性質を｢部分正当性」とよぶ。
停止性をこめた(本当の)正しさを、単に｢正当性｣とよぶ。強調し
て、｢全正当性」とよぶことがある。
42
7
停止性の証明
ここまでのまとめ
数学的帰納法を使う。
任意のx>0、y>0に対して、このプロ
グラムは停止する。
0<x<yのとき
z
Ｃ言語などで書かれたプログラムの検証
z
whileループに１度もはいらず、停止
x≧yのとき
z
whileループを１度まわるとw＝x－ｙ
x-y<x なので、帰納法の仮定より
foo(x-y,y)が停止する
そのことを使えば、whileループを１
度まわったあとの計算が停止す
ることがいえる。
結局、foo(x,y)の計算が停止する。
部分正当性
z
プログラムの流れ(コントロール・フロー）を追いかける
z
ループ不変条件を発見することが鍵
停止性
z
帰納法を使う
Hoare論理 [Hoare 1969]
手続き型プログラム言語を検証するための論理
現在でも、検証の基礎となっている。
以上より、どんなｘ＞０、ｙ＞０に対し
ても、foo(x,y)の計算は停止する。
43
次回の予告：
もっと検証しやすいプログラム言語は？
z
z
z
z
今日のまとめ
手続き型プログラム言語 (今回）
z
44
z
Ｃ言語、Ｊａｖａ言語など
プログラムは、代入文などを次々と実行していくという形式で記
述される。
実行の流れを理解する必要がある。
z
z
z
宣言型プログラム言語 (次回）
z
z
z
関数型プログラム言語：Lisp/Scheme, ML, Haskell など
論理型プログラム言語: Prolog など
z
z
z
わかりやすいプログラムが正しいプログラムにつながる
プログラムの仕様、正当性、検証
z
関数あるいは論理式としてプログラムが記述される。
プログラムの実行の流れに関係なく、プログラムの意味を理解
することができる。
z
ソフトウェア科学の重要課題の１つ：信頼性
信頼性の第一歩：｢良いプログラム｣を書くこと
正当性は、仕様とプログラムに対して決まる概念
検証はテストとは異なる
検証の方法
スローガン
z
良いプログラムとは正しさの保証がしやすいプログラム
45
46
講義資料・質問・問合せ
今後の予定
亀山のホームページ
http://logic.cs.tsukuba.ac.jp/~kam
この授業の資料
上記ページ→教育→２００６年度の授業
→情報科学概論１
質問等のあて先
kamのあとに＠cs.tsukuba.ac.jp
総合研究棟Ｂ １００８号室
次回から2週間は久野先生担当です。
数理計画法（アルゴリズムの話）
亀山担当の次回は、3週先の９月29日です。
その際に、レポート課題を出します。
47
48
8