{"created":"2021-03-01T06:26:30.817660+00:00","id":19054,"links":{},"metadata":{"_buckets":{"deposit":"798ee5f5-a25d-4c75-a34b-a44e8b84b441"},"_deposit":{"id":"19054","owners":[],"pid":{"revision_id":0,"type":"depid","value":"19054"},"status":"published"},"_oai":{"id":"oai:nagoya.repo.nii.ac.jp:00019054","sets":["312:313:314"]},"author_link":["55638","55639","55640","55641","55642","55643","55644","55645","55646","55647"],"item_10_alternative_title_19":{"attribute_name":"その他のタイトル","attribute_value_mlt":[{"subitem_alternative_title":"Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems","subitem_alternative_title_language":"en"}]},"item_10_biblio_info_6":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2008-09","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"2","bibliographicPageEnd":"121","bibliographicPageStart":"100","bibliographicVolumeNumber":"1","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌, プログラミング","bibliographic_titleLang":"ja"}]}]},"item_10_description_4":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"手続き型プログラムの検証手法として，モデル検査やホーア論理に基づく検証手法が代表的である．一方，項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている．本論文では，帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる．具体的には，自然数上のwhile言語で定義された手続き型関数からプレスブルガー文を規則の制約として持つことが許された制約付き項書換え系への変換を与え，その変換により手続き型プログラムの等価性を書換え系の関数の等価性に帰着させ，潜在帰納法を用いて等価性検証を試みる．この手法を実現するために，合流性を保証するための危険対定理および完備化手続きを制約付き書換えに対応するように拡張する．","subitem_description_language":"ja","subitem_description_type":"Abstract"},{"subitem_description":"In the field of procedural programming, several verification methods based on model checking or Hoare logic have been proposed. On the other hand, in the field of term rewriting, implicit induction and rewriting induction have been widely studied as methods for proving inductive theorems. In this paper, we try to take advantages of methods for proving inductive theorems in verifying procedural functions written in a \"while\" language with natural number type. More precisely, we propose a transformation from procedural programs to constrained term rewriting systems whose constraints are in Presburger arithmetic, and show that the transformation reduces the equivalence of procedural programs to that of functions in rewrite systems. By verifying the equivalence between rewrite systems, we verify the equivalence between the corresponding procedural functions. To establish this approach, we extend Critical Pair Theorem and the basic completion procedure for constrained systems.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_10_identifier_60":{"attribute_name":"URI","attribute_value_mlt":[{"subitem_identifier_type":"URI","subitem_identifier_uri":"http://id.nii.ac.jp/1001/00016440/"},{"subitem_identifier_type":"HDL","subitem_identifier_uri":"http://hdl.handle.net/2237/21160"}]},"item_10_publisher_32":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"一般社団法人情報処理学会","subitem_publisher_language":"ja"}]},"item_10_relation_43":{"attribute_name":"関連情報","attribute_value_mlt":[{"subitem_relation_type":"isVersionOf","subitem_relation_type_id":{"subitem_relation_type_id_text":"http://id.nii.ac.jp/1001/00016440/","subitem_relation_type_select":"URI"}}]},"item_10_rights_12":{"attribute_name":"権利","attribute_value_mlt":[{"subitem_rights":"ここに掲載した著作物の利用に関する注意 本著作物の著作権は情報処理学会に帰属します。本著作物は著作権者である情報処理学会の許可のもとに掲載するものです。ご利用に当たっては「著作権法」ならびに「情報処理学会倫理綱領」に従うことをお願いいたします。Notice for the use of this material The copyright of this material is retained by the Information Processing Society of Japan (IPSJ). This material is published on this web site with the agreement of the author (s) and the IPSJ. Please be complied with Copyright Law of Japan and the Code of Ethics of the IPSJ if any users wish to reproduce, make derivative work, distribute or make available to the public any part or whole thereof.<br/>All Rights Reserved, Copyright (C) Information Processing Society of Japan.<br/>Comments are welcome. Mail to address editj＠ipsj.or.jp, please.","subitem_rights_language":"ja"}]},"item_10_select_15":{"attribute_name":"著者版フラグ","attribute_value_mlt":[{"subitem_select_item":"publisher"}]},"item_10_source_id_7":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"0387-5806","subitem_source_identifier_type":"PISSN"}]},"item_1615787544753":{"attribute_name":"出版タイプ","attribute_value_mlt":[{"subitem_version_resource":"http://purl.org/coar/version/c_970fb48d4fbd8a85","subitem_version_type":"VoR"}]},"item_access_right":{"attribute_name":"アクセス権","attribute_value_mlt":[{"subitem_access_right":"open access","subitem_access_right_uri":"http://purl.org/coar/access_right/c_abf2"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"古市, 祐樹","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55638","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"西田, 直樹","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55639","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"酒井, 正彦","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55640","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"草刈, 圭一朗","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55641","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"坂部, 俊樹","creatorNameLang":"ja"}],"nameIdentifiers":[{"nameIdentifier":"55642","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Furuichi, Yuki","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55643","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Nishida, Naoki","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55644","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Sakai, Masahiko","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55645","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Kusakari, Keiichirou","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55646","nameIdentifierScheme":"WEKO"}]},{"creatorNames":[{"creatorName":"Sakabe, Toshiki","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"55647","nameIdentifierScheme":"WEKO"}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2018-02-21"}],"displaytype":"detail","filename":"IPSJ-TPRO0102009.pdf","filesize":[{"value":"431.7 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"IPSJ-TPRO0102009.pdf","objectType":"fulltext","url":"https://nagoya.repo.nii.ac.jp/record/19054/files/IPSJ-TPRO0102009.pdf"},"version_id":"837a2529-fa58-455a-a894-0ec633a7846b"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"journal article","resourceuri":"http://purl.org/coar/resource_type/c_6501"}]},"item_title":"制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み","subitem_title_language":"ja"}]},"item_type_id":"10","owner":"1","path":["314"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2015-01-29"},"publish_date":"2015-01-29","publish_status":"0","recid":"19054","relation_version_is_last":true,"title":["制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-16T04:08:01.240710+00:00"}