{"links":{},"id":10816,"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00010816","sets":["581:638:642"]},"path":["642"],"owner":"1","recid":"10816","title":["有限状態機械に基づくプログラミングでのgoto文使用の是非：Hoare論理の観点から"],"pubdate":{"attribute_name":"公開日","attribute_value":"2004-09-15"},"_buckets":{"deposit":"2195c48a-9869-4cfa-a207-50694bda943e"},"_deposit":{"id":"10816","pid":{"type":"depid","value":"10816","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"有限状態機械に基づくプログラミングでのgoto文使用の是非：Hoare論理の観点から","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"有限状態機械に基づくプログラミングでのgoto文使用の是非：Hoare論理の観点から"},{"subitem_title":"On the Use of goto's in Programming Based on Finite State Machines: From the Hoare Logic Viewpoint","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"論文","subitem_subject_scheme":"Other"}]},"item_type_id":"2","publish_date":"2004-09-15","item_2_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"株式会社日立製作所システム開発研究所"},{"subitem_text_value":"北陸先端科学技術大学院大学"}]},"item_2_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Systems Development Laboratory, Hitachi, Ltd.","subitem_text_language":"en"},{"subitem_text_value":"Japan Advanced Institute of Science and Technology (JAIST)","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/10816/files/IPSJ-JNL4509002.pdf"},"date":[{"dateType":"Available","dateValue":"2006-09-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-JNL4509002.pdf","filesize":[{"value":"219.2 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"8"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"f96bbae5-b38a-49c0-94dc-e0bbf3cae6fb","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2004 by the Information Processing Society of Japan"}]},"item_2_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"金藤栄孝"},{"creatorName":"二木, 厚吉"}],"nameIdentifiers":[{}]}]},"item_2_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Hidetaka, Kondoh","creatorNameLang":"en"},{"creatorName":"Kokichi, Futatsugi","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_2_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN00116647","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_2_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7764","subitem_source_identifier_type":"ISSN"}]},"item_2_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"Dijkstraのgoto文有害説とそれに引き続く構造的プログラミングの提唱以降，goto文の使用に関する問題は永く議論された．goto文の使用法に関し理論的裏付けを持つ研究としては，逐次的プログラムでの任意の制御フローは順次接続・条件分岐・反復の3基本構造のみで表現可能であるという結果に基づくMillsらのgoto文排斥論以外は皆無である．Dijkstra本来の正しさを示しやすいプログラムを書くための構造化という立場?つまりプログラム検証論の立場?からのgoto文使用の是非は考察されていない．本論文では検証手段としてのHoare論理に基づき有限状態機械モデルに基づくプログラミングでのgoto文の使用を検討する．その結果，状態をラベルで表し状態遷移をgoto文での飛び越しで行うプログラミングスタイルが，状態を表す変数を追加しgoto文を除いたプログラミングスタイルと比べ，Hoare論理による検証での表明が簡単で自然な形となり機械的検証の時間的コストも少ない．ゆえにプログラムの正しさの示しやすさという観点からは有限状態機械モデルに基づくプログラミングでの状態変数導入によるgoto文除去は有害でありgoto文を用いたスタイルの方が望ましいことを示す．","subitem_description_type":"Other"}]},"item_2_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"There have been a vast amount of debates on the issue on the use of goto statements initiated by the famous Dijkstra's Letter to the Editor of CACM and his proposal of “Structured Programming”. Except for the goto-less programming style by Mills based on the fact that any control flows of sequential programs can be expressed by the sequential composition, the conditional (if-then-else) and the indefinite loop (while), there have not been, however, any scientific accounts on this issue from the Dijkstra's own viewpoint of verifiability of programs. In this work, we reconsider this issue from the viewpoint of Hoare Logic, the most standard framework for correctness-proving, and we see that the use of goto's for expressing state transitions in programs designed with the finite state machine modelling can be justified from the Hoare Logic viewpoint by showing the fact that constructing the proof-outline of a program using goto's for this purpose is easier than constructing the proof-outline of a Mills-style program without goto by introducing a new variable.","subitem_description_type":"Other"}]},"item_2_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"2137","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌"}],"bibliographicPageStart":"2124","bibliographicIssueDates":{"bibliographicIssueDate":"2004-09-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"9","bibliographicVolumeNumber":"45"}]},"relation_version_is_last":true,"item_2_alternative_title_2":{"attribute_name":"その他タイトル","attribute_value_mlt":[{"subitem_alternative_title":"プログラミングの理論"}]},"weko_creator_id":"1"},"created":"2025-01-18T22:45:37.224822+00:00","updated":"2025-01-23T02:36:19.315602+00:00"}