基于B方法的体系结构描述语言的精化研究

丁湘陵

(怀化学院物理与信息工程系,湖南怀化 418008)

1 B方法和ABC/ADL体系结构描述语言

B方法[1,2]是一种用于描述、设计计算机软件的严格语言,其作用一直延伸到代码生成,同时已经实现了一些工具系统,支持基于B方法的软件开发的全过程.最早由法国人J.R.Abrail于20世纪80年代前期开始研究,目的是希望为实际软件开发过程提供一个坚实的数学基础.在B方法思想形成过程中,C.A.R.Hoare和E.W.Dijkstra的关于程序作为一个数学对象、前-后置谓词、不确定性、最弱前置谓词的概念,无疑是它的中心思想;同时,C.C.Morgan的重要思想“Programmingfrom Specification”对其的形成起了深远影响和巨大作用.使得该语言成为目前国际上最受重视的软件形式化方法之一.

ABC/ADL体系结构描述语言[3-6]是北京大学信息科学技术学院梅宏等人设计的一种通用软件体系结构描述语言,以面向对象分析和设计方法为主导,主要概念包括构件、连接子和体系机构风格,并吸取了面向Aspect的开发思想,最突出的特点是支持软件体系结构描述向详细设计和实现的映射,并支持构件的组装,使用复合构件和复杂连接子逐步精化系统,但缺乏语义支持.

于是,将B方法和ABC/ADL两相结合,取长补短,展开了体系结构精化的研究,提出了一种使两者无缝集成的精化开发方法：首先定义精化约束和规则保证在精化过程中模型系统的一致性;然后对ABC/ADL复合构件和复杂连接子使用定义的精化约束和规则逐步精化,直到可执行程序.

2 体系结构精化研究

2.1 复合构件和复杂连接子[5]

ABC/ADL提供复合构件和复杂连接子的机制来帮助设计人员逐步精化系统.从构件对外的角度来看,复合构件和原子构件没有区别,因此它需要所有原子构件规约中的部分：模板规约、属性规约、Player规约等.不同点在于复合构件还需要定义内部结构规约,内部结构规约定义了内部体系结构名,它指向一个体系结构定义;还定义了若干个映射规约,每个规约将复合构件自身的一个Player映射到内部体系结构某个构件的Player.图1是例子中复合构件Ticket Agent的定义,它的内部结构是一个名为TA的体系结构,seller是在TA中定义的一个构件实例,复合构件的Player get Order Sheet被映射为seller的Player get Order Sheet.

图1 复合构件定义

从与构件连接的角度看,复杂连接子和简单连接子没有区别.类似复合构件,它有自己的内部结构;但是与复合构件不同的是,复杂连接子的角色要被映射为内部结构中某个连接子实例的角色.

2.2 构件或者连接子精化理论

在ABC/ADL中使用复合构件和复杂连接子逐步精化系统,但缺乏理论基础.本节将介绍使用经过事件机制扩展的B方法来证明精化的合理性和保证构件和连接子精化过程的无死锁性,并在此基础上精化到可执行代码.这里以构件模型来加以说明,连接子模型可以类推.在详细介绍精化过程之前,先引入2个约束和3个规则并加以适当阐述.

在精化过程中可能包含更多的变量和更多的事件,而这些事件必须满足下面提出的约束1和约束2才能被引入,这样才能保证在精化过程中模型系统的一致性.

约束1：事件的守卫精化必须是正确的 (在当前的不变量内),这是因为决不让构件进入死锁状态.(注意：在构件的初始情况下显然是不存在死锁状态的).

约束2：在精化过程中引入的新的事件不允许永远执行,这意味着这些事件必须一直减少一个确定的自然数变量或者一个确定的有限集合.

将最终的事件转化为可执行代码必须遵循一定的转化规则,在这里提出三条规则,规则1将事件提出来,规则2和规则3将事件合成一个结果代码.在提出规则之前,首先说明一些符号的含义,S为事件 (被守卫着的执行)的选择;⇒为守卫操作;让 []为选择操作.

