著者

山田一宏 森口草介 渡部卓雄 西崎真也

雑誌

第73回全国大会講演論文集

巻号頁・発行日

vol.2011, no.1, pp.505-506, 2011-03-02

---

我々は,Morrisの2分木走査アルゴリズムのCによる実装を対象として,証明支援系を用いた正当性の検証を試みた.本論文はその手法と結果に関する報告である.Morrisのアルゴリズムは,ポインタの書き換えを行うことで再帰やスタックを用いずに2分木走査を行う方法のひとつである.また他のポインタ反転法と異なり節点に印を付けるためのビットを設ける必要もないのが特徴である.我々は,入力および走査結果についての仕様を事前・事後条件として与え,C用の検証支援ツールであるCaduceusによって検証条件を生成した.ループ不変条件は必要に応じて適宜与えた.生成された検証条件を自動検証ツールSimplifyおよび証明支援系Coqを用いて証明した.

著者

川﨑 樹 森口 草介 高橋 和子

出版者

一般社団法人 人工知能学会

雑誌

人工知能学会全国大会論文集 第33回全国大会(2019)

巻号頁・発行日

pp.4E3OS7b03, 2019 (Released:2019-06-01)

---

法律の構成から双極議論フレームワーク(BAF)を構築する手法を示す. 各法律はその効果を発揮するために満たすべき要件事実と, その効果を排斥させるための例外から成る. それぞれを論証間の支持関係、攻撃関係に対応させて BAF を構築する. また,BAF を用いて,与えられた事実から結論すなわち効果を発揮する法律が何かを 推論する手法を示す. この手法は事実と結論の間の双方向の推論になっており,まず,与えられた事実のみから得られる結論を導き, その推論結果を用いて新たな結論を導くのに必要な事実を抽出する.

著者

森口 草介 渡部 卓雄

雑誌

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

巻号頁・発行日

vol.2, no.5, pp.43-43, 2009-11-20

---

アスペクト指向が提案されて十余年たち,ソフトウェア工学の広い分野で用いられている.しかしながら,アスペクトとは何であるかを議論することはほとんどなく,ただAspectJに代表されるジョインポイントモデルにおけるモジュールをアスペクトとすることが多い.このように本質を定義しないままの議論は実際の言語に強く依存したものとなり,またツールにおけるアルゴリズムとその実装もアドホックになる.アスペクト指向はモジュール化を主眼としたものであり,その特徴はアスペクトモジュールの結合方法にあるといえる.本研究では,この結合方法を抽象化および定式化し,アスペクト指向の理解や議論の基礎とすることを目標としている.本研究の特徴はアスペクト指向言語のとらえ方にある.現存するアスペクト指向言語は,既存の言語に対して拡張を施すことによって作成されている.一方,既存研究ではアスペクト指向言語を1) ラムダ計算のような既存の計算体系にアスペクト指向を加えたもの,または2) 言語全体を記述する体系で定式化している.それに対し,本研究では2) と同様に既存の計算体系に依存せずにアスペクト指向としての操作の定式化のみを行い,他の体系との組合せによって1のように言語を表現する.本発表では,アスペクト指向における操作の定式化と,ラムダ計算との組合せによる言語の定式化,および他研究における議論の表現について述べる.Aspect-orientation has gained in software development in the last decade. However, formal and/or general definitions of aspects and related concepts are not thoroughly discussed so far. The important concepts such as aspect, join point, pointcut, advice, etc. are defined on top of specific aspect-oriented languages such as AspectJ. Our goal is to formalize some'aspectual'operations commonly used in aspect-oriented languages. We designed a simple calculus that models the operations independently from other computational activities such as function application or message passing. We can easily construct a model of a specific aspect-oriented language by mixing our calculus with another model that represents the base computation. In this presentation, we give a formalization of the aspectual operations in our calculus and then discuss the formalization by comparing to other works.