形式手法

科目基礎情報

学校	大分工業高等専門学校	開講年度	令和05年度 (2023年度)
授業科目	形式手法
科目番号	R05AES208	科目区分	専門 / 選択
授業形態	授業	単位の種別と単位数	学修単位: 2
開設学科	専攻科電気電子情報工学専攻	対象学年	専2
開設期	前期	週時間数	前期:2
教科書/教材	“ソフトウェアの基礎” Benjamin C. Pierce他（インターネット上で公開されている書籍を参照する）
担当教員	西村 俊二

到達目標

(1) 型システムに基づいた証明支援システムによるプログラミング言語の動作保証の原理を理解し，説明することができる．（定期試験）
(2) 証明支援システムにより動作が保証されたプログラムを記述することができる．（レポート）

ルーブリック

	理想的な到達レベルの目安	標準的な到達レベルの目安	未到達レベルの目安
到達目標(1)の評価指標	型システムによる論理記述とプログラミングの関係について，一般論として説明できる	特定の例については型システムによる論理記述とプログラミングの関係を説明できる	型システムによる論理記述とプログラミングの関係が説明できない
到達目標(2)の評価指標	証明支援システムを使って高度なプログラミングができる	証明支援システムを使って簡単なプログラミングができる	証明支援システムを使ったプログラミングができない

学科の到達目標項目との関係

学習・教育目標 (E1) （専門工学の知識を獲得する）

JABEE 1.2(d)(1) （分野別要件－専門工学（工学（融合複合・新領域）における専門工学の内容は申請高等教育機関が規定するものとする）の知識と能力）

教育方法等

概要:

形式手法はコンピュータ・システムの開発に用いられる手法で，数理論理学に基づいた記述言語を使って求められる動作を表現することにより，設計の上流工程の効率化や網羅的な検証を可能にするものである．本講義では，具体的なツールとして証明支援システムCoqを用い，型システムによりある種の動作が保証されたプログラミングを実践する．

授業の進め方・方法:

インターネット上で公開されている書籍 “Software Foundations” (by Benjamin Pierce et al.) とその邦訳（“ソフトウェアの基礎”として公開されている）を中心として進め，区切り毎に内容のまとめや確認問題を行う．
（事前学習）
授業後に公前される講義資料を用いて前回までの内容を復習しておくこと．

注意点:

（履修上の注意）
授業中にコードを書く時間を設ける場合があるため，可能な限りPCを持ち込んで受講されたい．
（自学上の注意）
講義資料及び確認問題をwebサイト等で公開するので復習に活用されたい．

評価

（総合評価）
総合評価＝ 定期試験の平均点 x 0.8 + レポート x 0.2
（単位修得の条件）
総合評価60点以上かつ課せられた全レポート課題のうち60%以上を提出していること．
（再試験について）
定期試験を受けた上で60 点に満たない者に対して一度だけ再試験を実施する．

授業の属性・履修上の区分

アクティブラーニング

ICT 利用

遠隔授業対応

授業計画

		週	授業内容	週ごとの到達目標
前期
	1stQ
		1週	概要とCoqの紹介	授業の導入として，以下の項目に沿って学ぶ： 科目の既要 / Coqについて / 列挙型の記述
		2週	関数プログラミングとプログラムの証明 (1/2)	以下の項目に沿って学ぶ： introsタクティック / 書き換え（Rewriting）による証明 / Case分析 / Caseへのネーミング
		3週	関数プログラミングとプログラムの証明 (2/2)	以下の項目に沿って学ぶ： 帰納法 / 形式的証明と非形式的証明 / 証明の中で行う証明
		4週	直積、リスト、オプション (1/3)	以下の項目に沿って学ぶ： 数のペア / 数のリスト
		5週	直積、リスト、オプション (2/3)	以下の項目に沿って学ぶ： リストを使ったバッグ / リストに関する推論 / お小言 / リスト上の帰納法 / SearchAbout
		6週	直積、リスト、オプション (3/3)	以下の項目に沿って学ぶ： オプション / applyタクティック / 帰納法の仮定を変更する
		7週	多相性と高階関数 (1/3)	ポリモルフィズム（多相性）について理解する
		8週	多相性と高階関数 (2/3)	データとしての関数について理解する
	2ndQ
		9週	多相性と高階関数 (3/3)	さらに高度なCoqタクティックについて学ぶ
		10週	命題と根拠 (1/3)	命題によるプログラミングとその根拠について理解する
		11週	命題と根拠 (2/3)	帰納法の仮定や帰納的定義について，より深く理解する
		12週	命題と根拠 (3/3)	CoqのTypeとPropについて理解する
		13週	Coqにおける論理 (1/2)	Coqにおける全称記号や，真と偽，否定の概念について理解する
		14週	Coqにおける論理 (2/2)	Coqにおける存在量化子や，同値性の扱い方について理解する
		15週	前期末試験	到達目標(1)(2)
		16週	前期末試験の解答と解説

評価割合

	試験	レポート	合計
総合評価割合	80	20	100
専門的能力	80	20	100