K.Funakoshiのホームページ(天文以外の頁)  last update:2017.9.24

-ソフトウェアと数学の接点-

 ここでは、ソフトウェア(又はプログラム)の問題に数学的考え方を適用する例として
主に「抽象解釈(Abstract Interpretation)」を取り上げます。抽象解釈については日本語で
分かり易く書かれた資料がないので、この分野の開拓者であるCousotの論文を中心に紹介
します。また、抽象解釈の根底にはスコットのプログラム理論があるのでそれについても紹介
します。

■抽象解釈

 1.抽象解釈とは?

 2.単純なプログラム例による抽象解釈入門(Cousot初期論文[1977年]を読む)

   ・
目次及び序論

   ・第1章 準備

   ・第2章 抽象解釈概要(主にCousot初期論文から)

   ・第3章 初期論文以降の展開と抽象解釈考

 3.Cousot 1976年の論文(プログラムの動的性質の静的決定)紹介
  →Cousot初期論文[1977年]の前年の論文。プログラムの抽象解釈の基本的な考え方が
   具体例で示されている。

 4.widening解説

 5.抽象解釈の初心者向け解説の紹介

   @
エコール・ノルマルP.Cousot教授のMITでの抽象解釈紹介資料解説
    →2005年にMIT(マサチューセッツ工科大学)で行われた抽象解釈の集中講義(Lecture1〜20)
     の最初の導入部分(Lecture1)。

   Aカンサス州立大学D. Schmidt教授の抽象解釈紹介資料解説
    →「象の絵」で抽象解釈の概念を説明するなど分かり易い資料。

 6.【仏和対訳】Cousotの2000年の論文(工事中)


 7.フロー・ダイアグラムの束 − Dana Scottの論文紹介
  →ソフトウェアのフローダイアグラムの構造を数学の束論により表現できることを示している。
   また、無限ループを完備性により説明している。

 8.モデル検査における抽象化(工事中)
  →Kripke構造間のガロア接続について


 9.ガロア接続の由来

 10.(参考)【仏和対訳】ガロアの第一論文(工事中)

■スコットのプログラム理論 NEW
 1.中島玲二著 数理情報学入門を読む(1)

HPのTOP(天文関係)へ戻る

 ご意見・ご感想は ccr61210(at)syd.odn.ne.jp (atを@にして) まで。