著者

坂口 和彦 亀山 幸義

雑誌

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

巻号頁・発行日

vol.10, no.1, pp.14-28, 2017-01-06

---

本研究は,対話的定理証明器Coqの有限型と有限ドメイン関数に関する既存ライブラリを改良し,従来のライブラリを用いた証明をほとんど変更することなく,その証明から抽出されるプログラムの効率を大幅に改善したものである.CoqのSSReflect/Mathematical Componentsライブラリは,有限型と有限ドメイン関数をサポートするライブラリfintypeとfinfunを提供し,これらのデータに対する証明の手間を大幅に削減することに成功している.しかし,その証明からプログラム抽出の手法で作成したプログラムは,多くの場合において非常に効率が悪いという問題がある.本研究では,fintypeやfinfunを改善したライブラリを実装した.このライブラリを用いて作成した証明から抽出したOCamlコードは,既存ライブラリの場合と比べて非常に高速である.例として,行列積の計算では,計算時間をおよそO(n5)からO(n3)へ改善できたことを示す.また,既存のSSReflectライブラリを用いたCoqの証明は,ほとんど書き換えることなく本研究のライブラリを用いた証明となる.例として,GonthierらのFeit-Thompson定理の約17万行におよぶ形式証明が,わずか10行以下の修正で,本研究のライブラリを用いた証明にできたことを示す.

著者

高島 尚希 亀山 幸義

雑誌

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

巻号頁・発行日

vol.5, no.1, pp.27-27, 2012-03-28

---

本発表は,コントロールオペレータの表現力を解明すること,特に,捕捉される限定継続の範囲が入れ子になることを許すコントロールオペレータnested shift/resetを,入れ子を許さないコントロールオペレータcontrol/promptを用いて表現できることを厳密に示すことを目的とする.コントロールオペレータnested shift/resetは,よく知られているコントロールオペレータshift/resetに,タグを付加して拡張したものである.本研究の出発点は,独立に提案され研究されているnested shift/resetとcontrol/promptが,抽象機械のレベルでは非常に類似した構造を持つ,という観測である.この観測に基づき,抽象機械のレベルで前者を後者でシミュレートできることを証明する.この手法を拡張して,nested control/promptをcontrol/promptでシミュレートできることも示す.最後に,抽象機械をソースコードレベルに戻す変換を適用することにより,nested shift/resetやnested control/promptを,control/promptでマクロ定義可能であることを示す.本手法によるマクロ定義は,簡潔なデータ型を用いて実現され,多くの関数型言語でそのまま利用可能である.

著者

杉浦 啓介 亀山 幸義

雑誌

全国大会講演論文集

巻号頁・発行日

vol.第70回, no.ソフトウェア科学・工学, pp.303-304, 2008-03-13

著者

田中 陽 亀山 幸義

雑誌

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

巻号頁・発行日

vol.48, no.SIG12(PRO34), pp.67-67, 2007-08-15

---

本研究は、関数型言語 Scheme における動的環境と限定継続の共存について検討し、形式的意味論を定義し、それに基づく実装を与えたものである。動的環境はプログラム実行時に動的に決定される環境で、Scheme では、プログラム中の手続きが一定の動的環境を持つことを保証するための機構として、dynamic-wind が用意されている。限定継続は、「計算の残りの一部」のことである。Scheme の標準手続き call/cc が、「計算の残り」全体を操作するのに対して、本研究で扱う shift/reset はこの限定継続を操作し、種々の探索問題などがより簡潔に記述できるようになる。すでに知られているように、dynamic-wind と call/cc の共存は容易ではない。Scheme の仕様書 R5RS の形式的意味論はこれらの共存に対応しておらず、後の研究で修正された。我々は、shift/reset を Scheme に追加し、記述力を向上させる研究を行っている。本研究はその一環として、dynamic-wind と shift/reset の共存について取り組んだものである。まず、R5RS の表示的意味論を拡張して、shift/reset に対応した意味論を与える。次に、プログラムの実行が dynamic-wind の性質を保証することを示すために、その意味論に対応する抽象機械を導く。またあわせて、この意味論に基づいた Scheme インタプリタを作成し、shift/reset と dynamic-wind を含むプログラムが正しく動くことを確かめた。

著者

亀山 幸義

雑誌

全国大会講演論文集

巻号頁・発行日

vol.42, pp.47-48, 1991-02-25

---

