科目名	高度プログラミングA
単位数	1.0
担当者	情報工学専攻　准教授　川端英之
履修時期	前期（第1ターム）
履修対象	2年次
講義形態	講義
講義の目的	コンピュータに社会が支えられる今日，ソフトウェアの構成要素たるプログラムの品質への高い意識がプログラム開発者に求められるようになっている．プログラムの品質は，処理速度や要求資源量などの性能指標だけでなく，プログラムが意図通りの動作をすることの保証によって担保される必要がある．ここで，仕様検証の実施はもちろん，仕様検証に耐え得る高品質なプログラムの開発のためには，プログラミング言語に対する深い理解やプログラミング言語を客観的に数学的に捉える力が欠かせない．本授業では，受講者が，プログラミング言語の意味を数学的に論じるための考え方を理解し，プログラムの品質を形式的に論じるための基礎概念を獲得することを目的とする．
到達目標	・プログラムの仕様検証を論じるために必要な数学的な概念の基礎を理解し，プログラミング言語の構文や意味を数学的に定義する方法への理解を深め，議論できるようになること．【知識2】【技能1】【思考力・判断力】【表現力】 ・プログラムの仕様検証手法の考え方を理解し，具体的な理論の展開を追えるようになり，各手法の可能性や限界を意識できるようになること．【知識2】【技能1】【思考力・判断力】【表現力】
受講要件	・何らかのプログラミング言語を用いた経験があること．
履修取消の可否	可
履修取消不可の理由
事前・事後学修	・事前にテキストや配布資料を読み，前回の授業との関連性を確認し，トピックの全体像を把握すること． ・事後に十分な復習をし，不明点があれば迅速に担当教員に質問すること．
講義内容	１．数学的準備：論理式と集合，関係，関数 ２．プログラミング言語の構文：具象構文と抽象構文 ３．プログラミング言語の構文：構文の帰納的定義 ４．プログラミング言語の意味：評価規則と操作的意味論 ５．プログラムの性質に関する推論：プログラムの仕様の表明 ６．プログラムの性質に関する推論：正当性，ループ不変条件，ループ変動式 ７．ホーア論理：推論体系とその健全性，相対完全性 ８．ホーア論理：最弱事前条件，プログラムの半自動検証 ※授業の順序は変更することがある． ※試験期間に別途期末試験を実施する．
期末試験実施の有無	実施する
評価方法・基準	期末試験の得点70% 授業中の演習（小テスト等）の取り組みの程度30%
教科書等	教科書：小林直樹・住井英二郎著，プログラム意味論の基礎，サイエンス社，2020．
担当者プロフィール	情報工学を専攻．プログラミング言語処理系，高性能ライブラリ，プログラミング支援環境などに関する研究に従事． 研究室：情報科学部棟541号室． E-mail: kawabata@hiroshima-cu.ac.jp
講義に関連する実務経験
課題や試験に対するフィードバック	質問受付や返答，課題提示や講評等は，WebClass等の授業支援システムやメール等のオンラインコミュニケーションツールを用いて対応する． 質問等は随時受付．居室（情報科学部棟541号室）への訪問も随時受け付ける．
アクティブ・ラーニング	振り返り：授業中の演習（小テスト）による振り返りを行う．
キーワード	プログラミング言語，意味論，構文論，論理式，プログラムの仕様と正当性，ループ不変条件，ホーア論理，形式検証．
備考