授業科目
Course Title

ソフトウェア基礎
Basic of Computer Software

担当者
Instructor

教授   木下 佳樹
後 金1

単位
Credit

2

関連するディプロマポリシー
Related Diploma Policy

時代の課題と社会の要請に応えた専門的知識と技能/Expert knowledge and skills to address the issues of the age and the demands of society

到達目標
Target to be Reached

入力出力型プログラムが仕様を満たすことを証明するために必要な数理科学的な枠組を理解し、使えるようになること。

授業内容
Course Content

本科目では、プログラムが意図通り動くことを表現するため、ホア論理のモデルを集合と部分写像を用いて示す。また、意図通り動くことを
  事前条件が成り立つ時にプログラムを実行して停止したとすると実行後に事後条件が成り立つ
あるいは
  事前条件が成り立つ時にプログラムを実行すると必ず停止してしかも実行後に事後条件が成り立つ
ことと捉え、プログラムの正しさを導き出すホアの論理によるプログラムの正当性証明 (プログラムが意図通りに動くことの証明) を取り扱う。

以下の項目について講義する。
1) 集合と部分写像の基本的性質。
2) プログラムが仕様通りに動くことを集合と部分写像によって数学的に説明
するモデル。
3) 2) のモデルに基づいてプログラムが仕様通りに動くことを証明するための
ホア論理 (Hoare logic)。

授業計画
Course Planning

1. 集合と部分写像 I。序論。プログラムの「正しさ」とは? なぜ正しさの証明をするか?集合。集合の帰納的定義。whileプログラムの集合。
2. 集合と部分写像 II。二項関係の一価性、全域性、単射性、全射性。写像と部分写像。部分写像の合成と逐次合成。全射と単射。空集合。一点集合。
3. 集合と部分写像 III。直積集合、冪集合、直和集合とif文。
4. 総合演習 I。
5. 集合と部分写像 IV。集合の帰納的極限とwhile文。
6. 集合と部分写像 V。プログラムの部分写像によるモデル。
7. ホア論理 I。部分正当性規則 I (代入文規則、逐次連接文規則、事前条件強化、事後条件弱化)
8. ホア論理 II。部分正当性規則 II (累積代入文規則、多重逐次連接文規則、while文規則)
9. ホア論理 III。部分正当性規則 III (if文規則、skip文規則、abort文規則、連言規則、選言規則、安定性)
10. 総合演習 II。
11. ホア論理 IV。全正当性規則 (while文全正当性、安定性全正当性)
12. ホア論理 V。プログラムと正当性証明の並行構築。高速冪乗計算。
13. ホア論理 VI。配列の規則
14. ホア論理 VII。正当性証明の演習。二分探索算法の正当性証明。

授業運営
Course Management

時間外学習について。本科目は2単位なので、修得のための学習時間は総計90時間である。教室での講義時間100分×14=23時間20分を除くと66時間40分の時間外学習が求められる。この時間はもっぱら復習と課題解答作成のために費やされることが想定されている。復習は講義内容を正確に理解し、記憶することが基本である。さらに理解を確実にするために、講義の内容を変えてみてその結果を考えて見ることが薦められる。講義に用いられたプログラムコードや、言葉(概念)の定義をを少し変えて、その結果を考えるのである。また、講義中に課される課題解答を試みること。解答ので理解の不十分なところがわかり、復習につなげることができる。

受講者は、以下の技能を有することを前提とする。

1) 「プログラミングI」修得済みあるいは同等の技能を有すること。とくにプログラミング言語の代入文、逐次連接文、分岐文、繰り返し文などの言語構造に関する直感的理解を有すること。
2) 「離散数学I」を修得済みあるいは同等の技能を有すること。とくに集合(とくに直積集合)、二項関係(とくに同値関係、半順序関係)、写像(とくに合成、単射、全射、添数付集合族)などに関する基本的知識を有すること。

本科目では教科書を用いず、講義ノートを講義支援システム(dotCampusあるいは同等のもの)を通じて配布する。講義ノート閲覧のために受講者はノートブックコンピュータを講義に携行する必要がある。(情報科学科学生に貸与されているもので十分である。情報科学科以外の受講者で、必要な者には貸与する。)

適宜、演習課題を与えて講義支援システムを用いて提出させる。

評価方法
Evaluation Method

総合演習の結果、提出物、演習での発表状況などを総合して評価する。

オフィスアワー
Office Hour (s)

木曜日11:00-12:30、2-226(変更ある場合には講義などで通知する。
なお、これ以外の時刻でもメイルなどで面談の約束を受け付けるので、積極的な質問や相談を歓迎する。

参考書
Book (s) for Reference

C.A.R Hoare,An axiomatic Basis for Computer Programming,ACM,(https://dl.acm.org/citation.cfm?id=363259),1969
John Reynolds,Theories of Programming Languages,Cambridge University Press,1998

Copyright© 2017 Kanagawa University. All Rights Reserved.