著者

片山 卓也 島津 明 東条 敏 二木 厚吉 緒方 和博 有本 泰仁 落水 浩一郎 早坂 良

出版者

JAIST Press

巻号頁・発行日

vol.2, 2007-09

---

法令工学は,法令文書の作成や変更,法令実働化情報システムの構築を系統的に行うため,人工知能,言語処理,ソフトウェア工学の研究成果を使おうとする工学的アプローチであり,21 世紀COEプログラム「検証進化可能電子社会」の主要研究課題の一つである.安心な電子社会の実現には,電子社会の仕様書である法令を適切に作成し,それを施行する情報システムを正しく構築しなければならない.また,法令の改定に対しては,関係法令への変更伝播を整合的に行い,それを情報システムへの変更に矛盾なくつなげる必要がある.法令工学は,このような問題を工学的に解決することめざして,本COEで世界で初めて提案されたものである.現在,企業活動における法令尊守などが大きな社会問題として取り上げられているが,組織における規則の作成や尊守機構の設計なども法令工学の範疇に入ると考えられ,今後訪れる本格的な電子社会時代において,安心で公正な社会や組織の設計や実現に,法令工学はその基本技術を提供するものであると考えている.本書は,本COEにおける法令工学の研究活動を紹介するために書かれたものであるが,各章の著者は以下のようである.第1章 片山卓也 第2章 島津明 第3章 東条敏 第4章 二木厚吉,緒方和博,有本泰仁 第5章 落水浩一郎,早坂良

著者

二木 厚吉 大堀 淳 柴山 悦哉 安村 通晃 竹内 郁雄 上田 和紀 村井 純 萩谷 昌己

出版者

一般社団法人情報処理学会

雑誌

情報処理 (ISSN:04478053)

巻号頁・発行日

vol.33, no.3, pp.272-289, 1992-03-15

被引用文献数

1

著者

金藤 栄孝 二木 厚吉

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:03875806)

巻号頁・発行日

vol.45, no.3, pp.770-784, 2004-03-15

---

Dijkstraのgoto文有言説とそれに引き続く構造的プログラミングの提唱以降,goto文の使用に関する問題は長く議論されてきたが,coto文の使用法に関しての理論的裏付けを持つ研究としては,逐次的プログラムの制御フローは3基本構造(順次接続,条件分岐,反復)のみで表現可能であるからgoto文を用いたプログラムは3基本構造のみによる等価なプログラムに書き換えられる,という結果に基づいたMillsらのgoto文排斥論以外は皆無であり,Dijkstra本来のプログラムの正しさを示す手段としてのプログラムの構造化という観点でのgoto文の使用の是非は,プログラム検証論の立場から考察されなかった.本論文では,プログラムの正しさを示すという検証手段としてのHoare論理に基づきgoto文の使用を再検討する.特に,多重ループの打ち切りの場合,goto文を用いて脱出するプログラミングスタイルの方が,Mills流のBoolean型変数を追加してループを打ち切るスタイルよりも,Hoare論理での証明アウトラインが簡単に構成でき,したがって,前者のgoto文を用いたプログラミングスタイルの方が,そのようなプログラムに対するHoare論理による検証上からは望ましいことを示す. : There have been a vast amount of debates on the issue on usages of goto statements initiated by the famous Dijkstra's Letter to the Editor of CACM and his proposal of "Structured Programming". Except for the goto-less programming style by Mills based on the fact that any control nows of sequential programs can be expressed by the sequential composition, the conditional (if-then-else) and the indefinite loop (while), there have not been, however, any scientific accounts on this issue from the Dijkstra's own viewpoint of verifiability of programs. In this work, we reconsider this issue from the viewpoint of Hoare Logic, the most standard framework for proving the correctness of programs, and we see that usages of goto's in escaping from nested loops can be justified from the Hoare Logic viewpoint by showing the fact that constructing the proof-outline of a program using a goto for this purpose is gasier than constructing the proof-outline of a Mills-style program without goto by introducing a new Boolean variable.

著者

二木 厚吉 Kokichi Futatsugi 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST).

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.13, no.1, pp.4-22, 1996-01-16

参考文献数

18

被引用文献数

5

著者

二木 厚吉

出版者

一般社団法人情報処理学会

雑誌

情報処理 (ISSN:04478053)

巻号頁・発行日

vol.28, no.7, pp.p906-912, 1987-07-15

著者

金藤栄孝 二木厚吉

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.45, no.3, pp.770-784, 2004-03-15

被引用文献数

1

