Extending Hoare Calculus to Deal with Crash

真正的程序可能会崩溃，在某种意义上说，它们没有做应该做的事情。我们希望找到一种在抽象层次上描述程序的方法，以便我们不仅可以推理它们以及它们应该做什么，而且我们还可以推理它们是否会崩溃。我们工作的长期目标是为有崩溃和异常的程序的推理提供适当的解释。这将包括关于整数下溢/溢出、数组边界和悬空指针的推理。我们想开发微积分来处理这些现象，并证明它们的可靠性和完备性。这将首先涉及对崩溃的适当处理，其次涉及相应的扩展以处理例外。在短期内，我们希望开发一个Hoarecalculus的扩展，它可以充分地处理崩溃，并证明它的可靠性和完备性。

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.