Scholarlink

We investigate three proof rules for proving termination of while programs and show their proof-theoretic equivalence. This involves a proof-theoretic analysis of various auxiliary proof rules in Hoare’s logic. By discussing representations of proofs in the form of proof outlines, we reveal differences between these equivalent proof rules when used in practice. We also address applications in the context of the paradigm of design by contract.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Three Ways of Proving Termination of Loops

  • 章节

  • 发表日期：

    2025年

查看全文
  • Krzysztof R. Apt,
  • Frank S. de Boer,
  • Ernst-Rüdiger Olderog

摘要

We investigate three proof rules for proving termination of while programs and show their proof-theoretic equivalence. This involves a proof-theoretic analysis of various auxiliary proof rules in Hoare’s logic. By discussing representations of proofs in the form of proof outlines, we reveal differences between these equivalent proof rules when used in practice. We also address applications in the context of the paradigm of design by contract.