---

Dijkstraのgoto文有害説とそれに引き続く構造的プログラミングの提唱以降,goto文の使用に関する問題は長く議論されてきたが,goto文の使用法に関しての理論的裏付けを持つ研究としては,逐次的プログラムの制御フローは3基本構造(順次接続,条件分岐,反復)のみで表現可能であるからgoto文を用いたプログラムは3基本構造のみによる等価なプログラムに書き換えられる,という結果に基づいたMillsらのgoto文排斥論以外は皆無であり,Dijkstra本来のプログラムの正しさを示す手段としてのプログラムの構造化という観点でのgoto文の使用の是非は,プログラム検証論の立場から考察されなかった.本論文では,プログラムの正しさを示すという検証手段としてのHoare論理に基づきgoto文の使用を再検討する.特に,多重ループの打ち切りの場合,goto文を用いて脱出するプログラミングスタイルの方が,Mills流のBoolean型変数を追加してループを打ち切るスタイルよりも,Hoare論理での証明アウトラインが簡単に構成でき,したがって,前者のgoto文を用いたプログラミングスタイルの方が,そのようなプログラムに対するHoare論理による検証上からは望ましいことを示す.There have been a vast amount of debates on the issue on usages of goto statements initiated by the famous Dijkstra's Letter to the Editor of CACM and his proposal of ``Structured Programming''.Except for the goto-less programming style by Mills based on the fact that any control flows of sequential programs can be expressed by the sequential composition, the conditional (If-Then-Else)and the indefinite loop (While), there have not been, however, any scientific accounts on this issuefrom the Dijkstra's own viewpoint of verifiability of programs.In this work, we reconsider this issue from the viewpoint of Hoare Logic,the most standard framework for proving the correctness of programs, and we see that usages of goto's in escaping from nested loops can be justified from the Hoare Logic viewpoint by showing the fact that constructing the proof-outline of a program using a goto for this purpose is easier than constructing the proof-outline of a Mills-style program without goto by introducing a new Boolean variable.

著者

渡辺 真啓 中村 正樹 二木 厚吉

出版者

FIT(電子情報通信学会・情報処理学会)運営委員会

雑誌

情報科学技術フォーラム一般講演論文集

巻号頁・発行日

vol.3, no.1, pp.173-174, 2004-08-20

著者

石川 洋 二木 厚吉 渡部 卓雄

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス

巻号頁・発行日

vol.98, no.295, pp.23-30, 1998-09-22

被引用文献数

3

---

並行システムの動作の詳細を把握するのは一般的には困難である.本研究では, 並行システムの例として有機的プログラミング言語GAEAをとりあげる.本言語は有機的プログラミングと呼ばれる新しいソフトウェア構築方法論に基づいておりプログラムの動的変更や並行処理が可能である.この言語はPrologを基礎としてるので並列論理型プログラミング言語と考えることができる.そこで本言語は並行システムとみなし, そのシステムの計算状態や動作の明示的な記述を試みている.その記述は状態を持つ並行システムの動的変化が表現可能な書き換え論理を用いて与えている.

著者

原 光太朗 緒方 和博 中村 正樹 二木 厚吉

出版者

FIT(電子情報通信学会・情報処理学会)運営委員会

雑誌

情報科学技術フォーラム一般講演論文集

巻号頁・発行日

vol.3, no.1, pp.177-178, 2004-08-20

著者

鳥居 宏次 二木 厚吉 真野 芳久

出版者

一般社団法人情報処理学会

雑誌

情報処理 (ISSN:04478053)

巻号頁・発行日

vol.20, no.1, pp.p22-43, 1979-01-15

著者

金藤栄孝 二木 厚吉

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.45, no.9, pp.2124-2137, 2004-09-15

---

