B: a model-based method using generalised substitutions
B: a model-based method using generalised substitutions
复制标题
B：使用广义替换的基于模型的方法
DOI：
10.1007/978-1-4471-0701-9_3
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
M. Frappier
中科院分区：
文献类型：
--
作者：
H. Diab;M. Frappier
B符号[1]是由Jean-Raymond Abrial开发的。它支持开发生命周期的很大一部分，从规范到实现。B符号是形式的：它具有基于Dijkstra [6]的最弱前提演算的公理语义。Abrial显著地扩展了Questra最初的保护命令集，提出了一个完整的规范和设计符号，可扩展到大型系统开发。其中一些扩展的灵感来自牛津大学编程研究小组的工作（例如，[7]）。B表示法与Z表示法和VDM表示法密切相关（Abrial是Z的发展的重要贡献者）。
The B notation [1] was developed by Jean-Raymond Abrial. It supports a large segment of the development life cycle, from specification to implementation. The B notation is formal: it has an axiomatic semantics based on the weakest-precondition calculus of Dijkstra [6]. Abrial has significantly extended the initial set of Diskstra’s guarded commands, proposing a complete specification and design notation scalable to large system development. Some of these extensions are inspired from the work of the programming research group at Oxford (e.g., [7]). The B notation is closely related to the Z notation and the VDM notation (Abrial was a strong contributor to the development of Z).