Development of formally verifiable framework for program transformation

我们开发了一种方法，它是逐步细化方法的扩展，用于使用指针操作和异常等高级特性的程序的正确性保持转换。我们已经说明，每个特性都有相应的逻辑系统，即指针操作的分离逻辑和异常的四值逻辑。已经证明，通过在计算机上基于每个特定的逻辑系统开发形式证明，程序的正确性得到了形式的保证。

We have developed a method, which is an extension of the stepwise refinement method, for correctness-preserving transformation of programs that make use of advanced features such as pointer manipulations and exceptions. We have shown that each feature has a corresponding logical system, namely, separation logic for pointer manipulations and four-valued logic for exceptions. It has been shown that the correctness of programs is formally guaranteed by developing formal proofs on computers, based on each particular logical system.