Dijkstraのgoto文有害説とそれに引き続く構造的プログラミングの提唱以降,goto文の使用に関する問題は永く議論された.goto文の使用法に関し理論的裏付けを持つ研究としては,逐次的プログラムでの任意の制御フローは順次接続・条件分岐・反復の3基本構造のみで表現可能であるという結果に基づくMillsらのgoto文排斥論以外は皆無である.Dijkstra本来の正しさを示しやすいプログラムを書くための構造化という立場?つまりプログラム検証論の立場?からのgoto文使用の是非は考察されていない.本論文では検証手段としてのHoare論理に基づき有限状態機械モデルに基づくプログラミングでのgoto文の使用を検討する.その結果,状態をラベルで表し状態遷移をgoto文での飛び越しで行うプログラミングスタイルが,状態を表す変数を追加しgoto文を除いたプログラミングスタイルと比べ,Hoare論理による検証での表明が簡単で自然な形となり機械的検証の時間的コストも少ない.ゆえにプログラムの正しさの示しやすさという観点からは有限状態機械モデルに基づくプログラミングでの状態変数導入によるgoto文除去は有害でありgoto文を用いたスタイルの方が望ましいことを示す.There have been a vast amount of debates on the issue on the use of goto statements initiated by the famous Dijkstra's Letter to the Editor of CACM and his proposal of "Structured Programming". Except for the goto-less programming style by Mills based on the fact that any control flows of sequential programs can be expressed by the sequential composition, the conditional (if-then-else) and the indefinite loop (while), there have not been, however, any scientific accounts on this issue from the Dijkstra's own viewpoint of verifiability of programs. In this work, we reconsider this issue from the viewpoint of Hoare Logic, the most standard framework for correctness-proving, and we see that the use of goto's for expressing state transitions in programs designed with the finite state machine modelling can be justified from the Hoare Logic viewpoint by showing the fact that constructing the proof-outline of a program using goto's for this purpose is easier than constructing the proof-outline of a Mills-style program without goto by introducing a new variable.

著者

金藤栄孝 二木厚吉

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.45, no.3, pp.770-784, 2004-03-15

---

Dijkstraのgoto文有害説とそれに引き続く構造的プログラミングの提唱以降,goto文の使用に関する問題は長く議論されてきたが,goto文の使用法に関しての理論的裏付けを持つ研究としては,逐次的プログラムの制御フローは3基本構造(順次接続,条件分岐,反復)のみで表現可能であるからgoto文を用いたプログラムは3基本構造のみによる等価なプログラムに書き換えられる,という結果に基づいたMillsらのgoto文排斥論以外は皆無であり,Dijkstra本来のプログラムの正しさを示す手段としてのプログラムの構造化という観点でのgoto文の使用の是非は,プログラム検証論の立場から考察されなかった.本論文では,プログラムの正しさを示すという検証手段としてのHoare論理に基づきgoto文の使用を再検討する.特に,多重ループの打ち切りの場合,goto文を用いて脱出するプログラミングスタイルの方が,Mills流のBoolean型変数を追加してループを打ち切るスタイルよりも,Hoare論理での証明アウトラインが簡単に構成でき,したがって,前者のgoto文を用いたプログラミングスタイルの方が,そのようなプログラムに対するHoare論理による検証上からは望ましいことを示す.

著者

二木 厚吉 外山 芳人

雑誌

情報処理

巻号頁・発行日

vol.24, no.2, 1983-02-15

著者

二木 厚吉 緒方 和博 中村 正樹 Kokichi Futatsugi Kazuhiro Ogata Masaki Nakamura 北陸先端科学技術大学院大学情報科学研究科 北陸先端科学技術大学院大学情報科学研究科 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.25, no.2, pp.1-13, 2008-04-24

参考文献数

6

被引用文献数

3

---

CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する.第2回以降では,言語の構文と意味(第2回),等式推論と項書換システム(第3回)について説明し,証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する.さらに,認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する.The formal method, or the method for writing and verifying formal specifications, with the CafeOBJ language system is described in a series of six tutorials. The CafeOBJ language is a most advanced formal specification language which extents the OBJ language, and behavioral, rewriting, and parameterized specifications can be written in it. The CafeOBJ language system can simulate equational reasoning by executing equations as rewrite rules, and be used as an interactive verification system. This first tutorial presents an overview of the CafeOBJ formal method by using an example of "mutual exclusion protocol with a waiting queue" without getting into details of the language and the verification technique. In the following tutorials, the language and its semantics (2nd tutorial), equational reasoning and term rewriting systems (3rd tutorial) are presented, and the CafeOBJ's verification method with proof scores which only uses reductions (4th tutorial) is explained. Furthermore, CafeOBJ's verifications of an authentication protocol (5th tutorial) and a communication protocol (6th tutorial) are also presented, and several verification techniques are explained.

著者

泉田 大宗 森 彰 二木 厚吉

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.29, no.4, pp.4_199-4_218, 2012-10-25 (Released:2012-11-25)

---

