|
授業科目名
|
担当教員
|
|||||||||||||||||||||
|
論理と形式手法
|
岩沼 宏治
|
|||||||||||||||||||||
|
時間割番号
|
単位数
|
コース
|
履修年次
|
期別
|
曜日
|
時限
|
||||||||||||||||
| 263136 | 2 | CS | 3 | 前期 | 火 | II | ||||||||||||||||
| ［概要］ | ||||||||||||||||||||||
| 数理論理や数理科学に基づく，プログラムやハードウエアの仕様記述，開発と検証法に関する理論と技術について学ぶ。極めて高い信頼性を必要とする大規模システム（例えば CPU LSIなど）を開発する際の基礎をなす技術である．具体的には，情報処理学会J07-CSの「離散構造」及びJ07-SEの「論理と計算理論」ならびに「形式手法」の項目に準拠し、その一部を取り上げる． | ||||||||||||||||||||||
| ［具体的な達成目標］ | ||||||||||||||||||||||
| 1. 形式的手法の基盤となる数理論理やモデル検査などの数理科学の基礎について学ぶ。<BR>2. Floyd-Hoare論理や有限状態モデルなどに基づくシステムの正当性検証に関する基本について学ぶ．<BR>3. データベースシステムなどの実例を通して，形式的仕様記述の実際を学ぶ<BR>4. VDM やZ などの形式的な仕様記述検証のためのツールの実際について理解する． | ||||||||||||||||||||||
| ［必要知識・準備］ | ||||||||||||||||||||||
| 離散数学（集合，順序，関係など），線形代数，アルゴリズムとデータ構造，プログラミング | ||||||||||||||||||||||
| ［評価方法・評価基準］ | ||||||||||||||||||||||
|
||||||||||||||||||||||
| ［教科書］ | ||||||||||||||||||||||
| ［参考書］ | ||||||||||||||||||||||
| (未登録) | ||||||||||||||||||||||
| ［講義項目］ | ||||||||||||||||||||||
| 第1回 命題論理と述語論理<BR>第2回 命題論理の意味と決定手続き<BR>第3回 SATソルバーと制約充足ソルバー<BR>第4回 述語論理の意味と形式推論体系<BR>第5回 形式体系上の証明： 自然演繹法、導出原理<BR>第6回 中間評価（総括とまとめ）<BR>第7回 正当性検証：プログラムの正しさ，事後条件、帰納表明<BR>第8回 正当性検証：部分的正当性，停止性証明<BR>第9回 プログラム検証論理：Floyd-Hoare論理，配列要素と代入文の公理 <BR>第10回 プログラムの形式的仕様記述： <BR>第11回 VDMによる仕様記述：<BR>第12回 仕様記述の実例：データベース<BR>第13回 仕様記述の実例：状態遷移マシン（自動販売機）<BR>第14回 演習<BR>第15回 総合評価（総括とまとめ） | ||||||||||||||||||||||
| ［教育方法］ | ||||||||||||||||||||||
| 個本的に講義形式の教育を行い，部分的に演習を行う．全ての講義資料をPowerPointを利用して電子的に作成し，ホームページから配布する予定だる．<BR>• 適宜，自主勉強用の演習問題プリントを配布する．<BR>• 中間試験の答案用紙の採点結果を返却する予定である．これにより自己の実力の確認を行なってもらいたい． | ||||||||||||||||||||||
| ［JABEEプログラムの学習・教育目標との対応］ | ||||||||||||||||||||||
| (未登録) | ||||||||||||||||||||||
| ［その他］ | ||||||||||||||||||||||
| オフィスアワー：月曜４時限目 | ||||||||||||||||||||||