...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>情報処理学会論文誌 >多重ループからの脱出でのgoto文の是非：Hoare論理の観点から
【24h】

多重ループからの脱出でのgoto文の是非：Hoare論理の観点から

机译：转义多重循环中 goto 语句的优缺点：从霍尔逻辑的角度来看

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Dijkstraのgoto文有害説とそれに引き続く構造的プログラミングの提唱以降，goto文の使用に関する問題は長く議論されてきたが，goto文の使用法に関しての理論的裏付けを持つ研究としては，逐次的プログラムの制御フローは3基本構造（順次接続，条件分岐，反復）のみで表現可能であるからgoto文を用いたプログラムは3基本構造のみによる等価なプログラムに書き換えられる，という結果に基づいたMillsらのgoto文排斥論以外は皆無であり，Dijkstra本来のプログラムの正しさを示す手段としてのプログラムの構造化という観点でのgoto文の使用の是非は，プログラム検証論の立場から考察されなかった．本論文では，プログラムの正しさを示すという検証手段としてのHoare論理に基づきgoto文の使用を再検討する．特に，多重ループの打ち切りの場合，goto文を用いて脱出するプログラミングスタイルの方が，Mills流のBoolean型変数を追加してループを打ち切るスタイルよりも，Hoare論理での証明アウトラインが簡単に構成でき，したがって，前者のgoto文を用いたプログラミングスタイルの方が，そのようなプログラムに対するHoare論理による検証上からは望ましいことを示す．
机译：自从 Dijkstra 的 goto 语句的危害性理论和随后的结构规划提出以来，goto 语句的使用问题已经讨论了很长时间，但作为一项有理论支持使用 goto 语句的研究，顺序程序的控制流具有三种基本结构（顺序连接、条件分支、 除了 Mills 等人拒绝 goto 语句之外，没有其他论点，其结果是使用 goto 语句的程序可以重写为只有三个基本结构的等效程序，因为它只能通过迭代来表示，并且从构建程序的角度使用 goto 语句作为显示 Dijkstra 原始程序正确性的手段的利弊是 在本文中，我们重新研究了基于Hoare逻辑的goto语句的使用，作为验证程序正确性的手段。 特别是在中止多个循环的情况下，使用 goto 语句进行转义的编程风格比 Mills 风格添加布尔变量并中止循环的 Mills 风格更容易在 Hoare 逻辑中构造证明轮廓。从通过 Hoare 逻辑验证此类程序的角度来看，使用 goto 语句的前一种编程风格更可取。

著录项

相似文献

  • 外文文献
  • 中文文献
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号