Language：English   Publishing type：Research paper (scientific journal)  

DOI： 10.2197/ipsjtrans.7.82

researchmap

Language：Japanese   Publishing type：Research paper (international conference proceedings)  

researchmap

Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Information Processing Society of Japan (IPSJ)  

Atomic grouping is one of the extensions of regular expressions used in programing languages. When a word is matched against an atomic group, the construct disables backtracking into the group. In this paper, we translate regular expressions extended with atomic grouping into finite automata and prove the correctness of the translation. The semantics of extended regular expressions is given as a nondeterministic parser defined with the list monad. Then, the language of an extended regular expression is represented by using mutually recursive functions: a nondeterministic parser defined with the set monad and a deterministic parser defined with the option monad. We construct finite automata with regular lookahead based on their definitions and translate them into finite automata without lookahead by a standard construction. We have implemented this translation in OCaml, and conducted experiments of translating regular expressions containing atomic groups into DFA. For the experiments, we use regular expressions that appear in CPAN (Comprehensive Perl Archive Network) and Mastering Regular Expressions 3rd Edition.

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)  

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

Language：English   Publishing type：Research paper (international conference proceedings)  

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

Language：English   Publishing type：Research paper (scientific journal)  

DOI： 10.1016/j.jal.2011.11.003

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：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

Language：English   Publishing type：Research paper (international conference proceedings)  

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

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：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

Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Information Processing Society of Japan (IPSJ)  

We design a semi-flow-sensitive control flow analysis for Ruby, and prove its soundness. Static analysis of scripting languages including Ruby has been actively studied recently, but few of the analysis proved their correctness with respect to language semantics. We formalize an operational semantics of the core of Ruby. It is designed based on the intermediate language obtained by the parser of ruby-1.9, and supports dynamic method definition, iterator blocks, and non-local exits. Our analysis is semi-flow-sensitive in the sense that it is not sensitive on the values of a variable at each program point, but on which method definitions have been evaluated. This sensitivity makes it possible to precisely analyze typical Ruby programs where the definition of a class is split into several top-level class definitions.

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：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

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Springer  

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

researchmap

Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Information Processing Society of Japan (IPSJ)  

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 adaptaion 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 signature and method implementation coexist in a class definition. We encounter difficluties 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 difficluties by introducing transformations that duplicate class definitions.

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Springer  

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Springer  

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Japan Society for Software Science and Technology (JSSST)  

DOI： 10.11309/jssst.24.3_15

Scopus

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：Springer  

researchmap

Language：Japanese   Publishing type：Research paper (scientific journal)   Publisher：Information Processing Society of Japan (IPSJ)  

To obtain a correct compiler, it is not enough to show its formalization is correct, but it is also required to show that the implementation of the compiler is correct. We formalized a compiler with the theorem prover Isabelle/HOL, and proved its correctness. Then, we translated the compiler definition from Isabelle/HOL into a Standrad ML program, using Isabelle/HOL's code generation facility. Since this code generation program only performs simple syntactic translation, the correctness of the obtained program can be highly trusted. The compiler we defined with Isabelle/HOL covers all phases of the compiler, except a front-end. We provided a hand-written parsing program, and obtained a verified, executable compiler. Our compiler compiles a functional language similar to Scheme into a Java virtual machine assembly language. It includes several non-trivial program transformations such as closure conversion and inline expansion. Taking compilation time into consideration, we chose efficient data structures in our specification. Benchmarks show that our compiler is comparable to existing compilers both in compilation time and running time.

researchmap

Language：Japanese   Publishing type：Research paper (scientific journal)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)   Publisher：ACM  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (international conference proceedings)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

researchmap

Language：English   Publishing type：Research paper (scientific journal)  

researchmap