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

Formal method of procedure call based on Hoare logic

作　　者：雷富兴[1] 张来顺[1] 

机构地区：[1]解放军信息工程大学电子技术学院,河南郑州450004

出　　处：《计算机工程与设计》2011年第1期197-201,共5页Computer Engineering and Design

摘　　要：采用Hoare逻辑风格的推理,提出了一些从源代码推导过程和这些过程调用的形式化语义规范的技术和算法。为了推导一个过程调用的语义,将过程看作一个抽象单元从程序分离出来,提取过程的形式化语义规范。对于一个具体的过程调用,形式化这个调用的前置条件,根据这些条件形式化求解调用的最强后置条件,也就是调用的语义作用。Techniques and algorithms for deriving specifications directly from code for procedures and for deriving specifications of the semantic effects of calling those procedures are presented based on Hoare logic style reasoning.In order to reason about the semantic effects of a procedure call,the semantic specification of the procedure is called as an independent abstract unit needs to be abstracted.A specific procedure call is given,and the formal precondition is abstracted that hold at invocation of a procedure,and then these conditions is used as a precondition to the procedure body to calculate its strongest postcondition,the postcondition is also the semantic effects of procedure call.

关 键 词：HOARE逻辑 过程语义 过程调用语义 前置条件 后置条件 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]