{"_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"}, "item_10_alternative_title_19": {"attribute_name": "\u305d\u306e\u4ed6\u306e\u8a00\u8a9e\u306e\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_alternative_title": "Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems"}]}, "item_10_biblio_info_6": {"attribute_name": "\u66f8\u8a8c\u60c5\u5831", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2008-09", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "2", "bibliographicPageEnd": "121", "bibliographicPageStart": "100", "bibliographicVolumeNumber": "1", "bibliographic_titles": [{"bibliographic_title": "\u60c5\u5831\u51e6\u7406\u5b66\u4f1a\u8ad6\u6587\u8a8c, \u30d7\u30ed\u30b0\u30e9\u30df\u30f3\u30b0"}]}]}, "item_10_description_4": {"attribute_name": "\u6284\u9332", "attribute_value_mlt": [{"subitem_description": "\u624b\u7d9a\u304d\u578b\u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u691c\u8a3c\u624b\u6cd5\u3068\u3057\u3066\uff0c\u30e2\u30c7\u30eb\u691c\u67fb\u3084\u30db\u30fc\u30a2\u8ad6\u7406\u306b\u57fa\u3065\u304f\u691c\u8a3c\u624b\u6cd5\u304c\u4ee3\u8868\u7684\u3067\u3042\u308b\uff0e\u4e00\u65b9\uff0c\u9805\u66f8\u63db\u3048\u306e\u5206\u91ce\u3067\u306f\u5e30\u7d0d\u7684\u5b9a\u7406\u306e\u8a3c\u660e\u624b\u6cd5\u3068\u3057\u3066\u6f5c\u5728\u5e30\u7d0d\u6cd5\u3084\u66f8\u63db\u3048\u5e30\u7d0d\u6cd5\u306a\u3069\u304c\u5e83\u304f\u7814\u7a76\u3055\u308c\u3066\u3044\u308b\uff0e\u672c\u8ad6\u6587\u3067\u306f\uff0c\u5e30\u7d0d\u7684\u5b9a\u7406\u306e\u8a3c\u660e\u6cd5\u3092\u5229\u7528\u3057\u3066\u624b\u7d9a\u304d\u578b\u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u7b49\u4fa1\u6027\u306e\u691c\u8a3c\u3092\u8a66\u307f\u308b\uff0e\u5177\u4f53\u7684\u306b\u306f\uff0c\u81ea\u7136\u6570\u4e0a\u306ewhile\u8a00\u8a9e\u3067\u5b9a\u7fa9\u3055\u308c\u305f\u624b\u7d9a\u304d\u578b\u95a2\u6570\u304b\u3089\u30d7\u30ec\u30b9\u30d6\u30eb\u30ac\u30fc\u6587\u3092\u898f\u5247\u306e\u5236\u7d04\u3068\u3057\u3066\u6301\u3064\u3053\u3068\u304c\u8a31\u3055\u308c\u305f\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u3078\u306e\u5909\u63db\u3092\u4e0e\u3048\uff0c\u305d\u306e\u5909\u63db\u306b\u3088\u308a\u624b\u7d9a\u304d\u578b\u30d7\u30ed\u30b0\u30e9\u30e0\u306e\u7b49\u4fa1\u6027\u3092\u66f8\u63db\u3048\u7cfb\u306e\u95a2\u6570\u306e\u7b49\u4fa1\u6027\u306b\u5e30\u7740\u3055\u305b\uff0c\u6f5c\u5728\u5e30\u7d0d\u6cd5\u3092\u7528\u3044\u3066\u7b49\u4fa1\u6027\u691c\u8a3c\u3092\u8a66\u307f\u308b\uff0e\u3053\u306e\u624b\u6cd5\u3092\u5b9f\u73fe\u3059\u308b\u305f\u3081\u306b\uff0c\u5408\u6d41\u6027\u3092\u4fdd\u8a3c\u3059\u308b\u305f\u3081\u306e\u5371\u967a\u5bfe\u5b9a\u7406\u304a\u3088\u3073\u5b8c\u5099\u5316\u624b\u7d9a\u304d\u3092\u5236\u7d04\u4ed8\u304d\u66f8\u63db\u3048\u306b\u5bfe\u5fdc\u3059\u308b\u3088\u3046\u306b\u62e1\u5f35\u3059\u308b\uff0eIn 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_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": "\u51fa\u7248\u8005", "attribute_value_mlt": [{"subitem_publisher": "\u4e00\u822c\u793e\u56e3\u6cd5\u4eba\u60c5\u5831\u51e6\u7406\u5b66\u4f1a"}]}, "item_10_rights_12": {"attribute_name": "\u6a29\u5229", "attribute_value_mlt": [{"subitem_rights": "\u3053\u3053\u306b\u63b2\u8f09\u3057\u305f\u8457\u4f5c\u7269\u306e\u5229\u7528\u306b\u95a2\u3059\u308b\u6ce8\u610f \u672c\u8457\u4f5c\u7269\u306e\u8457\u4f5c\u6a29\u306f\u60c5\u5831\u51e6\u7406\u5b66\u4f1a\u306b\u5e30\u5c5e\u3057\u307e\u3059\u3002\u672c\u8457\u4f5c\u7269\u306f\u8457\u4f5c\u6a29\u8005\u3067\u3042\u308b\u60c5\u5831\u51e6\u7406\u5b66\u4f1a\u306e\u8a31\u53ef\u306e\u3082\u3068\u306b\u63b2\u8f09\u3059\u308b\u3082\u306e\u3067\u3059\u3002\u3054\u5229\u7528\u306b\u5f53\u305f\u3063\u3066\u306f\u300c\u8457\u4f5c\u6a29\u6cd5\u300d\u306a\u3089\u3073\u306b\u300c\u60c5\u5831\u51e6\u7406\u5b66\u4f1a\u502b\u7406\u7db1\u9818\u300d\u306b\u5f93\u3046\u3053\u3068\u3092\u304a\u9858\u3044\u3044\u305f\u3057\u307e\u3059\u3002Notice 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.\nAll Rights Reserved, Copyright (C) Information Processing Society of Japan.\nComments are welcome. Mail to address editj\uff20ipsj.or.jp, please."}]}, "item_10_select_15": {"attribute_name": "\u8457\u8005\u7248\u30d5\u30e9\u30b0", "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": "ISSN"}]}, "item_creator": {"attribute_name": "\u8457\u8005", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "\u53e4\u5e02, \u7950\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "55638", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u897f\u7530, \u76f4\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "55639", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u9152\u4e95, \u6b63\u5f66"}], "nameIdentifiers": [{"nameIdentifier": "55640", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u8349\u5208, \u572d\u4e00\u6717"}], "nameIdentifiers": [{"nameIdentifier": "55641", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "\u5742\u90e8, \u4fca\u6a39"}], "nameIdentifiers": [{"nameIdentifier": "55642", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Furuichi, Yuki"}], "nameIdentifiers": [{"nameIdentifier": "55643", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Nishida, Naoki"}], "nameIdentifiers": [{"nameIdentifier": "55644", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Sakai, Masahiko"}], "nameIdentifiers": [{"nameIdentifier": "55645", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Kusakari, Keiichirou"}], "nameIdentifiers": [{"nameIdentifier": "55646", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Sakabe, Toshiki"}], "nameIdentifiers": [{"nameIdentifier": "55647", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "\u30d5\u30a1\u30a4\u30eb\u60c5\u5831", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2018-02-21"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "IPSJ-TPRO0102009.pdf", "filesize": [{"value": "431.7 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 431700.0, "url": {"label": "IPSJ-TPRO0102009.pdf", "url": "https://nagoya.repo.nii.ac.jp/record/19054/files/IPSJ-TPRO0102009.pdf"}, "version_id": "837a2529-fa58-455a-a894-0ec633a7846b"}]}, "item_language": {"attribute_name": "\u8a00\u8a9e", "attribute_value_mlt": [{"subitem_language": "jpn"}]}, "item_resource_type": {"attribute_name": "\u8cc7\u6e90\u30bf\u30a4\u30d7", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306e\u6f5c\u5728\u5e30\u7d0d\u6cd5\u3092\u5229\u7528\u3057\u305f\u624b\u7d9a\u304d\u578b\u30d7\u30ed\u30b0\u30e9\u30e0\u691c\u8a3c\u306e\u8a66\u307f", "item_titles": {"attribute_name": "\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_title": "\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306e\u6f5c\u5728\u5e30\u7d0d\u6cd5\u3092\u5229\u7528\u3057\u305f\u624b\u7d9a\u304d\u578b\u30d7\u30ed\u30b0\u30e9\u30e0\u691c\u8a3c\u306e\u8a66\u307f"}]}, "item_type_id": "10", "owner": "1", "path": ["312/313/314"], "permalink_uri": "http://hdl.handle.net/2237/21160", "pubdate": {"attribute_name": "\u516c\u958b\u65e5", "attribute_value": "2015-01-29"}, "publish_date": "2015-01-29", "publish_status": "0", "recid": "19054", "relation": {}, "relation_version_is_last": true, "title": ["\u5236\u7d04\u4ed8\u304d\u9805\u66f8\u63db\u3048\u7cfb\u306e\u6f5c\u5728\u5e30\u7d0d\u6cd5\u3092\u5229\u7528\u3057\u305f\u624b\u7d9a\u304d\u578b\u30d7\u30ed\u30b0\u30e9\u30e0\u691c\u8a3c\u306e\u8a66\u307f"], "weko_shared_id": null}