形式化方法B的证明技术

作者：鹿蕾形式化方法抽象机广义代换类型检查证明义务

摘要：用形式化方法开发软件是提高软件可靠性和开发效率并实现其自动持从规约到实现的全过程开发工作.本文介绍了B方法的分层开发与证明过程,针对构造AM以及对他进行精化和实现过程中的类型检查、证明义务进行了重点分析,最后通过具体应用说明了B方法的证明技术在实践中的有效性.

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社