本稿では動的解析と静的解析を組み合わせたマルウェアの振る舞い解析手法について述べる.静的解析部ではバイナリコードを低レベルの記号式で解釈した上で静的単一代入形式に変換し,後方解析を行うことで間接ジャンプの行き先を可能な限り解決している.静的解析では解析しきれない制御フローに関しては動的解析によって補遺する.従来のバイナリコード解析手法ではC言語などの高級言語からコンパイルされたバイナリのみを対象としていたが,本手法ではマルウェアのようにそのような前提条件を満たさないバイナリも解析可能である.また,動的解析部としてハイパーバイザ機構を使った仮想環境を用いる試みについても述べる.

著者

二木 厚吉 緒方 和博 中村 正樹

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.25, no.2, pp.2_1-2_13, 2008 (Released:2008-06-30)

---

CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する.第2回以降では,言語の構文と意味(第2回),等式推論と項書換システム(第3回)について説明し,証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する.さらに,認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する.

著者

二木 厚吉 外山 芳人

出版者

一般社団法人情報処理学会

雑誌

情報処理 (ISSN:04478053)

巻号頁・発行日

vol.24, no.2, pp.p133-146, 1983-02-15

被引用文献数

21

著者

金藤 栄孝 二木 厚吉

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:03875806)

巻号頁・発行日

vol.45, no.9, pp.2124-2137, 2004-09-15

---

Dijkstraのgoto文有害説とそれに引き続く構造的プログラミングの提唱以降,goto文の使用に関する問題は永く議論された.goto文の使用法に関し理論的裏付けを持つ研究としては,逐次的プログラムでの任意の制御フローは順次接続・条件分岐・反復の3基本構追のみで表現可能であるという結果に基づくMillsらのgoto文排斥論以外は皆無である. Dijkstra本来の正しさを示しやすいプログラムを害くための構造化という立場一つまりプログラム検証論の立場-からのgoto文使用の是非は考察されていない.本論文では検証手段としてのHoare論理に基づき有限状態機械モデルに基づくプログラミングでのgoto文の使用を検討する.その結果,状態をラベルで表し状態遷移をgoto文での飛び越しで行うプログラミングスタイルが,状態を表す変数を追加しgoto文を除いたプログラミングスタイルと比べ. Hoare論理による検証での表明が簡単で自然な形となり機械的検証の時間的コストも少ない.ゆえにプログラムの正しさの示しやすさという観点からは有限状態機械モデルに基づくプログラミングでの状態変数導入によるgoto文除去は有害でありgoto文を用いたスタイルの方が望ましいことを示す. : There have been a vast amount of debates on the issue on the use of goto statements initiated by the famous Dijkstra's Letter to the Editor of CACM and his proposal of "Structured Programming". Except for the goto-less programming style by Mills based on the fact that any control flows of sequential programs can be expressed by the sequential composition, the conditional (if-then-else) and the indefinite loop (while), there have not been, however, any scientific accounts on this issue from the Dijkstra's own viewpoint of verifiability of programs. In this work, we reconsider this issue from the viewpoint of Hoare Logic, the most standard framework for correctness-proving, and we see that the use of goto's for expressing state transitions in programs designed with the finite state machine modelling can be justified from the Hoare Logic viewpoint by showing the fact that constructing the proof-outline of a program using goto's for this purpose is easier than constructing the proof-outline of a Mills-style program without goto by introducing a new variable.

著者

片山 卓也 島津 明 東条 敏 二木 厚吉 落水 浩一郎

出版者

社団法人人工知能学会

雑誌

人工知能学会誌 (ISSN:09128085)

巻号頁・発行日

vol.23, no.4, pp.529-536, 2008-07-01

被引用文献数

3

著者

松本 充広 二木 厚吉

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス (ISSN:09135685)

巻号頁・発行日

vol.101, no.98, pp.25-32, 2001-05-22

---

近年, ソフトウェアの生産性向上が期待できることから, コンポーネントを組合せる手法によるソフトウェア開発(コンポーネントソフトウェア開発)が普及し始めている. しかし, コンポーネントを再利用し生産性を向上させるには, コンポーネント作成者とソフトウェア作成者との間で, コンポーネントがどのような状況で使用され, どのような振舞いをするか等についての合意が形成されている必要がある. この合意形成を行う方法論として, カタルシス法がある. カタルシス法では, UML図+OCL記述を形いてビジネスモデル, ソフトウェア仕様を記述する. しかし, どの程度フォーマルに記述するべきかまでは定めていない. 本発表では, (1)仕様間の一貫性検証を行うためにどの程度フォーマルに記述すべきか, についてのガイドライン, (2)クラス図制約の検証手法, (3)ズームイン・ズームアウトの一貫性検証手法, (3)仕様からのコネクタ生成手法, について議論する.