情報科学概論 ー論理とソフトウェアー 亀山 幸義 [email protected] 2002.04.19 今日のキーワード ソフトウェア科学 信頼性 論理パズル 形式化 システム検証 情報システム 社会の多種多様な場面で（しばしば、無意識 のうちに）使われている； 現代社会にとって 不可欠 単なる技術から、法律・経済・文化や社会風 俗にいたるまで影響を受ける 情報システムの中心はソフトウェア ソフトウェア科学 ソフトウェアそのものを対象とする学問；情報科学の 中心的話題 ソフトウェアの目指す方向性 高機能、高性能であること 使いやすいこと 安定していること、高い信頼性をもつこと 現在のソフトウェア・社会システムの弱点：信頼性 みずほ銀行 スペースシャトル：打ち上げ直前に延期 Y2K問題 （情報）システムの信頼性 システムが常に「意図した通りの動作」をする こと 仕様 (Specification) システム検証：システム（の記述：プログラム） が仕様を満たしていることを証明する システム検証に必要なもの 仕様の記述言語 形式的な記述が必要！ システムの記述言語 推論のための論理体系 （＋自動推論のための ソフトウェア etc.) 参考：システムの信頼性向上の技法 完全な検証ではなく、信頼性をある程度向上 させる技術；１００％の正しさではなく、許され るコストの範囲内で信頼性を高める技術 例：仕様を形式的に記述する（検証はしない） 早い段階でバグをとることができる(工学的に有 効） 形式化ということ 天国への扉、地獄への扉 天国、地獄（続き） 扉の先の道は以下のいずれか 天国への扉の前には天使がいる 天使はいつでも本当のことを言う 地獄への扉の前には悪魔がいる 天国へ通じる扉、地獄へ通じる扉 悪魔はいつでも嘘をつく 質問は YES/NO で回答できるもの１つ⇒ど のような質問をすべきか？ 天国と地獄の答 絶対正しいことを質問すればよい。 これは扉ですか？ 天使なら ＹＥＳ と答える ⇒天国への扉 悪魔なら ＮＯ と答える ⇒地獄への扉 天国への扉、地獄への扉ー２ 天国、地獄－２（続き） 扉の先の道は、天国か地獄か 中央に１人だけいる その人は天使か悪魔のいずれか 質問は YES/NO で回答できるもの１つ⇒ど のような質問をすべきか？ 定義可能な自然数 日本語（数字、四則演算、空白を含む）で一 意的に定義できる自然数 １００＋３００＊２ ９９９９９９９９９９ 富士山の高さ（メートル単位） １モル（の数） ｘｘの瞬間に宇宙にある分子数 定義可能な自然数（続き） 最大のものは？ いくらでも大きな自然数を定義可能 ｎ文字で定義可能な最大の自然数は？ 有限個（高々、数千、数万）の文字を、ｎ文字並べ てできる文字列は、有限個 そのうち自然数を定義しているものは有限個 最大が存在するはず 定義可能な自然数（続き） ｎ文字で定義可能な自 然数のうち、最大のも のが存在する 定義可能な自然数（続き） 「２６文字以内で定義可能な最大の 自然数」をNとする 「２６文字以内で定義可能な最大の 自然数に１を足したもの」をMとする ⇒ Ｍ＝Ｎ＋1 かつ N≧M レポート出題 のパズル 先生は、以下のいずれか１つの日に出題 する ５月１日、２日、３日、４日、５日 学生には事前に出題日はわからない 上記の条件を満たすとき、先生はいつ出 題するだろうか？ レポート出題（続き） ５日に出題できるはずがない ４日に出題できるはずがない ４日までに出題されなければ、５日に出題することがわかってし まう ３日までに出題されなければ、上の推論により５日にも出題で きないので、４日に出題されることがわかってしまう これを続けたら、どの日にも出題できるはずがない と思って安心していたら突然（たとえば５月４日に)出題 されてしまった。先生は嘘をついていない。どこがおかし かったのか？ 形式化（記号化）ー天国と地獄 ＬＥＦＴ 左の扉が、天国への扉 ＲＩＧＨＴ 右の扉が、天国への扉 ＬＥＦＴ ∨ ＲＩＧＨＴ ～（ＬＥＦＴ Λ ＲＩＧＨＴ） 〇Ａ 質問Ａにその人が ＹＥＳ と答える 「任意のＡに対して Ａ ⇔ 〇Ａ」かまたは 「任意のＡに対して Ａ ⇔ ～〇Ａ」のいずれか 一方のみ成立 問題： ＬＥＦＴ ⇔ 〇B となるBは？ 形式化（記号化）ー天国と地獄 Bとして○ＬＥＦＴをとればよい 「任意のＡに対して Ａ ⇔ 〇Ａ」の場合でも、 「任意のＡに対して Ａ ⇔ ～〇Ａ」の場合でも、 ○B⇔LEFT が成立する Bとして○LEFTをとるということは 「あなたは、この扉は天国への道ですか、と聞か れたらYESと答えますか？」と質問する、というこ と 形式化（記号化）ー天国と地獄 記号化は問題を解くのに不可欠か？ ＮＯ 記号化は問題を解くのに役に立ったか？ ＹＥＳ 問題の条件を整理することができた 解ける問題かどうかが客観的に判定できるように なった 形式化ということ 厳密な定義 記号列の上の機械的な操作を仮定して、 種々の概念の定義を与える。 誰が見ても正しい推論(あるいは計算規則）を 与える ⇒正しいかどうか計算機がチェックできる！ 例 数 ０は数である Ｎが数ならば、ｓ（Ｎ）は数である Ｍ，Ｎが数ならば、（Ｍ＋Ｎ）は数である Ｍ，Ｎが数ならば、（Ｍ＊Ｎ）は数である 帰納的な定義の例 例 数の形式的体系 推論に関する規則 等号に関する規則（Ｎ＝Ｎなど） ～（０＝ｓ（Ｎ）） ｓ（Ｎ）＝ｓ（Ｍ） ⊃ Ｎ＝Ｍ 数学的帰納法 足し算や掛け算に関する公理 Ｍ＋０＝Ｍ Ｍ＋ｓ（Ｎ）＝ｓ（Ｍ＋Ｎ） レポート出題のパズル 自分で考えてみてください システム検証の技法 自動的な方法 モデル検査 抽象実行 半自動的な方法(対話的な方法；人間が介在 する方法） 演繹による定理証明 具体例 モデル検査の技法によるシステム検証の具 体的な例（web page 版資料では具体例は削 除します） おわりに ソフトウェア作成(プログラミング）に論理的思 考は不可欠 ソフトウェア検証に形式論理は(不可欠とは限 らないが）非常に有用
© Copyright 2024 ExpyDoc
![移住者居住支援事業フロー図[PDF：378KB]](http://s1.expydoc.com/store/data/005897320_1-2fa095f0265cc835e40fe0a2cb701055-250x500.png)
