|
プログラム理論特論_E
|
|
| Instructor(s) |
Tetsuya Mizutnai, Yukiyoshi Kameyama
|
| Mizutani: mizutani (AT) cs.tsukuba.ac.jp, Kameyama: kam (AT) cs.tsukuba.ac.jp | |
| URL | |
| Office hours | Office hours will be announced at the first lecture. |
| Cource# | 01CH213 |
| Area | Intelligent Software |
| Basic/Advanced | |
| Course style | Lecture |
| Term | Fall A |
| Period | Fri5,6 |
| Room# | 3B302 |
| Keywords | Symbolic Logic, Specification, Verification, Semantics, Hoare Logic, Guarded commands, Non-determinacy |
| Prerequisites | Familiarity with propositional/predicate calculi (logic) and fundamentals of programming languages will be helpful, though not necessary. |
| relation degree program competence | Knowledge Utilization Skills,Expert Knowledge |
| Goal | |
| Outline | Logic plays an important role in the study of software science. In this course, we study logic for specification and verification of programs. |
| Course plan |
1. Preliminaries: Introduction to the first order logic, formal syntax and semantics of logic, mathematics and programs. 2. Formal syntax and semantics of while programs, partial correctness of while programs by Hoare Logic. 3. Total correctness of while programs and soundness of Hoare Logic. 4. Completeness of Hoare Logic, Proof outline. 5. Formal specification and verification of nondeterministic systems with guarded commands. |
| Textbook |
Apt, K. R., de Boer, F. S. and, Olderog, E-R. : Verification of Sequential and Concurrent Programs, 3rd edition, Springer-Verlag, 2009. Class materials are distributed via manaba. |
| References |
M. Huth and M. Ryan, "Logic in Computer Science (Second Edition)", Cambridge Univ. Press, 2004. S. Hayashi, "Verification of Programs", Kyoritsu Shuppan Co., Ltd., 1995 (in Japanese). |
| Evaluation | Based on the scores of reports and in-class exercises, assuming that students attend all lectures. No examination. |
| TF / TA | |
| Misc. | Japanese Course. There will be no TA not TF. |