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.