Scholarlink

In this chapter we consider the problem of mechanising the construction of derivations in Hoare logic having a given Hoare triple as conclusion. We are thus concerned with the backwards application of rules of the logic, which will eventually produce a derivation, i.e. a tree in which all leaves correspond to instances of axioms, and all side conditions hold.

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

Generating Verification Conditions

  • 章节

  • 发表日期：

    2026年

查看全文
  • José Bacelar Almeida,
  • Maria João Frade,
  • Jorge Sousa Pinto,
  • Simão Melo de Sousa

摘要

In this chapter we consider the problem of mechanising the construction of derivations in Hoare logic having a given Hoare triple as conclusion. We are thus concerned with the backwards application of rules of the logic, which will eventually produce a derivation, i.e. a tree in which all leaves correspond to instances of axioms, and all side conditions hold.