Extending Hoare Calculus to Deal with 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.