著者

松本 宗太郎 南出 靖彦

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.49, no.3, pp.39-54, 2008-03-15

参考文献数

9

---

本研究では,多相レコード型に基づいてRubyプログラムの型推論ツールを設計,実装した.型推論ツールは,組み込みライブラリの型を記述したシグネチャとRubyプログラムを入力とし,プログラムの型を推論し,誤りを検出する.しかし,Rubyの柔軟性を表現できる,実用的で健全な型体系を設計しようとすると,体系は非常に複雑になる.それを避けるため,多相レコード型によって拡張されたMLの型推論アルゴリズムを,直接,Rubyに適用した.型体系は,非常に制限されたRubyプログラムに対しては,健全になるように設計した.Rubyにおいては,組み込みクラスなどの既存のクラスを拡張することが許されており,実際に多くのプログラムで既存のクラスが拡張されている.このようなプログラムを処理するために,シグネチャとプログラムを分離して型推論するのではなく,プログラムの一部としてシグネチャが含まれるよう型体系を設計した.実際のRubyプログラムを型付けする場合には,多相レコード型の表現力やMLの型推論アルゴリズムにおける再帰的な定義の型推論に関する多相性の制限から,いくつかの問題が生じることが分かった.これらの制限は,特に組み込みライブラリの型付けにおいて問題になることから,クラス定義を複製し展開することによって型推論を行った.We design and implement a type inference tool for Ruby programs. The type system is based on polymorphic record types of Garrigue. The tool takes two inputs, a type signature of the built-in classes and a Ruby program, and then infers the type of the Ruby program and detect type errors. The type system is a direct adaptation of that of ML with polymorphic records, and designed to be sound only for a restricted tiny subset of Ruby. Ruby allows programmers to modify existing classes and many programs actually modify existing (built-in) classes. Thus we design our type system so that type signatures and method implementation coexist in a class definition. We encounter difficulties when typing common Ruby programs, since polymorphic methods are not expressible in our type system and the ML type inference does not infer polymorphic types in recursive definitions. We alleviate these difficulties by introducing transformations that duplicate class definitions.

著者

松本 宗太郎 南出 靖彦

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.49, no.SIG3(PRO36), pp.39-54, 2008-03-15

---

本研究では,多相レコード型に基づいてRubyプログラムの型推論ツールを設計,実装した.型推論ツールは,組み込みライブラリの型を記述したシグネチャとRubyプログラムを入力とし,プログラムの型を推論し,誤りを検出する.しかし,Rubyの柔軟性を表現できる,実用的で健全な型体系を設計しようとすると,体系は非常に複雑になる.それを避けるため,多相レコード型によって拡張されたMLの型推論アルゴリズムを,直接,Rubyに適用した.型体系は,非常に制限されたRubyプログラムに対しては,健全になるように設計した.Rubyにおいては,組み込みクラスなどの既存のクラスを拡張することが許されており,実際に多くのプログラムで既存のクラスが拡張されている.このようなプログラムを処理するために,シグネチャとプログラムを分離して型推論するのではなく,プログラムの一部としてシグネチャが含まれるよう型体系を設計した.実際のRubyプログラムを型付けする場合には,多相レコード型の表現力やMLの型推論アルゴリズムにおける再帰的な定義の型推論に関する多相性の制限から,いくつかの問題が生じることが分かった.これらの制限は,特に組み込みライブラリの型付けにおいて問題になることから,クラス定義を複製し展開することによって型推論を行った.

著者

高橋 和也 南出 靖彦

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.38, no.2, pp.2_53-2_70, 2021-04-23 (Released:2021-06-23)

---

文字列の検索等に広く用いられる正規表現マッチングはその多くがバックトラックに基づくアルゴリズムで実装されており,対象文字列の長さに対して線形時間でマッチングを完了できない場合がある.これを事前に検知するために,マッチングに要する計算量を静的解析する手法が複数の先行研究によって提案されている.本研究では先行研究を拡張し,先読みや後方参照など,現実のソフトウェアで使用されている拡張された正規表現に対しても解析が行える手法を提案する.さらに,既存の解析アルゴリズムを高速化し,より実用的な速度で解析を行える手法を提案する.そして,これらの改良を施した計算量解析のツールをScalaで実装し,Weidemanらによる既存のツールよりも多くの正規表現が解析できることを実験により確認した.

