{"created":"2023-05-15T08:43:29.314198+00:00","id":8466,"links":{},"metadata":{"_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":["34: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":[{}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2017-03-13"}],"displaytype":"detail","filename":"1531033.pdf","filesize":[{"value":"784.2 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","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"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2017-03-13"},"publish_date":"2017-03-13","publish_status":"0","recid":"8466","relation_version_is_last":true,"title":["部分的なプログラムの変更を考慮した証明支援"],"weko_creator_id":"13","weko_shared_id":-1},"updated":"2023-09-12T06:06:41.322947+00:00"}