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

作     者：雷富兴 张来顺 LEI Fu-xing;ZHANG Lai-shun

作者机构：解放军信息工程大学电子技术学院河南郑州450004 

出 版 物：《计算机工程与设计》 (Computer Engineering and Design)

年 卷 期：2011年第32卷第1期

页      码：197-201页

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

主 题 词：Hoare逻辑 过程语义 过程调用语义 前置条件 后置条件 

学科分类：081203[081203] 08[工学] 0835[0835] 0812[工学-测绘类] 

D　O　I：10.16208/j.issn1000-7024.2011.01.040

馆 藏 号：203465082...