著者

南出 靖彦 MINAMIDE YASUHIKO

巻号頁・発行日

2012

---

科学研究費助成事業(科学研究費補助金)研究成果報告書:基盤研究(C)2009-2011

著者

中川 みなみ 南出 靖彦

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.9, no.3, pp.28, 2016-06-06

---

正規表現マッチングは文字列を操作するウェブプログラムなど,様々な場面で用いられており,その実装の多くはバックトラックに基づいている.そのため,正規表現マッチングにかかる時間が文字列の長さに関して線形でないことがあり,最悪の場合指数関数時間となる.本発表では正規表現マッチングの時間計算量を判定する手法を提案する.対象の正規表現から先読み付き木トランスデューサを構成する.その先読み付き木トランスデューサから準同型写像や有限遷移系を構成し,それらを用いた遷移過程の中に反復補題が成り立つ遷移過程が存在しているか調べることで計算量を判定することができる.この判定には,AhoとUllmanによる木トランスデューサの増加率の判定法を先読み付き木トランスデューサに拡張したものを利用する.先行研究では,EngelfrietとManethのマクロ木トランスデューサの増加率の判定法を用い,正規表現マッチングの計算時間が入力文字列に対して線形であるかどうかを判定する手法が提案された.本発表で提案する手法は,時間計算量が線形であるかどうかの判定だけでなくO(n2),O(n3),...になることも判定できる.この提案手法をOCamlによって実装し,既存のPHPプログラムで使用されている正規表現を対象に実験を行った.実験の結果,393個中入力文字列の長さに対して338個が線形,44個が2乗,6個が3乗の計算量であると判定された.

著者

加賀江 優幸 南出 靖彦

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.8, no.3, pp.1-10, 2015-09-21

---

文字列から新たな文字列を生成する計算モデルとしてAlurとCernyによるストリーミング文字列トランスデューサ(Streaming String Transducer: SST)がある.SSTは,文字を受け取るごとに文字列を保存できる変数の内容を更新し,最終的には変数の内容を用いて出力文字列を構成するトランスデューサである.本研究では,関数的非決定性ストリーミング文字列トランスデューサ(関数的SST)の等価性判定を正規表現による文字列置換の等価性判定に応用する.ここで,関数的とは非決定性であっても出力がたかだか1つであることを示す.関数的SSTの等価性判定問題の決定可能性はAlurらによって証明されている.しかしながら,判定方法は複雑であり直感的な理解が困難であった.そこで,本論文では関数的SSTの等価性判定アルゴリズムの簡略化について述べる.また,本アルゴリズムの実装および実験結果についても述べる.正規表現による文字列置換はグループ変数にマッチした箇所を複数回出力することができることから有限状態トランスデューサでは模倣できない.そこで,本論文では正規表現による文字列置換を関数的SSTで模倣することにより,関数的SST上の検証問題に帰着させる.最終的には,関数的SSTの等価性判定アルゴリズムを正規表現による文字列置換の等価性判定に応用する.

著者

上里 友弥 南出 靖彦

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.7, no.4, pp.8-20, 2014-08-29

---

本論では,言語が決定性文脈自由言語(DCFL)ではないことを証明するための,決定性プッシュダウンオートマトン(DPDA)に基づく手法を提案する.提案する手法は,計算中でのスタックの高さを特徴付けるもので,以下のようなスタックの変化に対する直感を形式的に扱うことができる:言語{anbncn | n ≧ 1}が何らかのDPDAで受理できたとすると,aの個数とbの個数を比較した結果として,anbnの部分を読み終わった段階のスタックはほとんど空になっているはずである.このとき,続く文字列cnを検査することができない.したがって,この言語はDCFLではない.具体的には,十分に長い繰返し文字列を消費した結果のスタックの内容には繰返し構造があることを示し,繰返し文字列を消費した結果のスタックが一般化順序機械と呼ばれる機械で定義可能であることを示した.この結果を用いて,上の例のようにaの個数とbの個数を比較するためには,スタックがほとんど空にならなければならないことを形式化して示した.

