论文部分内容阅读
摘 要： B方法主要是用抽象机来描述软件系统的规范说明，且有大量工具支持。UML作为新一代面向对象建模语言得到了广泛的支持，已经成为事实上的工业标准。UML 图形是模型元素集合的可视化表示，类图表达了面向对象系统分析中的最基本元素——类和类之间联系，而类之间的依赖关系是类之间联系中的最重要、最普遍的一种联系。本文旨之讨论如何让用B方法来描述UML类图，从而能提高软件开发的效率、降低成本，也能改善软件工程的质量。
关键词： UML类图 B方法 静态模型 形式化
统一建模语言UML作为新一代面向对象建模语言得到了广泛的支持，已经成为事实上的工业标准。UML不仅支持面向对象分析与设计，而且支持从需求分析开始的软件开发的全过程，已大范围地用于现代企业集成信息系统的设计和开发当中。UML图形是模型元素集合的可视化表示。UML定义了9种图形，其中类图表达了面向对象系统分析中的最基本元素——类和类之间联系，而类之间的依赖关系是类之间联系中的最重要、最普遍的一种联系。
1.UML类图简介
UML类图表达的是对象模型的静态结构。其中一部分图形元素是基本的，如类、关联等，对于任何面向对象模型都是必不可少的。
类图表达一组类和它们的联系，在类图中，一方面描述各个类本身的组成，即类的属性、操作和对对象的约束，另一方面描述系统中类之间的静态的联系，其主要静态联系类型有关联、聚集、泛化、依赖等。
面向对象系统设计一般运用都是规模较大的空间，类的数目众多、类之间的关系错综复杂，设计者很难直接从类图中理清类与类之间的依赖关系。然而，面向对象系统基于UML语言在分析和设计过程中，已经生成了许多类图，如果能合理、有效地利用这些已经生成的成果，不仅能提高软件开发的效率、降低成本，而且能改善软件工程的质量。
2.B语言
B语言属于基于模型的规格说明符号语言的范畴，是一种基于对象的形式化语言。它以规格说明语言Z语言的研究为背景，在引入一些面向对象机制等特点的同时，保留了Z语言的优点［５］。B语言使用相对简单，且人们熟悉的符号表示法(广义代换)来表达状态的转换，从软件的规格说明到编码的形成是一致的形式描述，使程序和程序的规则说明处于统一的数学框架之下，以一种基于集合论的符号表示法来书写，减少了出现语义错误的可能性。这种数学框架是通过谓词变换和扩展的Dijkstra最弱前置条件提供的［１］。B语言的抽象机非常类似于Effiel中的类的概念，或者Ada语言的包。
3.UML类图静态模型的形式化
UML类图模型由对象类的命名方框构成，方框中列出了类的所有属性及其操作，实体之间的关系用连线表示。一般说来，UML类图中的类将表示为B机器，它封装了可能的和存在的该类类型的属性集合，以及对这些属性的操作集合。类之间的关联关系使用B机器的包含INCLUDES机制表示，继承关系可以使用EXTENDS结构化机制来表示。
下面我们给出把UML类图模型映射到B机器系统的基本方法和过程：
（1）标识类图中的实体类型族，也就是实体类型集合，这些实体类型是一个给定类型T的子类型，而T本身没有父类型。
（2）标识每个族内类型的操作和属性所需要的访问路径，这些访问是针对其它族中的类型。
（3）产生一个有向无环图，图中的节点就是类型族，图中的边是节点之间的包含关系USES或SEES。
（4）按照下面给出的步骤，为每个类型族定义机器，并使用上一步标识的关系包含其它的机器［６］。
根据上述方法，一个类图的转换可以写成如下形式：（假设类名为实体类Entity，ENTITY为一实体集合，T1——Tn都是T类型的子类型）
MACHINE Entity
SETS
ENTITY
VARIABLES
Entities，
Att1，att2，...，attn
INVARIANT
entitues?哿ENTITY att1∈entites→T1 att2∈entites→T2... attn∈entites→Tn
...
END［３］
该机器是一组Entity实例的模型，而不是一个单独的实体。集合ENTITY代表Entity实例的所有可能同类体的集合，entities代表当前已有的Entity实例的对象同类体集合。Entity实例的标准创建操作为：
i ←create_entity(att1_val，...，attn_val)=
PRE att1_val∈T1 ...attn_val∈Tn entities ENTITY
THEN
ANY j
WHERE
j∈ENTITY- entities
THEN
I：=j‖
entities：= entities∪{j}‖
att1(j)：=att1_val‖
...
attn (j)：=attn_val
END
END［４］
如果类模型的实体之间存在某些关系，那么T1，T2，...，Tn中的某些将涉及其它的实体，比如Entity2，Entity3，...，这时，我们要查看SEE或者使用USE相关的机器：
MACHINE Entity
SEES Entity2，Entity3，...
...
END
如果在Entity的不变式中只需使用同类体集合ENTITY2，ENTITY3，...，那么我们可以使用SEES。如果需要更具体的并且要使用已有的实体集entity2等作为不变式中的范围类型，那么要使用USES。
我们还可以使用一个参数对一个将允许的给定实体的最大实例数给出限制：
MACHINE Entity (maxEntity)
CONSTRAINTS
maxEntity≥1
...
PROPERTIES
Card (ENTITY)=maxEntity
INVARIANT
Entities?哿ENTITY ...
END
如果Entity2继承Entity1，那么需要把约束entities2 ( entities1放在标识超类的机器不变式中。
MACHINE Entity1
SETS
ENTITY1
VARIABLES
entities1，entities2
INVARIANT
entities1?哿ENTITY1(
entities2 ?哿entities1
...
END［２］
4.结语
本文讨论如何让用B方法来描述UML类图，从而为提高软件开发的效率、降低成本打下了基础，并能大大地改善软件工程的质量。
参考文献：
［1］裘宗燕译.Ｂ方法.电子工业出版社，2004，06.
［2］Kevin Lano.The B Language and Method：A Guide to Practice Formal Development.Springer Verlag，1996.
［3］B-Core Ltd.B-toolkit User’s Manual.Oxford（UK），1996.
［4］Emil Sekerinski and Rafik Zurob.Translation Statecharts to B.Spinger-Verlag，McMaster University，2003.
［5］鄒盛荣，郑国梁.B语言和方法与Z、VDM的比较.计算机科学，2002（10）：136-138.
［6］邹盛荣，郑国梁.形式化方法B和UML的结合研究.中国科技论文在线，2003中国计算机大会.
关键词： UML类图 B方法 静态模型 形式化
统一建模语言UML作为新一代面向对象建模语言得到了广泛的支持，已经成为事实上的工业标准。UML不仅支持面向对象分析与设计，而且支持从需求分析开始的软件开发的全过程，已大范围地用于现代企业集成信息系统的设计和开发当中。UML图形是模型元素集合的可视化表示。UML定义了9种图形，其中类图表达了面向对象系统分析中的最基本元素——类和类之间联系，而类之间的依赖关系是类之间联系中的最重要、最普遍的一种联系。
1.UML类图简介
UML类图表达的是对象模型的静态结构。其中一部分图形元素是基本的，如类、关联等，对于任何面向对象模型都是必不可少的。
类图表达一组类和它们的联系，在类图中，一方面描述各个类本身的组成，即类的属性、操作和对对象的约束，另一方面描述系统中类之间的静态的联系，其主要静态联系类型有关联、聚集、泛化、依赖等。
面向对象系统设计一般运用都是规模较大的空间，类的数目众多、类之间的关系错综复杂，设计者很难直接从类图中理清类与类之间的依赖关系。然而，面向对象系统基于UML语言在分析和设计过程中，已经生成了许多类图，如果能合理、有效地利用这些已经生成的成果，不仅能提高软件开发的效率、降低成本，而且能改善软件工程的质量。
2.B语言
B语言属于基于模型的规格说明符号语言的范畴，是一种基于对象的形式化语言。它以规格说明语言Z语言的研究为背景，在引入一些面向对象机制等特点的同时，保留了Z语言的优点［５］。B语言使用相对简单，且人们熟悉的符号表示法(广义代换)来表达状态的转换，从软件的规格说明到编码的形成是一致的形式描述，使程序和程序的规则说明处于统一的数学框架之下，以一种基于集合论的符号表示法来书写，减少了出现语义错误的可能性。这种数学框架是通过谓词变换和扩展的Dijkstra最弱前置条件提供的［１］。B语言的抽象机非常类似于Effiel中的类的概念，或者Ada语言的包。
3.UML类图静态模型的形式化
UML类图模型由对象类的命名方框构成，方框中列出了类的所有属性及其操作，实体之间的关系用连线表示。一般说来，UML类图中的类将表示为B机器，它封装了可能的和存在的该类类型的属性集合，以及对这些属性的操作集合。类之间的关联关系使用B机器的包含INCLUDES机制表示，继承关系可以使用EXTENDS结构化机制来表示。
下面我们给出把UML类图模型映射到B机器系统的基本方法和过程：
（1）标识类图中的实体类型族，也就是实体类型集合，这些实体类型是一个给定类型T的子类型，而T本身没有父类型。
（2）标识每个族内类型的操作和属性所需要的访问路径，这些访问是针对其它族中的类型。
（3）产生一个有向无环图，图中的节点就是类型族，图中的边是节点之间的包含关系USES或SEES。
（4）按照下面给出的步骤，为每个类型族定义机器，并使用上一步标识的关系包含其它的机器［６］。
根据上述方法，一个类图的转换可以写成如下形式：（假设类名为实体类Entity，ENTITY为一实体集合，T1——Tn都是T类型的子类型）
MACHINE Entity
SETS
ENTITY
VARIABLES
Entities，
Att1，att2，...，attn
INVARIANT
entitues?哿ENTITY att1∈entites→T1 att2∈entites→T2... attn∈entites→Tn
...
END［３］
该机器是一组Entity实例的模型，而不是一个单独的实体。集合ENTITY代表Entity实例的所有可能同类体的集合，entities代表当前已有的Entity实例的对象同类体集合。Entity实例的标准创建操作为：
i ←create_entity(att1_val，...，attn_val)=
PRE att1_val∈T1 ...attn_val∈Tn entities ENTITY
THEN
ANY j
WHERE
j∈ENTITY- entities
THEN
I：=j‖
entities：= entities∪{j}‖
att1(j)：=att1_val‖
...
attn (j)：=attn_val
END
END［４］
如果类模型的实体之间存在某些关系，那么T1，T2，...，Tn中的某些将涉及其它的实体，比如Entity2，Entity3，...，这时，我们要查看SEE或者使用USE相关的机器：
MACHINE Entity
SEES Entity2，Entity3，...
...
END
如果在Entity的不变式中只需使用同类体集合ENTITY2，ENTITY3，...，那么我们可以使用SEES。如果需要更具体的并且要使用已有的实体集entity2等作为不变式中的范围类型，那么要使用USES。
我们还可以使用一个参数对一个将允许的给定实体的最大实例数给出限制：
MACHINE Entity (maxEntity)
CONSTRAINTS
maxEntity≥1
...
PROPERTIES
Card (ENTITY)=maxEntity
INVARIANT
Entities?哿ENTITY ...
END
如果Entity2继承Entity1，那么需要把约束entities2 ( entities1放在标识超类的机器不变式中。
MACHINE Entity1
SETS
ENTITY1
VARIABLES
entities1，entities2
INVARIANT
entities1?哿ENTITY1(
entities2 ?哿entities1
...
END［２］
4.结语
本文讨论如何让用B方法来描述UML类图，从而为提高软件开发的效率、降低成本打下了基础，并能大大地改善软件工程的质量。
参考文献：
［1］裘宗燕译.Ｂ方法.电子工业出版社，2004，06.
［2］Kevin Lano.The B Language and Method：A Guide to Practice Formal Development.Springer Verlag，1996.
［3］B-Core Ltd.B-toolkit User’s Manual.Oxford（UK），1996.
［4］Emil Sekerinski and Rafik Zurob.Translation Statecharts to B.Spinger-Verlag，McMaster University，2003.
［5］鄒盛荣，郑国梁.B语言和方法与Z、VDM的比较.计算机科学，2002（10）：136-138.
［6］邹盛荣，郑国梁.形式化方法B和UML的结合研究.中国科技论文在线，2003中国计算机大会.