WEKO3
アイテム
定理証明システムCoq上でのPre Logical Relationを用いた詳細化の正しさの証明
https://ipsj.ixsq.nii.ac.jp/records/16856
https://ipsj.ixsq.nii.ac.jp/records/168566ff826d6-76ba-42cd-96c9-3e798e27a7b5
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO4211018.pdf (36.0 kB)
|
Copyright (c) 2001 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2001-11-15 | |||||||
| タイトル | ||||||||
| タイトル | 定理証明システムCoq上でのPre Logical Relationを用いた詳細化の正しさの証明 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Proof Method of Correctness of Refinement with Pre - Logical Relation on Coq | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 発表概要 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 京都大学大学院情報学研究科 | ||||||||
| 著者所属 | ||||||||
| 京都大学大学院情報学研究科 | ||||||||
| 著者所属 | ||||||||
| 京都大学大学院情報学研究科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者名 |
永山, 友和
× 永山, 友和
|
|||||||
| 著者名(英) |
Tomokazu, Nagayama
× Tomokazu, Nagayama
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 仕様からプログラムを開発する際，抽象的な仕様を具体的なプログラムへ変換することが行われている．抽象的な仕様には，用いるプログラミング言語では与えられていないデータ構造が含まれている可能性があり，具体的なプログラムとは，それらのデータ構造が実現されたプログラムである．このような変換のことを“詳細化”と呼ぶ．Honsellは，Pre Logical Relationを用いる，詳細化の正しさの証明技法を提案した．本研究では，定理証明システムCoqを用いて彼らの技法を形式化した．このことより，計算機上でプログラムの詳細化の正しさを厳密に証明することができる． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 42, 号 SIG11(PRO12), p. 100-100, 発行日 2001-11-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
