基于Hoare逻辑的过程调用的形式化方法

采用Hoare逻辑风格的推理,提出了一些从源代码推导过程和这些过程调用的形式化语义规范的技术和算法。为了推导一个过程调用的语义,将过程看作一个抽象单元从程序分离出来,提取过程的形式化语义规范。对于一个具体的过程调用,形式化这个调用的前置条件,根据这些条件形式化求解调用的最强后置条件,也就是调用的语义作用。

循环条件的形式化推导在程序验证中的应用

提出了一种求解命令式程序中循环执行和终止条件的方法。该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导。现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序。提出的形式化方法可以在一个原型工具中实现,通过该工具来推导循环执行和终止条件,辅助程序验证和程序缺陷修正。