我々の目的は、洗錬された論理体系に基づき、数学の定理やプログラムの性質の証明を計算機上で実行できる環境を構築し、ひとつのシステムの中で、定理証明やプログラムの合成、変換等を行うことである。ここで、基礎とする論理体系は構成的(直観主義的)なので、証明された定理に含まれるアルゴリズムを、プログラムの形で自動的に抽出することができる。従って、このシステムの中では、証明の作成作業はプログラミングと同一視できることになる。構成的数学の体系は、近年、プログラムのための論理として活発に研究されており、計算機上の実現の例も、Maztin-Lofの型理論に基づいたConstableらのNuprl[1]や、FefermanのT0に基づいた林のPX[2]などがある。また、我々も、上記の目的のために、体系SSTと関数型言語Aを用いたシステムを提案している[3]。本研究の主な特徴は、・論理体系に含まれるプログラム言語を用いて、証明システムを実現したため、システムの性質をそれ自身の中で論じることができる。・扱う対象は、普通の数学の定理だけでなく、超数学(証明論)の定理を自然に形式化し、証明することを含んでいる。という2点である。これらの騎徴を示す例として、Aの項に対するChuzh=Rosserの定理の証明をあげる。また、その他の超数学の定理の形式化について簡単にのべる。

著者

中島 一 亀山 幸義

出版者

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

雑誌

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

巻号頁・発行日

vol.45, no.12, pp.11-24, 2004-11-15

被引用文献数

2

---

本研究の目的は,抽象化・精密化の手法を用いて,実時間モデル検査の状態数爆発問題を解決することにある.実時間モデル検査は,実時間システムの検証に用いられる手法で,そのシステムを時間オートマトンで記述する.実時間モデル検査における状態数爆発問題は,探索する状態空間が,実数値をとるクロック変数の数に対し指数的に大きくなり,実用的な時間内で検査が終了しないというものである.抽象化・精密化に基づくモデル検査法では,抽象化によりクロック変数をすべて省いた,初期抽象システムを構築し検査する.しかし,このような抽象化では検証結果として,間違った結果すなわち偽物の反例を得てしまうことがある.その場合,初期抽象システムから抽象化のレベルを低くしたシステムに作り替え,検証をやり直す.これを,正しい結果が得られるまで繰り返す.この手法の最大の課題は,得られた反例を基に,抽象化のレベルが高くかつ検証可能なシステムをどのように作るかということである.提案手法では,取り除いた変数のうち必要なものを復元する精密化を行う.また状態数を抑えるため,システム全体に変数を復元するのではなく,部分的に復元する.さらにクロック変数を復元せず不必要な遷移を除去する,もう1 つの精密化を併用することで状態数の増加を抑える.本稿では,提案手法の適用例として時間オートマトンの到達可能性解析を試み,実験でその有効性の検証を行った.We address the state explosion problem in real-time model checking. Real-time model checking automatically verifies real-time systems described as timed automata. This method suffers from the state explosion problem: the size of the state space grows exponentially with the number of real-valued clock variables. We use abstraction-refinement for reducing the state space. Using this method, an initial abstract system, which is an over-approximation to behaviors of the timed automaton, is constructed by removing all clock variables, and then the abstract system is verified. This kind of conservative abstraction may lead to a false result, that is a spurious counterexample. In this case, the abstract system is refined on the basis of the counterexample and the refined system is verified. The process is repeated until a correct result is obtained. The difficulty in this method is how the system is refined. In our approach, we extract clock variables needed in the refinement. Additionally, we do not refine the whole system but a part of the system. Besides this refinement, we introduce another refinement removing transitions which are proved to never fire in the timed automaton. Our approach avoids the state explosion problem by combining these refinements. In this work, we apply our techniques to reachability analysis of timed automata.

著者

永山 友和 佐藤 雅彦 亀山 幸義

出版者

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

雑誌

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

巻号頁・発行日

vol.42, no.11, pp.100-100, 2001-11-15

---

仕様からプログラムを開発する際,抽象的な仕様を具体的なプログラムへ変換することが行われている.抽象的な仕様には,用いるプログラミング言語では与えられていないデータ構造が含まれている可能性があり,具体的なプログラムとは,それらのデータ構造が実現されたプログラムである.このような変換のことを"詳細化"と呼ぶ.Honsellは,Pre Logical Relationを用いる,詳細化の正しさの証明技法を提案した.本研究では,定理証明システムCoqを用いて彼らの技法を形式化した.このことより,計算機上でプログラムの詳細化の正しさを厳密に証明することができる.In developing programs form specifications, we transform abstract programs (specifications) into concrete programs. Abstract programs may have data, which are not available in our programming languages. In concrete programs, these data are represented by data which are provided. We call these transformation data refinement. Honsell suggest proof method of data refinement which use pre-logical relation. In this paper, we formalize their method with Coq. As a result, we can strictly prove the correctness of data refinement on computer.