著者

住井 英二郎

雑誌

情報処理

巻号頁・発行日

vol.56, no.5, pp.434-437, 2015-04-15

---

いわゆる「形式手法」によるソフトウェア検証の基本となる「プログラミング言語理論」の特に基本的な部分を,中学~大学1年程度の数学のみを用いて,できるだけ平易に(ただし実質的詳細にも踏み込んで)紹介する.

著者

住井 英二郎

出版者

一般社団法人日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.25, no.2, pp.28-38, 2008-04-24

被引用文献数

1

---

約2000行のMLコードにより実装された,教育目的のコンパイラMinCamlについて議論する.対象言語は値呼び,非純粋,暗な単相型を持つ高階関数型言語である.レイトレーシングを含むいくつかのアプリケーション・プログラムに対し,実行速度においてObjective CamlやGCCとほぼ同等のコードを生成することができた.

著者

上嶋 祐紀 住井 英二郎

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.26, no.1, pp.139-154, 2009

---

C言語サブセットのプログラムを安全なJava言語のプログラムに変換する方式を実装した.そのような変換のためには,C言語独特の操作であるポインタ演算を,Javaプログラムで安全に模倣する必要がある.これを実現するために,まずC言語のポインタやメモリブロックを表現するJavaのクラスを定義した.次に,これらのクラスを利用するようなJavaへの変換規則を定め,規則に従ってトランスレータを実装した.また,C言語ではポインタと整数を相互にキャストすることが可能なので,整数もポインタと同様のオブジェクトに変換しなければならない.しかし,すべての整数をポインタと同様に表現すると大幅に効率が悪化する.そこで,データフロー解析により,ポインタが代入されない基本型の変数は,Javaの通常の基本型変数に変換する,などの最適化を実装した.9個のベンチマークプログラムで実験したところ,最適化前の変換結果コードは元のCプログラムに対し3.3倍~585倍程度の実行時間がかかったが,最適化後は(元のCプログラムに対し)1.3倍~5.9倍程度に改善した.

著者

住井 英二郎 首藤 一幸

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.26, no.2, pp.2_1-2_2, 2009-04-24 (Released:2009-06-24)

著者

住井英二郎 大根田裕一 米澤 明憲

雑誌

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

巻号頁・発行日

vol.45, no.SIG12(PRO23), pp.67-82, 2004-11-15

---

制御フローグラフに類似した一般的な命令型言語を,CPS(継続渡しスタイル)を中間表現としてコンパイルする方法を提案する.CPS とは,「残りの計算」(継続と呼ばれる)を表現する関数を生成することにより,すべての関数呼び出しや条件分岐を末尾位置においた関数型言語の一種であり,Scheme やML といった関数型言語のコンパイラに広く用いられている.命令型言語をCPS に変換することで,スタックフレームや例外ハンドラが継続として明示化され,関数適用や例外処理における複雑な制御の流れが明確化される.結果として,インライン展開や末尾呼び出し最適化を含む多くの最適化が容易に実現できる.我々は命令型言語をCPS に変換する過程の単純な定式化を与え,その正しさを証明する.

著者

住井 英二郎

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.25, no.2, pp.2_28-2_38, 2008 (Released:2008-06-30)

---

約2000行のMLコードにより実装された,教育目的のコンパイラMinCamlについて議論する.対象言語は値呼び,非純粋,暗な単相型を持つ高階関数型言語である.レイトレーシングを含むいくつかのアプリケーション・プログラムに対し,実行速度においてObjective CamlやGCCとほぼ同等のコードを生成することができた.

著者

住井 英二郎

出版者

公益財団法人 日本学術協力財団

雑誌

学術の動向 (ISSN:13423363)

巻号頁・発行日

vol.21, no.3, pp.3_118-3_120, 2016-03-01 (Released:2016-07-01)

著者

住井 英二郎 小林 直樹

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.16, no.4, pp.4_372-4_377, 1999-07-15 (Released:2018-11-05)

著者

上嶋 祐紀 住井 英二郎

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.26, no.1, pp.1_139-1_154, 2009-01-27 (Released:2009-03-27)

---

C言語サブセットのプログラムを安全なJava言語のプログラムに変換する方式を実装した.そのような変換のためには,C言語独特の操作であるポインタ演算を,Javaプログラムで安全に模倣する必要がある.これを実現するために,まずC言語のポインタやメモリブロックを表現するJavaのクラスを定義した.次に,これらのクラスを利用するようなJavaへの変換規則を定め,規則に従ってトランスレータを実装した.また,C言語ではポインタと整数を相互にキャストすることが可能なので,整数もポインタと同様のオブジェクトに変換しなければならない.しかし,すべての整数をポインタと同様に表現すると大幅に効率が悪化する.そこで,データフロー解析により,ポインタが代入されない基本型の変数は,Javaの通常の基本型変数に変換する,などの最適化を実装した.9個のベンチマークプログラムで実験したところ,最適化前の変換結果コードは元のCプログラムに対し3.3倍~585倍程度の実行時間がかかったが,最適化後は(元のCプログラムに対し)1.3倍~5.9倍程度に改善した.

著者

住井 英二郎

出版者

一般社団法人 日本応用数理学会

雑誌

応用数理 (ISSN:24321982)

巻号頁・発行日

vol.17, no.4, pp.280-290, 2007-12-26 (Released:2017-04-08)

参考文献数

15

---

This survey presents Abadi and Gordon's spi-calculus, which is a "process calculus" (i.e., a formal language of concurrent computation) for the verification of "cryptographic protocols" (i.e., procedures for secure communication in computer networks). First, we present process calculi before the spi-calculus (CCS and the pi-calculus), introducing the notion of reaction relation and structural congruence. We then define the spi-calculus and show an example of cryptographic ptotocols, represented as a class of spi-calculus processes. After discussing the formalization of security properties (secrecy and authenticity) and multiple sessions, we conclude by referring to generalizations of the spi-calculus (Abadi and Fournet's applied pi-calculus, and a recent result by Bruno Blanchet).

著者

水野 雅之 住井 英二郎

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.34, no.2, pp.2_114-2_119, 2017-04-26 (Released:2017-05-11)

---

コンパイラの形式的検証は盛んに研究されているが,入出力等の副作用がある高階関数型プログラミング言語のコンパイラの検証はあまり行われていない.これは無限に入出力を行うプログラムの意味論の形式化が自明でないためである.我々は,入出力等の副作用を持つ外部関数の呼び出しや再帰関数,高階関数,組を持つ値呼びの関数型プログラミング言語に対するK正規化を定理証明支援系Coqを用いて形式的に検証した.K正規化とはlet式を用いて全ての中間式に対し陽に名前を与えるプログラム変換であり,束縛の操作を伴う点で形式化が自明でない.本研究では,余帰納的大ステップ操作的意味論によりプログラムの意味を外部関数呼び出しの無限列として与えた.また,束縛の表現としては,他の手法と比較検討した上でde Bruijnインデックスを採用した.

著者

住井 英二郎

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.33, no.2, pp.2_92-2_93, 2016-04-22 (Released:2016-06-22)