ソフトウェア構成論
Software Development Method
講義内容
ソフトウェアの仕様を厳密に記述し,それに基づいて高品質のソフトウェアを開発するために必要な,基本的な手法や考え方を説明する。仕様の段階的詳 細化を系統的に行ない,その正しさを保証するためには,仕様やプログラムの意味が形式的に定義されていることが重要である。そこで本授業ではまず,仕様記述法の例として,理論的整備の進んでいる代数的仕様記述法について説明する。また,代数的仕様の操作的意味を与える項書換え系についてやや詳しく述べる。さらに,関数型言語を仕様の部分クラスとして位置づけ,プログラム技法や実行方式について概説する。
1. 形式的仕様記述法
・定義と仕様記述例
・仕様の詳細化と検証
・始代数意味論
2. 項書換え系
・合流性
・停止性
・書換え戦略
3. 関数型言語
・プログラム例
・ラムダ計算
・実行方式
教科書
なし
参考書
授業中に紹介する
前提とする知識(必ずしも先修条件ではない)
アルゴリズムとデータ構造 ( アルゴリズム概論 )
形式言語理論,計算可能性 ( 計算理論 I )
一階述語論理 ( 人工知能基礎論 )