Extending Hoare Calculus to Deal with Crash

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

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.