記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.2197/ipsjtrans.7.82

researchmap

記述言語：日本語   掲載種別：研究論文（国際会議プロシーディングス）  

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：一般社団法人情報処理学会  

プログラミング言語における正規表現の拡張の1つとしてアトミックグループがある.アトミックグループとは,一度構文内でのマッチが成功し構文を抜けると,構文内へのバックトラックを禁止する構文である.本論文では,アトミックグループで拡張された正規表現のオートマトンへの変換を構成し,その正当性を証明する.拡張された正規表現の意味はSakumaらによるリストモナドを用いた定義により与える.アトミックグループで拡張された正規表現の表す言語を定義するために,集合モナドを用いた非決定構文解析器を定義する.アトミックグループによるマッチングは,オプションモナドを用いた決定性構文解析器によって表現する.この非決定性構文解析器と決定性構文解析器は相互再帰的な等式となっており,それによって拡張された正規表現の表す言語を表現する.この相互再帰的な等式をもとに,それと等価な先読み付きオートマトンを構成する.先読み付きオートマトンは先読みなしのオート

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

The reachability analysis of weighted pushdown systems is a very powerful technique in verification and analysis of recursive programs. Each transition rule of a weighted pushdown system is associated with an element of a bounded semiring representing the weight of the rule. However, we have realized that the restriction of the boundedness is too strict and the formulation of weighted pushdown systems is not general enough for some applications. To generalize weighted pushdown systems, we first introduce the notion of stack signatures that summarize the effect of a computation of a pushdown system and formulate pushdown systems as automata over the monoid of stack signatures. We then generalize weighted pushdown systems by introducing semirings indexed by the monoid and weaken the boundedness to local boundedness. © 2013 Springer-Verlag.

DOI： 10.1007/978-3-642-36742-7_17

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Pushdown systems are a model of computation equipped with one stack where only the top of the stack is inspected and modified in each step of transitions. Although this is a natural restriction, some extensions of pushdown systems require more general operations on stack: conditional pushdown systems inspect the whole stack contents and discrete timed pushdown systems increment the ages of the whole stack contents. In this paper, we present a general framework called pushdown systems with transductions (TrPDS) for extending pushdown systems with transitions that modify the whole stack contents with a transducer. Although TrPDS is Turing complete, it is shown that if the closure of transductions appearing in the transitions of a TrPDS is finite, it can be simulated by an ordinary pushdown system and thus the reachability problem is decidable. Both of conditional and discrete timed pushdown systems can be considered as such subclasses of TrPDS. © 2013 Springer International Publishing.

DOI： 10.1007/978-3-319-02444-8_29

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.1016/j.jal.2011.11.003

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：ELSEVIER SCIENCE BV  

Regular expression matching is an essential tool in string manipulating programs and plays crucial roles in scripting languages. We focus on regular expression matching based on the strategy of Perl and develop a translation from regular expression matching into transducers. The representation makes it possible to apply the theory of formal languages in static analysis and verification of string manipulating programs.
We first formulate the semantics of regular expression matching as a nondeterministic parser by using the composition of the list and output monads. Then, we transform the nondeterministic parser into deterministic one by introducing lookahead. The deterministic parser is formulated with the option monad instead of the list monad and derived through equational reasoning involving monads. From the definition of the deterministic parser, we can easily construct transducers through transducers with regular lookahead. We have implemented the translation and conducted experiments on regular expressions found in several popular PHP programs. (C) 2011 Published by Elsevier B.V.

DOI： 10.1016/j.jal.2011.11.003

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

A draft standard for HTML, HTML5, includes the detailed specification of the parsing algorithm for HTML5 documents, including error handling. In this paper, we develop a reachability analyzer for the parsing specification of HTML5 and automatically generate HTML documents to test compatibilities of Web browsers. The set of HTML documents are extracted using our reachability analysis of the statements in the specification. This analysis is based on a translation of the specification to a conditional pushdown system and on a new algorithm for the reachability analysis of conditional pushdown systems. In our preliminary experiments, we generated 353 HTML documents automatically from a subset of the specification and found several compatibility problems by supplying them to Web browsers. © 2012 Springer-Verlag.

DOI： 10.1007/978-3-642-32759-9_26

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：IEEE COMPUTER SOC  

Regular expression matching is an essential tool in string manipulating programs and plays crucial roles in scripting languages. We focus on regular expression matching based on the strategy of Perl and develop a translation from regular expression matching into transducers. The representation makes it possible to apply the theory of formal languages in static analysis and verification of string manipulating programs.
We first formulate the semantics of regular expression matching as a nondeterministic parser. Then, we transform the nondeterministic parser into deterministic one by introducing lookahead. From the definition of the deterministic parser, we can easily construct transducers through transducers with regular lookahead. We have implemented the translation and conducted experiments on regular expressions found in several popular PHP programs.

DOI： 10.1109/SYNASC.2010.50

Web of Science

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：一般社団法人情報処理学会  

Rubyプログラムの制御フロー解析を設計し,その健全性を操作的意味論に基づき証明する.Ruby などのスクリプト言語に関する静的プログラム解析は多く提案されているが,その健全性について言語の意味論に基づき証明がなされたものは少ない.本研究では,Ruby のコア言語について操作的意味論を定義し,その意味論に基づき制御フロー解析の健全性を証明する.Ruby のコア言語は,ruby 1.9 処理系の構文解析器によって得られる中間言語をモデルとし,メソッドの動的な定義・イテレータブロック・大域脱出などを含む.Ruby では,クラス・メソッドの定義は,宣言ではなく動的に評価される式であり,さらにメソッド定義の上書きが可能である.そのため,プログラムの実行時の制御フローによって,異なるクラス定義・メソッド定義が得られる可能性がある.本研究では,メソッド定義が評価されたかどうかについて,制御フローを区別する解析を行う.これにより,特に多く見られる,トップレベルでクラス・メソ

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：ASSOC COMPUTING MACHINERY  

PHP is a popular language for server-side applications. In PHP, assignment to variables copies the assigned values, according to its so-called copy-on-assignment semantics. In contrast, a typical PHP implementation uses a copy-on-write scheme to reduce the copy overhead by delaying copies as much as possible. This leads us to ask if the semantics and implementation of PHP coincide, and actually this is not the case in the presence of sharings within values. In this paper, we describe the copy-on-assignment semantics with three possible strategies to copy values containing sharings. The current PHP implementation has inconsistencies with these semantics, caused by its naive use of copy-on-write. We fix this problem by the novel mostly copy-on-write scheme, making the copy-on-write implementations faithful to the semantics. We prove that our copy-on-write implementations are correct, using bisimulation with the copy-on-assignment semantics.

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Springer  

DOI： 10.1007/978-3-540-70844-5_13

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：一般社団法人情報処理学会  

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

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Springer  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Springer  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会  

DOI： 10.11309/jssst.24.3_15

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Springer  

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：一般社団法人情報処理学会  

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

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：ACM  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

Previous studies on safety of program transformations with respect to performance considered two criteria: preserving performance within a constant factor and preserving complexity. However, as the requirement of program transformations used in compilers the former seems too restrictive and the latter seems too loose. We propose a new safety criterion: a program transformation preserves performance within a factor proportional to the size of a source program. This criterion seems natural since several compilation methods have effects on performance proportional to the size of a program. Based on this criterion we have shown that two semantics formalizing the size of stack space are equivalent. We also discuss the connection between this criterion and the properties of local program transformations rewriting parts of a program. ©2000 Published by Elsevier Science B. V.

DOI： 10.1016/S1571-0661(04)80871-5

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap