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