{"updated":"2025-01-23T02:31:23.255498+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00010943","sets":["581:638:648"]},"path":["648"],"owner":"1","recid":"10943","title":["多重ループからの脱出でのgoto文の是非：Hoare論理の観点から"],"pubdate":{"attribute_name":"公開日","attribute_value":"2004-03-15"},"_buckets":{"deposit":"c97548e1-e321-4767-a7cc-a63cda511404"},"_deposit":{"id":"10943","pid":{"type":"depid","value":"10943","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 Escaping from Nested Loops: 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-03-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/10943/files/IPSJ-JNL4503013.pdf"},"date":[{"dateType":"Available","dateValue":"2006-03-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-JNL4503013.pdf","filesize":[{"value":"199.7 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":"44a0d295-63da-4961-9d43-64a40a50fb47","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;KokichiFutatsugi","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基本構造（順次接続，条件分岐，反復）のみで表現可能であるからgoto文を用いたプログラムは3基本構造のみによる等価なプログラムに書き換えられる，という結果に基づいたMillsらのgoto文排斥論以外は皆無であり，Dijkstra本来のプログラムの正しさを示す手段としてのプログラムの構造化という観点でのgoto文の使用の是非は，プログラム検証論の立場から考察されなかった．本論文では，プログラムの正しさを示すという検証手段としてのHoare論理に基づきgoto文の使用を再検討する．特に，多重ループの打ち切りの場合，goto文を用いて脱出するプログラミングスタイルの方が，Mills流のBoolean型変数を追加してループを打ち切るスタイルよりも，Hoare論理での証明アウトラインが簡単に構成でき，したがって，前者のgoto文を用いたプログラミングスタイルの方が，そのようなプログラムに対するHoare論理による検証上からは望ましいことを示す．","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 usages 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 issuefrom 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 proving the correctness of programs, and we see that usages of goto's in escaping from nested loops can be justified from the Hoare Logic viewpoint by showing the fact that constructing the proof-outline of a program using a goto for this purpose is easier than constructing the proof-outline of a Mills-style program without goto by introducing a new Boolean variable.","subitem_description_type":"Other"}]},"item_2_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"784","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌"}],"bibliographicPageStart":"770","bibliographicIssueDates":{"bibliographicIssueDate":"2004-03-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"3","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:42.808186+00:00","id":10943,"links":{}}