规则1：

S→S’[]U

Condition

S⊆S’ skip⊆U I⇒grd(S’) ∨grd(U) I⇒V∈N

I⇒ (V=n⇒ [U](V

规则1中⊆说明数据精化操作,新的事件U精化skip并将自然数变量减少,这些条件本质上验证了规则1在约束1和约束2中是满足的.

规则2：

(P∧Q) ⇒S[](P∧┐Q⇒T)[]U→ (P⇒IF Q Then S else T)[]U

规则2的作用是在风格上使两个事件合为一体形成一个IF语句.

规则3：

(P∧Q) ⇒S[](P∧┐Q⇒T)[]U→ (P⇒While Q Do S End;T)[]U

Condition：S和T没有被守卫

∧P∧Q⇒[S]P

注意：在守卫Q下循环体S应该维持P不变式.规则3有两种特殊情况：①当谓词P简单消失 (在这种情况中通过条件的第二条来严格限制),②当T精化为skip.

在前面已经知道如何通过规则1将一个新的事件引入进来,该事件必须精化skip并且同时减少一个确定的自然数或者一个有限的集合,同样该变量在相应的精化步骤中也可能引入一些新的变量.

为了容易实现这个规则,就必须进行如下操作：假设一个变量y被正常引入,具有类型Sy,并且具有一些粘结不变量.在精化Ri+1步,同样假设一个新的事件NewEvent在该事件引入.假设一个相应的变量由NewEvent去减少,表示为一个自然数表达式V(y).设想由被引入的变量y和前一阶段Ri的事件NewEvent组成加上维持变量y在其类型允许范围内的最小可能并减少V(y)的量.粘结不变式没有被引入Ri,仍在Ri+1中,这样就会以如下形式执行：NewEventBegin y：y∈Sy∧V(y)

约束和规则提出之后,下面以构件的精化过程为例加以说明：构件首先被刻画为一些参数,这些参数暗示将来程序的一些不变的输入,也就是说在将来它们运行时,它们将不改变这些参数,如Parameters∈Sp,Sp说明了参数类型.同样它也具有一些变量,称之为结果 (results).这些变量被定义为Sr类型,如：results∈Sr.由参数和变量可以得到该构件的初始规约描述,获得抽象的player和computation.构件的精化主要针对computation处理,computation可以通过约束1和约束2精化为更小的内部实体computationi,针对每个小实体同样可以使用约束1和约束2进行进一步精化转化为事件.不过也要注意一点：可能没有computationi而直接精化到具体的事件.事件已经是可精化的最小单元.通过研究观察,可能发现这些事件具有输入或者输出的功能,如果它们与player具有相同的功能或者行为,可以将它们与player进行mapping,这样就得到了复合构件.如果没有任何关联,事件就转化为构件的method.最后,只需要使用规则1、2、3就可以将所有事件进行综合得到构件的最终可执行代码.

3 实例研究

本节介绍一个简单数据库系统的完整开发过程,使用上节介绍的方法,将初始的构件模型和连接子模型精化为具有众多事件的事件系统,分析事件和player或role的关系得到复合构件或复杂连接子并最终精化到可执行代码.

在这个例子里,要描述的是保存某个人群中个人信息的系统.假定出现在数据库里的个人都有一个性别 (male或female)和一个状态 (living或dead),因此,需要定义两个枚举集合SEX和STATUS,还要定义一个集合PERSON,定义如下：SEX{male,female};STATUS={living,dead}.这些集合除了具有数据之外还有对相应数据的各种操作.例如：r←SEX-READBegin r：∈SEX End;SEX-WRITE(i)=PRE i∈SEX Then skip End.这里就是对集合SEX的操作,对于其他集合也具有类似的操作,在此不详细描述.

首先分析该系统应实现的功能：对于输入的个人信息执行相应的操作,比如说当前一位婴儿诞生,就必须对他进行登记,将他的相关信息输入并调用相关的操作 (birth-operation)对数据库文件进行修改.由此,该系统必须具有的变量：person,sex,status,mother,husband,wife,command.它们对应的不变式如下：person⊆PERSON∧sex∈person→SEX∧status∈person→STATUS∧mother∈person→ (MARRIED∩WOMAN) ∧husband∈WOMAN →MAN∧wife=husband-1∧command∈COMMAND其中MAN=sex-1[{man}];WOMAN=sex-1[{woman}];LIVING=status-1[{living}];DEAD=status-1[{dead}];MARRIED=Dom(husband∪wife);SING LE=person-MARRIED;ANG LE=PERSON-person;COMMAND = {new,birth,marriage,death,print,quit}.现在研究该系统所具有的事件,对于输入的控制命令command做出相应的操作来获得所必需的person,sex,称之为incom事件;事件trandata接受由in-com事件传递过来的数据,同时将数据传递给下一事件;最后一个事件接收传送来的数据,进行简单的数据检验,在这里要提供一个变量b来标明数据是否合格,如果b为true,则进行与command对应的操作内容;如果为false,则输出错误原因或错误信息,这个事件称之为operation-data.该系统的数据传递过程如图2所示,显然这是一个典型客户/服务器风格的系统.

图2 数据传递图

基于上面分析,初始模型分解如表1所示.

表1 初始模型分解表

观察表1发现person,sex在三个模型中都存在,但是可能希望在事件的演变过程中对person,sex进行精化,这就意味着它们不能成为共享变量,必须把它们从相对独立的模型中分离出来并且提出中间变量作为模型之间交流的数据.由于Server的数据也是由Client端发送过来的,所以在这里引入中间变量p1,s1与Client的person,sex相关联.另两个中间变量p2,s2和Client的p1,p2相关联,这样就将Client和Server中的person和sex就被间接消除掉了.数据的精化结果如表2所示.

表2 数据精化结果表

对于Server模型 (即Server构件)具有两个输入数据p2和s2以及输出操作成功与否.其初始构件规约描述为：

初始事件receive可以描述为：receive(p2,s2)p2∈PERSON∧s2∈SEX End.现研究一下Server构件的内部规约computation.对于不同的COMMAND控制命令,数据库中数据的修改也将产生不同的事件,事件的发生是非常不确定的,new↔first-human(s);birth↔new-born(s,w);marriage↔marriage(w,m);death↔death(p);print↔printperson(p);同时这些事件在任意时刻只有一个可以发生.这里只对在command=new的情况进行分析,其他情况可以相似类推.command=new对应的数据库操作first-human(s)初始化描述为：first-human(s)∈SEX End.进一步精化描述为：

对于该事件可以更进一步的精化斯之产生可执行代码,首先将上面相应的数学符号具体化.于是引入事件：baby←createobject;mod-field(1,baby,code-SEX(s));mod field (2,baby,code-STATUS(living)).

第一个事件实现产生集合对象并返回一个该对象的实例,第二、三个事件设定实例的性别和状态.对于第一个事件更进一步分析发现对于一个新生的婴儿必然在数据的文件中产生记录,由此提出文件变量,它包含最多maxrec的记录值的有穷序列和一个具体的变量bufvrb,定义如下：file∈seq(FIELD→VALUE) ∧size(file) ≤max-rec∧buf-vrb∈INDEX→VALUE.

相应操作如下：

基于文件变量,可以将第一个事件精化为如下形式：baby←create object=Begin NEWRECORD(v);baby←SIZEFILE End;而对于第二和第三个事件发现它们具有共同点,对此提出一个通用事件modfile(o,i,v)PRE o∈Dom(file) ∧i∈FIELD∧v∈VALUE Thenfile(o)(i)：=v End.这样得到了对于new操作的所有事件.使用同样方法可以得到其他操作事件.但是在这里还必须提出关于数据状态的检测机制,因此,引入如下事件来检测数据的正确性.

is-present(p);is living(p);is woman(p);is-married(p);has mather(p);valstatus(p);valsex(p);val spouse(p);valmother(p).到此,Server模型的所有事件就都已经提出来了.

仔细分析,发现Server的扮演者receive与firstname、new-born、marriage、death、print-person具有相同的行为：都需要输入数据p2或者s 2,由此可以将它们进行映射;扮演者send输出操作结果与在各个操作中的STRING-WRITE具有同样行为,可以将它们进行映射 (注意：代码实现时要加以改进将各个操作中的STRING-WRITE提炼出来),这样Server也具有了复合结构,在这里只描述了部分映射关系,其它也可类似得到.

到此为止,Server构件完成了精化,但本文的目标并不仅仅到此,而是必须按照规则精化到可执行代码.由此将已经提出的事件按照定义的约束和规则综合,得到如下可执行代码.

观察SERVER模型的实现,发现还必须设计了一些关于文件的操作：

到此,一个简单数据库系统的设计已经告一段落.现在必须完善的就是对于这种设计结果正确与否,还必须对事件进行证明.比如说,要验证事件death(p)的正确性,就必须维持不变式,这点可以描述为如下形式：

通过执行有关代换,除去不需要的假设及其明显的结论,将只需要证明公式：

STATUS={living,dead}

status∈person→STATUS

p∈PERSON

⇒[status：=status<+ {p→dead}]∈person→STATUS.使用工具Prob很容易将其实现.具体的使用在这里不详细介绍.对于连接子Clink和Client构件可以按照Server构件描述的方法实现.

4 结束语

本文展开了体系结构精化的研究,提出了一种使两者无缝集成的精化开发方法：首先定义精化约束和规则保证在精化过程中模型系统的一致性;然后对ABC/ADL复合构件和复杂连接子使用定义的精化约束和规则逐步精化,直到可执行程序.同时将该方法应用到人口统计的数据库系统,应用工具ProB验证该系统的动态行为.但是,基于ABC/ADL描述框架中的求精过程是一个复杂而且困难的工作且基于不变式性质不变的前提来实现求精过程,还需人工的操作,考虑开发可集成的验证工具集成到ABC/ADL开发工具中达到抽象模型到具体代码实现的求精过程的验证自动化.总之,使基于ABC/ADL结构框架的程序设计过程更加高效、可靠,且保证设计过程的正确性和可复用性是最终目的.

[1]J-R Abrial著.B方法 [M].裘宗燕译.北京：电子工业出版社,2004.

[2]T.Lecomte.Event B Reference Manual IST-1999-11435[EB/OL].http：//www.atelierb.eu/ressources/evt2b/eventb-reference-manual.pdf.2010.

[3]Hong Mei,Jichuan Chang,Fuqing Yang,Composing S of tware Components at Architectural Level[C].//In Proceedings of International Conference on S of tware-Theory and Practice,IFIP the 16th World Computer Congress(WCC2000/ICS2000),2000,(8)：224-231.

[4]Hong Mei,Feng Chen,Qianxiang Wang,and Yaodong Feng,ABC/ADL：An ADL Supporting ComponentComposition[C]//Proceedings of 4th International Conference on Formal Engineering Methods,ICFEM2002,Oct.2002：38-47.

[5]王晓光,冯耀东,梅 宏.ABC/ADL：一种基于XML的软件体系结构描述语言 [J].计算机研究与发展,2004.9,Vol.41,No.9：1521-1531.

[6]梅宏.基于体系结构、面向构件的软件开发方法ABC[C].//中国科学院信息技术科学部第19次技术科学论坛“软件技术”专题学术报告会,2006：1-8.