著者
小野 諭 小川 瑞史
出版者
一般社団法人日本ソフトウェア科学会
雑誌
コンピュータソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.13, no.2, pp.115-130, 1996-03-15
被引用文献数
2

抽象実行とは,プログラムの様々な性質を解析するために提案された理論的なフレームワークである.これは,プログラムのデータ領域や計算動作などの意味を抽象化した有限抽象領域を設計し,その上でプログラムを不動点計算と呼ばれる手法で「実行」することにより,プログラムの性質を求める. そこで,本チュートリアルでは,プログラム解析のごく初歩的な知識を持つ読者を対象にして,抽象実行の基本概念,分類,具体的設計法、仕様記述への展望などを説明する.対象言語としては,遅延評価型の関数型言語を取り上げる.ただし仕様記述への展望は,手続き型言語における様相論理や時相論理による仕様記述をベースに説明する.
著者
小川 瑞史
出版者
一般社団法人情報処理学会
雑誌
情報処理学会研究報告. [プログラミング-言語基礎実践-]
巻号頁・発行日
vol.93, no.46, pp.75-85, 1993-05-28

近年Robertson-Seymourにより証明されたグラフマイナー定理(Wagnberの予想)により有限グラフ上のminor-closedな性質の検出は多項式時間アルゴリズムが存在することが知られている.しかし,その証明は非構成的であり一般に実際のアルゴリズムを構成するのは難しかった.本稿ではグラフマイナー定理の簡単な場合であるHigmanの補題の構成的証明を用い,未解決問題であった時間概念を含むデータベース上の選言的単項質問処理の線形時間アルゴリズムを自動生成により与えた.
著者
小川 瑞史 小野 諭
出版者
一般社団法人日本ソフトウェア科学会
雑誌
コンピュータソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.13, no.4, pp.283-302, 1996-07-15
被引用文献数
2

関数型言語の抽象実行のフレームワークとして,領域抽象化による順方向実行と逆方向実行についてストリクトネス解析を例として説明する.さらにそれらを統一的に扱う4つのパラメータについて説明し,計算経路解析をそのパラメータ表現に基づき表す(1章).次に逆方向実行であるプロジェクション解析を説明し,計算経路解析と比較する(2章).最後にper (Partial Equivalence Relation)による順方向実行の抽象実行を説明し,プロジェクション解析や計算経路解析と比較する(3章).