Extending Hoare Calculus to Deal with Crash

扩展霍尔微积分来处理崩溃

• 批准号: EP/D034981/1
• 负责人: Manfred Kerber
• 金额: $ 0.11万
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2006
• 资助国家: 英国
• 起止时间: 2006 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FD034981%2F1
• 关键词: Extending; Hoare; Calculus; Deal; Crash

Real programs can crash in a sense that they don't do what they are supposed to do. We want to find a way to describe programs on an abstract level so that we can not only reason about them and what they should do, but also that we can reason as to whether they will crash or not.The long-term aim of our work is to give a proper accountfor reasoning about programs with crash and exceptions. This willinclude reasoning about integer underflow/overflow, array bounds anddangling pointers. We want to develop calculi to deal with thesephenomena and prove their soundness and completeness. This willinvolve firstly an adequate treatment of crash and secondly acorresponding extension to deal with exceptions. In the short term we want to develop an extension of the Hoarecalculus which can deal adequately with crash and prove its soundnessand completeness.

真正的程序可能会崩溃，因为它们没有做它们应该做的事情。我们希望找到一种方法来抽象地描述程序，这样我们不仅可以推理它们以及它们应该做什么，而且还可以推理它们是否会崩溃。我们的长期目标我们的工作是对出现崩溃和异常的程序进行合理的推理。这将包括关于整数下溢/溢出、数组边界和悬空指针的推理。我们希望开发微积分来处理这些现象并证明它们的合理性和完整性。这首先涉及对崩溃的充分处理，其次涉及相应的扩展以处理异常。短期内，我们希望开发霍尔微积分的扩展，它可以充分处理崩溃并证明其健全性和完整性。

项目成果

Extending Hoare Calculus to Deal with Crash

扩展霍尔微积分来处理崩溃

• 发表时间: 2006
• 作者: V Bono