著者

井田 哲雄 南出 靖彦 MARIN Mircea 鈴木 大郎

出版者

筑波大学

雑誌

基盤研究(B)

巻号頁・発行日

2008

---

ウェブソフトウェア検証の事例研究として, WebEosの核となる部分の形式化と検証を行った.幾何と代数の基本的な部分にMathematicaの計算結果を援用することで, 効率的な検証が可能となった.文字列解析による検証において, 正規表現マッチングの正確な解析を可能とした.また, データベースとの連携の解析を導入し, 蓄積型XSS脆弱性検査を実現した.ポジションオートマトンを利用した正規表現の貪欲マッチングアルゴリズムの設計と実装を行った.

著者

南出 靖彦

出版者

筑波大学

雑誌

若手研究(B)

巻号頁・発行日

2001

---

関数型プログラミング言語のコンパイラで用いられるCPS変換の定理証明システムIsabelle/HOLによる検証について二つの拡張を行った.まず,CPS変換がプログラムの実行に必要な記憶領域の大きさを保存することを検証した.証明すべき性質はより複雑なものになり,証明の長さも2倍程度になった.しかし,変換で導入される変数の形式化などは,記憶領域を考慮しない場合の形式化をそのまま応用することができ,自動証明を多くの補題の証明に用いることができた.次に,変換の検証を自由変数に含む式に拡張した.前年度の検証では,扱うプログラムが閉じた式であることを仮定し,証明を単純化した.しかし,前年度の証明を再検討したところ,この制限は証明の単純化にあまり貢献していないことがわかった.そこで,本年度には,この制限を取り除いて検証を行い,この制限が本質的でないことを確認した.関数型プログラミング言語の末尾呼び出しを,Java仮想機械などの末尾呼び出しを直接サポートしていない環境で効率的に実装するためのプログラム変換を提案した.末尾呼び出しをサポートしない環境でも,特殊な関数呼び出しの仕組みを用いることで,末尾呼び出しが実現できるが,そのような方法はオーバーヘッドが大きい.提案した方法では,型推論を用いてプログラムの末尾呼び出しに関する性質を推論する.その型情報に基づき,末尾呼び出しの正当な実装が必要な関数に対してだけ,選択的に,非効率的な末尾呼び出しの実装を用いることで,オーバーヘッドを抑えている.

著者

大熊 浩示 南出 靖彦

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌. プログラミング (ISSN:03875806)

巻号頁・発行日

vol.46, no.6, 2005-04-15

---

正しいコンパイラを得るためには, コンパイラの形式化が正しいだけでなく, その実装の正しさも検証しなければならない.我々は定理証明システムIsabelle/HOLを用いてコンパイラを形式化し, その正しさを検証した.さらに, Isabelle/HOLのコード生成機能を用い, Isabelle/HOLで記述されたコンパイラを実行可能なプログラムへ変換した.このコード生成機能はIsabelle/HOLの構文をStandard MLの構文に単純に変換するもので, 生成されたプログラムの信頼性は高いといえる.コンパイラは構文解析を除くすべてのフェーズがIsabelle/HOLで記述されており, コード生成機能で変換されたプログラムに構文解析プログラムなどを加えることにより実行可能な検証されたコンパイラを得ることができる.コンパイラはScheme構文を持つ関数型プログラミング言語を入力とし, Java仮想機械のアセンブリ言語を生成する.今回形式化したコンパイラはクロージャ変換やインライン展開など, これまで検証されたコンパイラでは扱われていない高度なプログラム変換を行っている.また, コンパイラの記述ではコンパイル時間も考慮し, 効率の良いデータ構造を採用した.得られたコンパイラをいくつかのSchemeプログラムに対して適用した結果, コンパイル時間, 生成されたプログラムの実行時間ともに既存のコンパイラに劣らない結果が得られた.