計算機ソフトウェア工学 / Computer Software Engineering

単位数: 2. 担当教員: 住井 英二郎. 開講年度: 2024. 科目ナンバリング: TEI-PRI308J.

メディア授業科目/Media Class Subjects

○

主要授業科目/Essential Subjects

○

授業の目的・概要及び達成方法等

Google Classroomのクラスコードは工学部Webページ
https://www.eng.tohoku.ac.jp/edu/syllabus-ug.html
（学部シラバス・時間割）にて確認すること。

授業にはGoogle Classroomを利用

１．目的
プログラミング言語の基本的な概念を理解する。
２．概要
プログラミング言語の構文論と意味論、プログラムの検証について述べる。
３．達成目標等
プログラミング言語の形式的な構文論と意味論、プログラムの検証、コンパイラの原理についての基本的な考え方を理解する。

授業の目的・概要及び達成方法等(Ｅ）

The class code for Google Classroom can be found on the Web site of the School of Engineering:
https://www.eng.tohoku.ac.jp/edu/syllabus-ug.html (JP Only)

Will use Google Classroom

1. Purpose
To understand fundamental concepts in programming languages.
2. Outline
Will describe syntax and semantics of programming languages, and program verification.
3. Goal
To understand the basic ideas on formal syntax and semantics of programming languages, program verification, and the principles of compilers.

他の授業科目との関連及び履修上の注意

「計算機学」および「プログラミング演習Ａ」の履修を前提としている。また、授業の理解を深めるためには、「オートマトン・言語理論」、「プログラミング演習Ｂ」、「コンパイラ」、「情報論理学」も履修することが望ましい。

他の授業科目との関連及び履修上の注意(Ｅ）

Prerequisite: 「計算機学 (Fundamentals of Computer)」 and 「プログラミング演習Ａ (Programming A)」 (or equivalent knowledge)
Recommended: 「オートマトン・言語理論 (Automata and Formal Languages)」, 「プログラミング演習Ｂ (Programming B)」, 「コンパイラ (Compiler)」, and 「情報論理学 (Logic for Computer Science)」

授業計画

１．序論（ソフトウェアの形式的検証）
２．論理式，集合
３．算術式の構文，帰納的定義
４．算術式の操作的意味論
５．プログラムの構文と操作的意味論
６．プログラムの仕様，表明
７．プログラムの正当性の証明
８．ループ不変条件とループ変動式
９．ホーア論理(1)
10．ホーア論理(2)
11．インタプリタとコンパイラ，スタックマシン
12．関数呼び出し，再帰
13．高階関数とλ計算
14．復習，試験
15．試験の解説

授業計画(Ｅ）

1. Introduction (formal verification of software)
2. Logical formulas, sets
3. Syntax of arithmetic expressions, inductive definitions
4. Operational semantics of arithmetic expressions
5. Syntax and operational semantics of programs
6. Specifications of programs, assertions
7. Correctness proofs of programs
8. Loop invariants and loop variants
9. Hoare logic (1)
10. Hoare logic (2)
11. Interpreter, compiler, and stack machine
12. Function calls, recursion
13. Higher-order functions and lambda-calculus
14. Review, exam
15. Review of exam

授業時間外学習

復習・予習、授業中に配布する課題・過去の試験問題等

授業時間外学習（Ｅ）

Preparation and review; problems and past exams distributed in class

成績評価方法及び基準

レポートと試験をもとに評価する。

成績評価方法及び基準(Ｅ）

Based on reports and exam

教科書および参考書

• プログラム意味論の基礎, 小林直樹・住井英二郎, サイエンス社 (2020) ISBN/ISSN: 9784781914831 資料種別:教科書/Textbook
• プログラミング言語の形式的意味論入門, Glynn Winskel原著、末永幸平監訳, 丸善出版 (2023) ISBN/ISSN: 9784621307632 資料種別:参考書
• プログラミング言語論, 大山口通夫、五味弘, コロナ社 (2008) ISBN/ISSN: 9784339027044 資料種別:参考書
• ソフトウェア工学の基礎知識, 白鳥則郎、高橋薫、神長裕明, 昭晃堂 ISBN/ISSN: 4785631031 資料種別:参考書

オフィスアワー

メールにより調整・決定する

オフィスアワー（Ｅ）

Appointment by e-mail