プログラム理論   [ GB21101 ] Program Theory
対象：3・4学年	開設学期：春AB	曜日・時限：火5・6	単位数：2単位
担当教員：水谷哲也

概要

　逐次プログラムの意味，プログラムの目的の表 明，仕様の表現，停 止性，正当性の検証方法を述べるとともに，並行実時間 プログラムの仕様 表現，正当性の検証体系について紹介する．

学習・教育目標

1. プログラムの意味・要求仕様の表現について理 解する (第1週)
2. Hoare理論による手続き型プログラムの正当性検 証の仕組みを理解する (第2〜7週)
3. 最弱前条件に基づく検証理論 を理解する (第8〜9週)
4. 並行実時間プログラムの検証の基礎を理解 する (第10週)

キーワード

プログラムの意味，仕様，停止性，検証，ホーア論理

Keywords

Semantics, Specification, Termination and Verification of Programs, Hoare Logic

時間割

週	講義内容/理解すべき項目
第1週	プログラムの意味，要求仕様表現と検証
第2- 6週	Hoare論理による逐次プログラムの検証；停止性を含む 正当性
第7週	配列・手続き等の理論的取扱い
第8- 9週	ダイクストラの最弱前条件に基づくプログラム検証
第10週	時相論理及びν理論を用いた並行実時間プログラムの仕様表現およびその検証

教材

授業中にプリント等を適宜配布する．

参考書籍

林晋：プログラム検証論，共立出版，1995.

Z. Manna: Mathematical Theory of Computation,McGraw-Hill, 1974. 
(日本語訳 五十嵐滋訳: プログラム の理論, 日本コンピュータ協会,1974.) 

予備知識・前提条件

　論理と形式化の授業を履修していることが前提条件．

成績評価

　期末試験(50%)，演習及びレポート(50%)により，出席状況を加味して評価する．

教員メールアドレス

水谷哲也：mizutani ＠ cs.tsukuba.ac.jp

オフィスアワー

木5限 3F708(水谷)