B方法规格说明的构造及应用  

Construction of B-method Specification and Its Application

作　　者：吴帅[1] 杨庆红[1] 樊艳芬[1] 

机构地区：[1]江西师范大学计算机信息工程学院

出　　处：《计算机与现代化》2007年第5期29-32,35,共5页Computer and Modernization

摘　　要：B方法是一种软件形式化方法,支持从规格说明到代码生成的整个软件开发周期。本文比较系统地分析了B方法规格说明的构造结构,并结合所设计的实例演示了用B方法编写规格说明的过程,简略地给出了其规格说明的证明义务,并对其规格说明进行了一次精化。B-method is a software formal method, which supports the whole lifecycle of software development from formal specification to code generation. This paper analyses the structure of B-method specification systematically, demonstrates the procedure of writing specification with B-method by an example, gives the proof obligation of specification simply, and at the same time refines the specification.

关 键 词：规格说明 B方法 抽象机 证明义务 精化 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]