| 基于Hoare逻辑的过程调用的形式化方法 |
| |
| 引用本文： | 雷富兴,张来顺.基于Hoare逻辑的过程调用的形式化方法[J].计算机工程与设计,2011,32(1):197-201. |
| |
| 作者姓名： | 雷富兴 张来顺 |
| |
| 作者单位： | 解放军信息工程大学电子技术学院,河南,郑州,450004 |
| |
| 摘 要： | 采用Hoare逻辑风格的推理,提出了一些从源代码推导过程和这些过程调用的形式化语义规范的技术和算法。为了推导一个过程调用的语义,将过程看作一个抽象单元从程序分离出来,提取过程的形式化语义规范。对于一个具体的过程调用,形式化这个调用的前置条件,根据这些条件形式化求解调用的最强后置条件,也就是调用的语义作用。
|
| 关 键 词： | Hoare逻辑 过程语义 过程调用语义 前置条件 后置条件 |
Formal method of procedure call based on Hoare logic |
| |
| LEI Fu-xing,ZHANG Lai-shun.Formal method of procedure call based on Hoare logic[J].Computer Engineering and Design,2011,32(1):197-201. |
| |
| Authors: | LEI Fu-xing ZHANG Lai-shun |
| |
| Affiliation: | (Institute of Electronic Technology,PLA Information Engineering University,Zhengzhou 450004,China) |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
