ソフトウェア基礎論
Foundations of Software Science

講義内容

ソフトウェアシステムを設計する際に大切なことは， まず対象を簡潔にモデ ル化し， 次に， 対象の性質を明らかにするための方法論をもつことである。
本講義では， データベース理論と形式的仕様記述法という二つの分野を取り 上げ， 重要な概念と方法論を紹介する。

  1. データベース理論
    データベースにおける質問言語に関する理論的な事柄を説明する。
    1. 関係代数， 関係論理
    2. 一階述語質問
    3. 再帰質問
    4. 否定を含む再帰質問
  2. ソフトウェアの形式的仕様記述法
    形式的仕様記述法の例として， 理論的整備の進んでいる代数的仕様記述法と， その操作的意味を与える項書換え系について説明する。
    1. 代数的仕様記述法
      • 始代数意味論
      • 仕様の記述・詳細化と形式的検証
      • プログラムへの変換が可能な部分クラス
    2. 項書換え系
      • 諸定義， 停止性， 合流性， Knuth-Bendixの完備化アルゴリズム
      • 項書換え系の部分クラスとしての関数型言語

教科書

なし

参考書

授業中に紹介

前提とする知識(必ずしも先修条件ではない)