WEKO3
アイテム
{"_buckets": {"deposit": "009cbcf0-0bcc-481c-a491-e33396dcacfd"}, "_deposit": {"created_by": 13, "id": "8466", "owners": [13], "pid": {"revision_id": 0, "type": "depid", "value": "8466"}, "status": "published"}, "_oai": {"id": "oai:uec.repo.nii.ac.jp:00008466", "sets": ["173"]}, "author_link": ["23006"], "control_number": "8466", "item_10006_date_granted_11": {"attribute_name": "学位授与年月日", "attribute_value_mlt": [{"subitem_dategranted": "2017-03-24"}]}, "item_10006_degree_grantor_9": {"attribute_name": "学位授与機関", "attribute_value_mlt": [{"subitem_degreegrantor": [{"subitem_degreegrantor_name": "電気通信大学"}]}]}, "item_10006_degree_name_8": {"attribute_name": "学位名", "attribute_value_mlt": [{"subitem_degreename": "修士"}]}, "item_10006_description_10": {"attribute_name": "学位授与年度", "attribute_value_mlt": [{"subitem_description": "2016", "subitem_description_type": "Other"}]}, "item_10006_description_7": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "プログラムの任意の性質を保証し,バグのないプログラムを開発するために,Coqなどの証明支援系と呼ばれるソフトウェアを用いる方法がある.Coqを用いて性質を保証したプログラムを開発する方法には,2通りの方法がある.1つ目はCoq上にプログラムを直接記述し,証明を行い,他言語へ変換する方法.2つ目は他言語で記述されたプログラムをCoqプログラムへ変換し,証明を行う方法である.しかし,どちらの方法であっても単方向の変換のみ行うため,前者の方法では他言語を直接変更できないため仕様が決定できず,後者の方法では証明を行いやすいようにCoq上でプログラムへ変更を加えることができない,という問題点がある.\n 本研究では,この問題を解決するため,OCamlプログラムとCoqプログラムの双方向の変換を可能とするシステムを提案する.これにより,OCamlプログラムの変更をCoqプログラムへ反映することで,OCaml側で仕様が決定できると同時に,証明を行いやすくするためにCoq側でプログラムに加えた変更を,OCamlプログラムへ反映することができる.さらに,変更前のCoqプログラムを利用し,差分の小さいCoqプログラムを生成することで,以前の証明を部分的に再利用できることが期待される.また,OCamlのListモジュールを本システムで変換することで,Coqで扱うことのできる構文に変換されるOCamlプログラムに対し,対応していることを示した.", "subitem_description_type": "Abstract"}]}, "item_10006_text_22": {"attribute_name": "専攻", "attribute_value_mlt": [{"subitem_text_value": "情報理工学研究科"}, {"subitem_text_value": "情報・通信工学専攻"}]}, "item_10006_version_type_18": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_ab4af688f83e57aa", "subitem_version_type": "AM"}]}, "item_creator": {"attribute_name": "著者", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "木下, 大輔", "creatorNameLang": "ja"}, {"creatorName": "キノシタ, ダイスケ", "creatorNameLang": "ja-Kana"}], "nameIdentifiers": [{"nameIdentifier": "23006", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2017-03-13"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "1531033.pdf", "filesize": [{"value": "784.2 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 784200.0, "url": {"label": "1531033", "url": "https://uec.repo.nii.ac.jp/record/8466/files/1531033.pdf"}, "version_id": "cdd7da39-49bc-4c54-9229-6c61dbf9dd54"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "thesis", "resourceuri": "http://purl.org/coar/resource_type/c_46ec"}]}, "item_title": "部分的なプログラムの変更を考慮した証明支援", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "部分的なプログラムの変更を考慮した証明支援", "subitem_title_language": "ja"}]}, "item_type_id": "10006", "owner": "13", "path": ["173"], "permalink_uri": "https://uec.repo.nii.ac.jp/records/8466", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2017-03-13"}, "publish_date": "2017-03-13", "publish_status": "0", "recid": "8466", "relation": {}, "relation_version_is_last": true, "title": ["部分的なプログラムの変更を考慮した証明支援"], "weko_shared_id": -1}
部分的なプログラムの変更を考慮した証明支援
https://uec.repo.nii.ac.jp/records/8466
https://uec.repo.nii.ac.jp/records/8466333cb836-ee38-47cc-9004-717e285ed7ae
名前 / ファイル | ライセンス | アクション |
---|---|---|
1531033 (784.2 kB)
|
|
Item type | 学位論文 / Thesis or Dissertation(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2017-03-13 | |||||
タイトル | ||||||
言語 | ja | |||||
タイトル | 部分的なプログラムの変更を考慮した証明支援 | |||||
言語 | ||||||
言語 | jpn | |||||
資源タイプ | ||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_46ec | |||||
資源タイプ | thesis | |||||
著者 |
木下, 大輔
× 木下, 大輔 |
|||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | プログラムの任意の性質を保証し,バグのないプログラムを開発するために,Coqなどの証明支援系と呼ばれるソフトウェアを用いる方法がある.Coqを用いて性質を保証したプログラムを開発する方法には,2通りの方法がある.1つ目はCoq上にプログラムを直接記述し,証明を行い,他言語へ変換する方法.2つ目は他言語で記述されたプログラムをCoqプログラムへ変換し,証明を行う方法である.しかし,どちらの方法であっても単方向の変換のみ行うため,前者の方法では他言語を直接変更できないため仕様が決定できず,後者の方法では証明を行いやすいようにCoq上でプログラムへ変更を加えることができない,という問題点がある. 本研究では,この問題を解決するため,OCamlプログラムとCoqプログラムの双方向の変換を可能とするシステムを提案する.これにより,OCamlプログラムの変更をCoqプログラムへ反映することで,OCaml側で仕様が決定できると同時に,証明を行いやすくするためにCoq側でプログラムに加えた変更を,OCamlプログラムへ反映することができる.さらに,変更前のCoqプログラムを利用し,差分の小さいCoqプログラムを生成することで,以前の証明を部分的に再利用できることが期待される.また,OCamlのListモジュールを本システムで変換することで,Coqで扱うことのできる構文に変換されるOCamlプログラムに対し,対応していることを示した. |
|||||
学位名 | ||||||
学位名 | 修士 | |||||
学位授与機関 | ||||||
学位授与機関名 | 電気通信大学 | |||||
学位授与年度 | ||||||
内容記述タイプ | Other | |||||
内容記述 | 2016 | |||||
学位授与年月日 | ||||||
学位授与年月日 | 2017-03-24 | |||||
著者版フラグ | ||||||
出版タイプ | AM | |||||
出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa | |||||
専攻 | ||||||
情報理工学研究科 | ||||||
専攻 | ||||||
情報・通信工学専攻 |