权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

プログラム抽出法の新展開　－－　証明自動化と高性能の両立

程序提取方法新进展——实现证明自动化与高性能

基本信息

批准号：
17J01683
负责人：
坂口和彦
金额：
$ 1.79万
依托单位：
University of Tsukuba
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2017
资助国家：
日本
起止时间：
2017-04-26 至 2020-03-31
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17J01683/
关键词：
対話的定理証明器プログラム抽出 Coq 形式検証

项目摘要

(1) 前年度に引き続き FLOPS 2018 の採録論文の論文誌版の改訂を行い、Science of Computer Programming (Elsevier) に採録となった。当該改訂の過程で、表現の問題のみならず技術的な面での改善を行った。特に顕著なものとしては、「定理証明器 Coq の効率的な有限ドメイン関数ライブラリ」（情報処理学会論文誌プログラミング）で提案したMathematical Components の方式・習慣に従って書かれた既存の形式証明ライブラリを、それを使う証明との互換性を維持しつつ変更する技法を、理論的裏付けがより明らかな形で改善したことが挙げられる。(2) 前年度に引き続き、各種量化子除去アルゴリズムの形式検証に向けて、Mathematical Components ライブラリに order ライブラリを取り込み、numeric domain/field の補題を整理した。これらの変更はすでに Mathematical Components 1.11.0 の一部としてリリースされている。また、それらに加えて区間に関する定義や補題の一般化に取り組み、束上の区間の集合が包含関係、共通部分、凸包について束をなすこと、また同様に全順序集合上の区間の集合が分配束をなすことを証明した。これによって、区間の包含関係に関する命題を、束論の問題に帰着して示すことが可能となった。(3) 上述の(2)の過程で Mathematical Components の代数構造の階層に新しい構造を追加する上での技術的問題を見出し、packed classes の形式で記述された代数構造の階層の実装上の誤りを検出するアルゴリズムを提案し、それを実際に使える検証ツールとして実装した。また、より高レベルな代数構造の定義の記述から packed classes の形式での定義を自動生成するためのツールの開発を行った。

(1) in the previous year, FLOPS 2018 was quoted, and the version of the text was revised, and Science of Computer Programming (Elsevier) was published. When it is time to improve the process and address the problem, the technical problems should be improved. This is a special introduction to the introduction of a limited number of information on the Coq rate of the Theorem Exhibitor. The proposal is to use the Mathematical Components method to improve the existing form of the device, to make it clear that it is interoperable, and to maintain a better understanding of techniques. In the theory, there is a clear understanding of how to improve the shape of the economy. (2) in the previous year, the quantifiers were introduced, and the quantifiers were removed in the form of Mathematical Components, order, and numeric domain/field. Please tell me more about the movie Mathematical Components 1.11.0. The general definition of the problem is that the cluster collection on the cluster includes the cluster, the common part, the convex cluster, the cluster cluster, and the cluster distribution cluster on the whole sequence set. There are many problems in the zone, such as the discussion and discussion of the problem, which indicates that the problem may be affected. (3) in the above Mathematical Components algebra system, the problem of adding new technology to the system has been found, and it is described in the form of packed classes that the system algebra has been installed with error equipment, and that the system has been installed in error mode. High-level computer algebra defines the definition of the system, and the packed classes form defines the automatic generation of the automatic generation system.