作者：高洪江; 覃征; 鹿蕾; 邵利平形式化方法广义代换抽象机前向精化反向精化证明义务
摘要：形式化方法B支持从抽象规约到实现的完整的开发过程,用于开发安全关键的软件系统。给出了B方法精化的定义后,介绍了抽象机的精化过程与方法,结合实例分析了仅使用前向精化的普通精化规则的不完整性,通过引入反向精化提供了完备的精化理论,二者联合起来能够证明任何正确的精化。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
《计算机工程》（CN：31-1289/TP）是一本有较高学术价值的大型月刊，自创刊以来，选题新奇而不失报道广度，服务大众而不失理论高度。颇受业界和广大读者的关注和好评。 《计算机工程》特点：以最快的速度、科学求实的精神，精选刊登代表计算机行业前沿科研、技术、工程方面的高、精、尖优秀论文。
部级期刊
人气 230963 评论 65
人气 216789 评论 35
省级期刊
人气 214070 评论 71
北大期刊、统计源期刊
人气 193649 评论 73
