ログイン
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

{"_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": ["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.\u003cbr/\u003eAll Rights Reserved, Copyright (C) Information Processing Society of Japan.\u003cbr/\u003eComments 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", "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_note", "mimetype": "application/pdf", "size": 431700.0, "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"], "permalink_uri": "http://hdl.handle.net/2237/21160", "pubdate": {"attribute_name": "PubDate", "attribute_value": "2015-01-29"}, "publish_date": "2015-01-29", "publish_status": "0", "recid": "19054", "relation": {}, "relation_version_is_last": true, "title": ["制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み"], "weko_shared_id": -1}
  1. A500 情報学部/情報学研究科・情報文化学部・情報科学研究科
  2. A500a 雑誌掲載論文
  3. 学術雑誌

制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み

http://hdl.handle.net/2237/21160
http://hdl.handle.net/2237/21160
40041e60-21a5-4d33-94db-421316622690
名前 / ファイル ライセンス アクション
IPSJ-TPRO0102009.pdf IPSJ-TPRO0102009.pdf (431.7 kB)
Item type 学術雑誌論文 / Journal Article(1)
公開日 2015-01-29
タイトル
タイトル 制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み
言語 ja
その他のタイトル
その他のタイトル Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems
言語 en
著者 古市, 祐樹

× 古市, 祐樹

WEKO 55638

ja 古市, 祐樹

Search repository
西田, 直樹

× 西田, 直樹

WEKO 55639

ja 西田, 直樹

Search repository
酒井, 正彦

× 酒井, 正彦

WEKO 55640

ja 酒井, 正彦

Search repository
草刈, 圭一朗

× 草刈, 圭一朗

WEKO 55641

ja 草刈, 圭一朗

Search repository
坂部, 俊樹

× 坂部, 俊樹

WEKO 55642

ja 坂部, 俊樹

Search repository
Furuichi, Yuki

× Furuichi, Yuki

WEKO 55643

en Furuichi, Yuki

Search repository
Nishida, Naoki

× Nishida, Naoki

WEKO 55644

en Nishida, Naoki

Search repository
Sakai, Masahiko

× Sakai, Masahiko

WEKO 55645

en Sakai, Masahiko

Search repository
Kusakari, Keiichirou

× Kusakari, Keiichirou

WEKO 55646

en Kusakari, Keiichirou

Search repository
Sakabe, Toshiki

× Sakabe, Toshiki

WEKO 55647

en Sakabe, Toshiki

Search repository
アクセス権
アクセス権 open access
アクセス権URI http://purl.org/coar/access_right/c_abf2
権利
言語 ja
権利情報 ここに掲載した著作物の利用に関する注意 本著作物の著作権は情報処理学会に帰属します。本著作物は著作権者である情報処理学会の許可のもとに掲載するものです。ご利用に当たっては「著作権法」ならびに「情報処理学会倫理綱領」に従うことをお願いいたします。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.
抄録
内容記述 手続き型プログラムの検証手法として,モデル検査やホーア論理に基づく検証手法が代表的である.一方,項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている.本論文では,帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる.具体的には,自然数上のwhile言語で定義された手続き型関数からプレスブルガー文を規則の制約として持つことが許された制約付き項書換え系への変換を与え,その変換により手続き型プログラムの等価性を書換え系の関数の等価性に帰着させ,潜在帰納法を用いて等価性検証を試みる.この手法を実現するために,合流性を保証するための危険対定理および完備化手続きを制約付き書換えに対応するように拡張する.
言語 ja
内容記述タイプ Abstract
抄録
内容記述 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.
言語 en
内容記述タイプ Abstract
出版者
言語 ja
出版者 一般社団法人情報処理学会
言語
言語 jpn
資源タイプ
資源タイプresource http://purl.org/coar/resource_type/c_6501
タイプ journal article
出版タイプ
出版タイプ VoR
出版タイプResource http://purl.org/coar/version/c_970fb48d4fbd8a85
関連情報
関連タイプ isVersionOf
識別子タイプ URI
関連識別子 http://id.nii.ac.jp/1001/00016440/
ISSN
収録物識別子タイプ PISSN
収録物識別子 0387-5806
書誌情報 ja : 情報処理学会論文誌, プログラミング

巻 1, 号 2, p. 100-121, 発行日 2008-09
著者版フラグ
値 publisher
URI
識別子 http://id.nii.ac.jp/1001/00016440/
識別子タイプ URI
URI
識別子 http://hdl.handle.net/2237/21160
識別子タイプ HDL
戻る
0
views
See details
Views

Versions

Ver.1 2021-03-01 16:24:04.077514
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3