| 形式化方法B的证明技术 |
| |
| 引用本文： | 鹿蕾.形式化方法B的证明技术[J].现代电子技术,2005,28(23):126-128. |
| |
| 作者姓名： | 鹿蕾 |
| |
| 作者单位： | 鲁东大学,山东,烟台,264025 |
| |
| 摘 要： | 用形式化方法开发软件是提高软件可靠性和开发效率并实现其自动持从规约到实现的全过程开发工作.本文介绍了B方法的分层开发与证明过程,针对构造AM以及对他进行精化和实现过程中的类型检查、证明义务进行了重点分析,最后通过具体应用说明了B方法的证明技术在实践中的有效性.
|
| 关 键 词： | 形式化方法 抽象机 广义代换 类型检查 证明义务 |
| 文章编号： | 1004-373X（2005）23-126-03 |
| 收稿时间： | 2005-09-16 |
| 修稿时间： | 2005年9月16日 |
The Proof Technology in Formal Method B |
| |
| LU Lei.The Proof Technology in Formal Method B[J].Modern Electronic Technique,2005,28(23):126-128. |
| |
| Authors: | LU Lei |
| |
| Affiliation: | Ludong University, Yantai, 264025, China |
| |
| Abstract: | Developing software using formal method is key to software automation. Formal method B can be used in the whole advance software reliability, improve developing efficiency and realize developing cycle from specifications to implementation by the aid of its tools. This paper presents the processes of hierarchical development and proof of method B,depicts its type checking and proof obligations from the construction of abstract machine to refinement and implementation in detail. Finally,the efficiency of the proof technology in method B is proved via practical applications. |
| |
| Keywords: | formal method abstract machine generalized substitution type checking proof obligations |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
