3 0 0 0 OA 証明支援系を用いたMorrisの2分木走査アルゴリズムの実装の検証
- 著者
- 山田一宏 森口草介 渡部卓雄 西崎真也
- 雑誌
- 第73回全国大会講演論文集
- 巻号頁・発行日
- vol.2011, no.1, pp.505-506, 2011-03-02
我々は,Morrisの2分木走査アルゴリズムのCによる実装を対象として,証明支援系を用いた正当性の検証を試みた.本論文はその手法と結果に関する報告である.Morrisのアルゴリズムは,ポインタの書き換えを行うことで再帰やスタックを用いずに2分木走査を行う方法のひとつである.また他のポインタ反転法と異なり節点に印を付けるためのビットを設ける必要もないのが特徴である.我々は,入力および走査結果についての仕様を事前・事後条件として与え,C用の検証支援ツールであるCaduceusによって検証条件を生成した.ループ不変条件は必要に応じて適宜与えた.生成された検証条件を自動検証ツールSimplifyおよび証明支援系Coqを用いて証明した.
2 0 0 0 OA ファーストクラス継続をもつ仮想機械
- 著者
- 西崎 真也 植田 友幸
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- 日本ソフトウェア科学会大会講演論文集 日本ソフトウェア科学会第20回記念大会 (ISSN:13493515)
- 巻号頁・発行日
- pp.6, 2003 (Released:2003-12-17)
従来,関数型言語のためのバイトコードを解釈する仮想機械として、SECDマシンやCAMマシンなど多くのものが提唱され,それらに基づく実装や理論的な側面に関する研究がなされてきた.本論文では,SECDマシンを単純化した仮想機械SAM(Simple Abstract Machine)を提唱する.変数参照機能を単純化することにより,仮想機械におけるファーストクラス継続を簡潔に扱うことが可能になっている。
2 0 0 0 OA 通信プロトコルにおけるサービス不能攻撃耐性解析のための型付きπ計算
- 著者
- 冨岡 大悟 池田 立野 西崎 真也
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.23, no.3, pp.3_66-3_84, 2006 (Released:2006-09-30)
通信プロトコルの安全性,特に認証プロトコルにおける認証の正当性に関する研究は,AbadiやGordonによるspi計算(secure pi-calculus)などをはじめとして,近年さかんに行なわれている.プロトコルにおける安全性は,認証の正当性や機密性などの他に,最近では,サービス不能攻撃(Denial-of-Service attack)耐性が重要視される.もっとも典型的な攻撃例としては,TCPの3ウェイハンドシェイクにおけるSYNあふれ攻撃(SYN-flooding attack)が知られている.プロトコルのサービス不能攻撃耐性を形式的に扱う枠組みとしては,メドーズらにより提唱された,コスト情報を付記したアリス・ボブ記法があった.この他に,最近,冨岡らにより提唱されたspice計算[13]がある.spice計算は,spi計算を拡張したもので,プロセスの計算における計算コストが,サーバーやクライアントの計算機において,どのように費されるかを明示的に表現できるように,システムにおける計算機構成を型として形式化した.そして,書き換えスタイルの操作的意味論があたえられており,プロセスに対する型付けの情報を利用することにより,計算の進行における計算コストを区別するようになっている.記憶コストは,サービス不能攻撃耐性を測る場合,各種の計算コストのうちで最も重要となるのだが,spice計算では,記憶領域の解放を明示的に行なうようにした.本研究では,従来のspice計算における型体系と操作的意味論を,計算機ごとの記憶コストの見積りに併せて,記憶領域の解放に関する正当性を保証するように,改良した.また,SYNあふれ攻撃とその防御策であるSYNクッキーが形式化できることを適用例として紹介する.
2 0 0 0 OA 継続つきプログラミング言語と線形論理
- 著者
- 西崎 真也
- 雑誌
- 情報処理学会研究報告プログラミング(PRO)
- 巻号頁・発行日
- vol.1991, no.32(1991-PRO-001), pp.21-28, 1991-04-26
線形論理の枠組のもとで継続つきプログラムについて考察した。継続つきプログラミング言語から線形論理への変換を定義し、継続プリィミティブ call/cc が証明ネットで記述でき、線形論理が継続つきのプログラムを記述する能力があることを示した。継続つきプログラムの特徴として、計算結果が評価戦略に依存することがあるが、この変換は評価戦略に関する情報を付加する。
2 0 0 0 デバッギングを指向した型推論に関する研究
平成14年度においては、次のような事項について研究を推進した。《先進的な型推論アルゴリズムの調査・分析》近年提唱された先進的な型推論アルゴリズムについて、網羅的に調査をおこない、デバッグ作業の支援という観点から検討・分析に取り組んだ。とくに、コンカレント・プログラミングのための型推論や、セキュア・プログラミングのための型推論などを中心にすえた。《デバッグ作業を支援するための型推論の拡張》前項で調査した「先進的な型推論アルゴリズム」に対する検討を基にして、平成13年度の「デバッグ作業を支援するための型推論の開発」の成果の拡張に取り組んだ。《プロトタイプシステムの実装》平成13年度の「デバッグ作業を支援するための型推論の開発」で得られた理論的成果、および、前項により得られた成果について、プロトタイプシステムを実装することを通して、実際的な観点から、有用性について評価をおこない、従来の言語処理系における型推論との比較検討をおこなった。
1 0 0 0 OA 論理と計算のしくみと私
- 著者
- 西崎 真也
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.32, no.3, pp.3_96-3_97, 2015-07-24 (Released:2015-09-24)
1 0 0 0 ファーストクラス環境による単一化機構の関数型言語への組み込み
- 著者
- 西崎 真也 樋口 貴志
- 出版者
- 一般社団法人情報処理学会
- 雑誌
- 情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
- 巻号頁・発行日
- vol.41, no.9, pp.103-103, 2000-11-15
本論文では,ファーストクラス環境の機構を用いて単一化機構を関数型言語へ組み込む方法を提唱する.単一化子は変数上の代入として表現されるが,これを変数の束縛する環境とを同一視することにより,単一化の機構を関数型言語へ自然に組み込むことが可能となる.In this paper, we propose a way of embedding of the unification mechanism into function languages through facility of first-class environments, where unificands are introduced as expressions and their evaluation is defined as the first-order unification.
1 0 0 0 ファーストクラス継続を持つオブジェクト計算
- 著者
- 西崎 真也 小田 崇史
- 出版者
- 一般社団法人情報処理学会
- 雑誌
- 情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
- 巻号頁・発行日
- vol.44, no.13, pp.116-116, 2003-10-15
AbadiとCardelliにより提唱されたオブジェクト計算は,大変簡潔な構文と意味論により定義されるにもかかわらず,セルフパラメータの遅延束縛などオブジェクト指向言語の主要な計算機構をモデル化することに成功している.継続とは,計算のある時点における計算の残りの部分を表現する概念であり,実行系の内部状態の1つである.ファーストクラス継続は,ある時点の継続をデータとして保存したり,データとして保存した継続をしたりすることを可能とするものである.ファーストクラス継続は,プログラミング言語Schemeで実現され,コルーチンやバックトラックなどを表現できることが知られている.本研究では,オブジェクト計算にファーストクラス継続の概念を導入した継続オブジェクト計算を提唱する,この体系において,意味論は評価文脈を用いて定義される弱簡約関係により与えられる.ファーストクラス継続は,評価文脈をフィールドに保存する継続オブジェクトとして形式化される.最初に型なし継続オブジェクト計算を紹介する.次に,継続オブジェクト計算の1階型体系を与え,主部簡約定理を示す.さらに,部分型体系を与え,主部簡約定理のほか,基本的性質を示す.With the advance of information society, releasing the software at an early stage that satisfies users has been required, and therefore it has been more important to quickly develop the software that the user can check and feed back. In software development, based on users' concept, developers make the specifications of a program cooperating with the users, and then design, make, test and debug the program. Through this procedure, programs are completed. If we can use the image that users have to design a program, and if the program is completed when the design finishes, we can easily develop software and reduce the time required to develop it. This presentation presents an approach to a brain-image oriented programming method and describes the BioPro system that implements this method for Web applications. The brain-image oriented programming has the features that users can develop programs based on their image, (2) easily verify the completeness of components that make up the program and the consistency between them, and (3) easily confirm what they have developed so far in the middle of the development.