Abstract: This paper gives extensions of formal language B aided by the experience of AOP extensions of conventional language——AspectJ and AspectC++. Limits of selections of join points in B construct and constraints of verification of system are analyzed. It suggests that the scope of join points should be in IMPLEMENTATION components in B and the verification of aspect code should take the context of join points into consideration. The core concepts of AOP —— join point, pointcut, advice, and aspect —— are described here in the environment of B language

Key words: Aspect-oriented programming; B-language; Join point; Pointcut; Advice; Aspect

摘要： 借助传统编程语言的面向方面编程扩充――AspectJ/AspectC++的技术经验，提出形式化语言B 的AOP 扩充机制AspectB。分析了B 语言针对AOP 扩充在连接点范围及正确性验证方面的制约，提出连接点的范围必须限制在IMPLEMENTATION 组件中，方面代码的正确性验证必须考虑连接点上下文所涉及的不变性条件。以一个简单图形编辑器为例，在B 语言环境中描述面向方面编程的核心概念——连接点、连接点集合、建议代码、方面

关键词: 面向方面编程；B 语言；连接点；连接点集合；建议代码；方面