プログラム理論

  [ GB21111 ]
Program Theory
対象:3・4学年 開設学期:春C 曜日・時限:水5・6 単位数:1単位
担当教員:水谷哲也

概要

プログラムの目的の表明, 仕様の表現, 逐次プログラムの意味, 正当性の検証体系, 停止性について紹介する.

学習・教育目標

  1. プログラム検証の基礎となる一階述語論理について概説するとともに,プログラムの意味・要求仕様の表現について理解する (第1週)
  2. Hoare理論による手続き型プログラムの正当性検証の仕組みを理解する (第2-4週)
  3. 発展的話題として,実時間並列プログラム系の検証方法について理解する(第5週)

キーワード

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

Keywords

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

時間割

講義内容/理解すべき項目
第1週 一階述語論理概説,プログラムの意味
第2週仕様表現と検証,Hoare論理概説
第3週Hoare論理によるプログラムの検証 部分的正当性と停止性の証明
第4週 Hoare論理における配列などの扱い
第5週 発展的話題:実時間並列プログラム系の検証

教材

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

参考書籍

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

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

予備知識・前提条件

 論理と形式化の授業を履修している,または数理論理学に関する基礎知識を持っていることが前提条件.

成績評価

 演習,レポートなどにより,出席状況を加味して総合的に評価する.

教員メールアドレス

水谷哲也:mizutani AT cs.tsukuba.ac.jp

オフィスアワー

木5限 3F708(水谷)

備考

平成27年度までに開設された「プログラム理論」(GB21101)の単位を修得した者の履修は認めない。