（计算机应用技术专业论文）基于流语言的并发软件测试.pdf

浙江理工大学硕士学位论文 摘要 并发程序的测试一直是软件测试中的关注点。所谓并发程序是指两个或多个进程 ( 或线程) 协同完成一个任务。每个进程是一个序列程序执行一串语句。进程间的交 流是通过信息传递来完成。然而由于与生俱来的不确定性( 使用了不确定性语句，过 程的进程速度难以预知) ，并发程序的测试有很大难度。 软件测试过程包括测试用例生成和测试用例运行。鉴于测试用例生成在测试中占 有主要作用，本文主要考虑测试用例的生成。用于生成测试用例的方法可分为两种： 随机测试( r a n d o mt e s t i n g ) 和分域测试( p a r t i t i o nt e s t i n g ) 。随机测试不能保证满 足标准，并且不能覆盖所有的元素。分域测试现有很多方法，这些方法以覆盖所有语 句，控制流，数据流或关键路径为目标。考虑到分域测试各方法的特点，从整体来说 可归结为基于路径的方法和基于状态的方法。基于路径的测试首先选取测试路径，然 后沿着测试路径对输入空间进行分解，但是这样的方法没有按程序语义进行，容易产 生不可行路径。基于状态的测试主要以状态机或变迁系统作为产生测试数据的模型， 状态空间会随着过程数增加而指数增长，很容易导致状态爆炸问题。 为了克服以上两种方法带来的缺点并且保持原有的优点，本文提出了一种形式化 方法，用于对基于流的序列程序和并发程序产生测试用例。我们首先定义条件和循环 覆盖准则，然后通过条件演算( c o n d i t i o nc a l c u l a t i o n ) 对序列程序产生测试用例，最后 根据定义的交互信息覆盖准则，在并发程序产生测试用例过程中将这些序列程序测试 用例合并产生同步序列( s y n s e q u e n c e ) 。该方法是一种精确的系统的测试程序的方 法。由于所产生的测试用例都是沿着程序语义进行，所以与现有的一些方法相比，该 方法避免了隐含的不可行路径。另外，通过对算法复杂度的分析也表明了该方法不会 产生状态爆炸。 关键字：软件测试，序列程序，并发程序，条件演算，同步序列 浙江理工大学硕士学位论文 t e s t i n go fc o n c u r r e n tp r o g r a mw i t hf l o wb a s e dl a n g u a g e a b s t r a c t t h et e s t i n go fc o n c u r r e n tp r o g r a m si saf o c u si np r o g r a mt e s t i n g ac o n c u r r e n tp r o - g r a ms p e c i f i e st w oo rm o r ep r o c e s s e s ( o rt h r e a d s ) t h a tc o o p e r a t et o g e t h e rt op e r f o r ma t a s k e a c hp r o c e s si sa s e q u e n t i a lp r o g r a mt h a te x e c u t e sas e q u e n c eo fs t a t e m e n t s t h e p r o c e s s e si n t e r a c tt oe a c ho t h e ru s i n gm e s s a g ep a s s i n g t h et e s t i n go fc o n c u r r e n tp r o - g r a m s i sd i f f i c u l td u et ot h ei n h e r e n tn o n d e t e r m i n i s mi nt h e s ep r o g r a m s ( n o n d e t e r m i n i s t i c s t a t e m e n to rn o n - p r e d i c t e de x e c u t i o nr a t e ) t h e r ea r et w op h a s e si nt h ep r o c e s so fs o f t w a r et e s t i n g ：t e s tc a s e sg e n e r a t i o na n d t e s tc a s e se x e c u t i o n w eo n l yc o n s i d e rt e s tc a s e sg e n e r a t i o nb e c a u s ei ti st h ek e ys t e p i nt h et e s t t h e r ee x i s t sal o to fs t r a t e g i e si ns o f t w a r et e s t i n gw h i c hc a nb ec l a s s i f i e da s r a n d o mt e s t i n ga n dp a r t i t i o nt e s t i n g r a n d o mt e s t i n gc a nn o tg u a r a n t e et h es a t i s f a c t i o n o fc o v e rc r i t e r i o n p a r t i t i o nt e s t i n gm a yc o v e ra l ls t a t e m e n t s ，c o n t r o lf l o w s ，d a t af l o w s o rc r i t i c a lp a t h s m e t h o d si np a r t i t i o nt e s t i n gc a nb ef u r t h e rc l a s s i f i e db a s e do np a t h s a n db a s e do ns t a t e s m e t h o d sb a s e do np a t h sf i r s ts e l e c tt e s tp a t h sf r o mp r o g r a m ，t h e n g e tt e s tc a s e sa l o n gt h ep a t h sb yd i v i d i n gi n p u ti n f o r m a t i o n h o w e v e rt h eg e n e r a t i o n p r o c e s si sn o tb a s e do nt h es e m a n t i c so ft h ep r o g r a m s ，t h u st h eg e n e r a t e dt e s tc a s e sm a y b ei n f e a s i b l e m e t h o d sb a s e do ns t a t e so f t e nu s u a l l yu s es t a t em a c h i n e so rt r a n s i t i o n s y s t e m sa su n d e r l y i n gm o d e l sf o rt e s tg e n e r a t i o n a st h en u m b e ro ft h et a s k si n c r e a s e s ， t h es t a t ew i l li n c r e a s ee x p o n e n t i a l l yw h i c hm a yl e a dt os t a t e se x p l o s i o np r o b l e m i no r d e rt ok e e pt h er i g o r o u sb u tn o tt oh i tt h es t a t ee x p l o s i o np r o b l e ma n di n f e a s i b l e p a t h sp r o b l e m ，t h i sp a p e rp r e s e n t saf o r m a lm e t h o dt og e n e r a t et e s tc a s e sf o rs e q u e n t i a l p r o g r a m sa n dc o n c u r r e n tp r o g r a m sw r i t t e n i naf l o wb a s e dp r o g r a ml a n g u a g e a c c o r d i n g t ot h ec o v e r a g ec r i t e r i o nd e f i n e d ，t e s tc a s e so fs e q u e n t i a lp r o g r a m sa r eg e n e r a t e db a s e do n c o n d t i o nc a l c u l a t i o n ，a n dc a nb ec o m b i n e dt o g e t h e rt of o r ms y n - s e q u e n c e s f o rc o n c u r r e n t p r o g r a mt e s t i n g o u rm e t h o dc a n b ec o n s i d e r e da sar i g o r o u sa n ds y s t e m a t i ca p p r o a c ht o t h et e s t i n go fp r o g r a m s c o m p a r i n gw i t hs o m ef o r m a lt e s t i n gm e t h o d s ，o u rm e t h o dc a n a v o i dh i t t i n gi n f e a s i b l ep a t h m o r e o v e r t h ec o m p l e x i t ya n a l y s i sr e v e a l st h a to u rm e t h o d a l s oc a na v o i ds t a t ee x p l o s i o np r o b l e m k e yw o r d s ：s o f t w a r et e s t i n g ，s e q u e n t i a lp r o g r a m s ，c o n c u r r e n tp r o g r a m s ，c o n d i t i o n c a l c u l a t i o n ，s y n s e q u e n c e l l - 浙江理工大学硕士学位论文 表格目录 垂1 子表属性2 6 垂2 原子属性2 6 垂3 测试用例3 3 7 1 资源统计4 6 7 - 2 测试用例4 6 浙江理工大学硕士学位论文 插图目录 3 - 1 程序分片1 8 冬1 部分i c 表达式的数据结构2 8 5 1 测试用例合并3 5 7 - 1a t m 上p p p 的架构4 5 7 - 2p p p 的部分代码4 7 1 1 1 浙江理工大学学位论文原创性声明 本人郑重声明：我恪守学术道德，崇尚严谨学风。所呈交的学位论文，是本人在导师 的指导下，独立进行研究工作所取得的成果。除文中已明确注明和引用的内容外，本论文 不包含任何其他个人或集体已经发表或撰写过的作品及成果的内容。论文为本人亲自撰 写，我对所写的内容负责，并完全意识到本声明的法律结果由本人承担。 学位论文作者签名_ 莲彝 日期：口、阿舒年夕月彩1 7 1 浙江理工大学学位论文版权使用授权书 学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保留并向国家 有关部门或机构送交论文的复印件和电子版，允许论文被查阅或借阅。本人授权浙江理工 大学可以将本学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印 或扫描等复制手段保存和汇编本学位论文。 本学位论文属于 保密口， 不保密口 学位敝储龇靠 同期：7 舻年弓月么 日 年解密后使用本版权书。 浙江理工大学硕士学位论文 第一章绪论 测试是一种通过执行系统或分析系统来检查系统正确实现的一种方法。测试中， 首先执行测试过程，将得出的测试结果与规约的结果进行比较来检查系统的正确性。 因此测试只能观测所有可能系统行为的一小部分，而不能测出所有的系统行为，正 如d j i k s t r a1 1 3 所说：测试仅仅可以找出错误所在，而不能找出缺少的部分。并发程序 的测试一直是程序测试中的关注点。所谓并发程序是指两个或多个进程( 或线程) 协 同完成一个任务。每个进程是一个序列程序执行一串语句。进程间的交流是通过共享 变量或信息传递来完成。然而由于与生俱来的不确定性( 如使用了不确定性语句，过 程的进程速度难以预知) ，并发程序的测试有很大难度。 1 1 研究现状 现在软件测试的方法有很多。软件测试过程包括测试用例生成和测试用例运行。 鉴于测试用例生成在测试中占有主要作用，本文主要考虑测试用例的生成。用于产生 测试用例的方法大致分为两种：随机测试( r a n d o mt e s t i n g ) 和分域测试( p a r t i t i o n t e s t i n g ) 。 1 1 1随机测试 随机测试集合都是可行的吣1 。这种产生过程看起来似乎更符合实际情况，然而随 机测试集合并不能保证满足标准，并且不能保证覆盖所有的元素。 1 1 2 分域测试 测试的目标集中在覆盖所有语句、控制流、数据流或者关键路径辟明。大量的工作 研究都是基于这个覆盖准则进行的。基于这个覆盖准则也有很多不同的方法。以下是 我们列出的其中几种方法： 控制流图( c f g ) 。这种方法旨在根据源代码构建一个控制流图，然后从图中选 取测试用例。例如对序列程序的路径分析测试中，y a n g 等人在c f g 中定义 了c p a t h 和c r o u t e 。在c r o u t e 中，沿着c - p a t h 就可以产生测试输入。一般来 说，c p a t h 由序列程序中的测试用例组成，c r o u t e 的行为类似于同步序列。 一1 一 浙江理工大学硕士学位论文 但是，从控制流图或者扩展后的控制流图( e x t e n d e dc f g ) 得出的路径有可能 是不可行的。b e r t o l i n o 和m a r r f 1 提出了一个算法并且描述了用于选择路径的 策略，这种方法的优点是得出的不可行路径的数量会减少。然而，正如作者 所说的，她们的算法“不能完全的满足引导执行路径的具体目标，因为她们的 方法仅仅是基于程序控制流的”。这种方法更适用于序列程序。k a t a y a m ap 到等 人从描述并发程序行为的源代码中推出了事件行为交互图( e v e n ti n t e r a c t i o n s g r a p h ，e i a g ) ，所描述的并发程序包括了任何任务类型( t a s k t y p e ) 和合作 路径( c o o p e r a t e dp a t h s ) 。他们在e i a g 上定义c o p a t h s 作为并发程序的测试用 例，但是作者也提到并不能保证所有的路径都是可行的。 可达图( r g l 。并发程序的执行行为是基于并发状态( r g 中的节点) 的p ”。 一旦并发状态图被构建，并发历史信息( c o n c u r r e n c yh i s t o r y ) 就是并发状态 图中一些路径的状态序列。并发历史信息引导了测试用例的执行过程。这 个方法中，每个选择的路径都是可执行的，但却面临着状态爆炸问题( s t a t e e x p l o s i o np r o b l e m ) ：在实际应用中，可达图的状态个数会很大。为了减缓状态 爆炸，k o p p o l 和t a i 忙4 1 提出了一种渐次增加的办法。对并发程序的每个任务都产 生一个带标签的迁移系统( l a b e l e dt r a n s i t i o ns y s t e m ) 。每一个l t s 对应一个可 达图。当一些过程在同一层面上整合时，它们就构成一个简化的可达图。基于简 化的可达图，选择测试路径来检查过程间的接口错误。 带标签的变迁系统( l b s ) 。带标签的变迁系统为规约提供了形式化语义。t r e t m a n s 和b e l i n f a n t e p 棚为p r o m e l a 规约定义了带标签变迁系统的特殊类，称为输入- 输出 变迁系统( i n p u t o u t p u tt r a n s i t i o ns y s t e m s ) 。他们假设所有的行为都归为输入 和输出两种行为。他们将i o c o 测试理论用于产生测试用例，他们还描述了测试 工具t o r x 。正如作者在文中所说：这个方法也面临状态爆炸问题。m u c c i n i 弘q 等 人用l t s 建模系统结构行为，然后选取能够覆盖抽象l t s 的测试路径来驱动测试 集合。最终，这个结构测试都被规约为代码层面( c o d e - l e v e l ) 的测试以便用来执 行。但作者提到得到一个全局的结构模型并不是一件容易的事情。 模型检测( m o d e lc h e c k i n g ) 。模型检测机建立有限状态迁移系统，并且穷尽了 所有可达的状态空间用于寻找背离的属性p 1 。如果能检测到背离的属性，模型检 测机将提供反例以说明这种情况如何发生。带有模型检测机的测试方法将反例 一2 浙江理工大学硕士学位论文 理解为测试用例。这个使用的模型是一个典型的可预测系统行为的模型，而且 这个模型可以由系统需求，测试用例和设计规约来驱动捌，甚至时代码本身都 可以创建模型p 。这种方法主要面临的问题是状态爆炸。一些研究人员已经将 模型检测用于指导产生测试用例的输入。如g a r g a n t i n i 和h e i t i n e y e r p 叫使用了一 个模型检测机来产生s c r 标记中给出的规约属性的偏离来产生测试。a m m a n n 和b l a c k w 将模型检测和变体分析( m u t a t i o na n a l y s i s ) 结合对规约产生测试用 例。r a y a d u r g a m b 叫等人用结构化的基于覆盖的方法对r s m l e 的规约产生测试 用例。然而这些方法都不能处理结构复杂的输入。 标号执行( s y m b o l i ce x e c u t i o n ) 。标号执行是一种对标号输入数值产生代数表 达式的程序分析方法。它保留了关于数据值的信息，这些数据值通常在静态并发 分析中会丢失。这个信息可以用来检查不可行执行路径，同样也可以产生测试数 据u0 1 。虽然标号执行缓解了不可行的问题，但是由于它自身的缺陷例，如不能分 析动态数据结构和数组，处理过程时可能会导致不可行等问题，这使得测试数据 生成器有时还不能找到输入数据来遍历所选的路径。 洳g u p t a p 所说：“它需要 复杂的代数操作机制，并且在处理数组和指针引用上还存在欠缺”。o f f u t t p u 同样 提到了标号执行“仍存在有一些实际问题，包括不能处理未确定的循环以及标志 表达式的大小”。注意到这些状态分析瞰儿驯被认为是对标号执行的路径选择机制， 而标号执行则是状态分析的机制。有时，标号执行和状态分析合并用于产生测试 用例。例女f i y o u n gt a y l o r 卜剐合并并发状态图用于确定可能的同步格式。a r t h o h 等人引进了扩展了标号执行的模型监测器来分析程序的输入域。 约束测试( c b t ) 。这个方法由m i u o 和o f f u t t 弘叫提出。线性约束( a l g e b r a i c c o n s t r a i n t ) 被用于描述一种错误的具体类型。c b t 通过消除异种( m u t a n t ) 来产生测试用例。c a r v e r 和蹦冽对分布式程序提出了叫做c s p e ( c o n s t r a i n t so n s u c c e e d i n ga n dp r e c e d i n ge v e n t s ) 的约束符号来产生测试序列。c s p e 约束可直接 从抽象程序中得到，测试序列根据约束从抽象程序选择序列。然而，序列的数量 通常都是很大或者是无限的。最近，通过描述基于标准的约束( c o n s t r a i n tb a s e d c r i t e r i a ) 以及相应的所需元素，条件和约束。v e r g i l i o p 别等人改进了测试用例集 的效率。但是他们的实验表明基于标准的方法的代价很大，需要花很大的精力来 确定不可行路径。 一3 一 浙江理工大学硕士学位论文 可达性测试( r e a c h a b i l i t yt e s t i n g ) 。该方法延续了可达图的思想，但与可达 图不同的是它不需要构建静态模型来自动产生同步序列( s y n s e q u e n c e ) 。它 假定测试的输入数据已经获得，再根据某个输入执行该输入下同步序列的变种 ( v a r i a n t s ) 。这种方法可以用于测试同步信息传递的程序p 0 1 ，同样，该方法也可 以用于测试异步信息传递的程序p 铷。近年来，允许可达性测试应用到一些同步结 构中p 5 。但是该方法所得的同步序列不一定都适合规约。 其他方法。受到达尔文的优胜劣汰了理论的启发，l i n 和y e h 弘卅提出了用于对已选 路径的自动产生测试用例的遗传算法。另外c a i 睁等人提出了适应性软件测试策 略。这种方法将软件的测试建模为马尔可夫链( m a r k o vc h a i n ) ，综合了控制原 理，理论和方法。m e m o n p 川等人引用了人工智能的方法来为g u i 系统自动产生测 试用例。一种根据这种方法开发称为p a t h s 的原型已经实行。 以上分域测试生成测试用例的方法可以归结为两种：基于路径的测试和基于状态 的测试。基于路径的测试首先选取测试路径，然后沿着测试路径对输入空间进行分 解，但是这样的方法没有按程序语义进行，容易产生不可行路径。基于状态的测试主 要以状态机或变迁系统作为产生测试数据的模型，状态空间会随着过程数增加而指数 增长，很容易导致状态爆炸问题。 1 2本文的研究意义及主要工作 为了克服基于路径测试和基于状态测试所带来的缺点并且保持原有的优点，我们 对序列程序和并发程序分析时引入了一种基于流的语言。这种语言可以认为是从高 级语言通过编译产生的中级语言，也可以是实际程序的语言。这个语法根据控制流 ( c o n t r o lf l o w ) 和数据流( d a t af l o w ) 来定义。从控制流中，我们针对序列程序开发了 抽象表达式，因为控制流能够通过部分系统来控制其他执行的系统。从数据流中，我 们建立了序列程序之间的交互。实际上，并发程序可以看成是序列程序以及交互过程 的集合。 我们提出的方法首先定义循环及条件覆盖准则，然后通过条件演算( c o n d i t i o n c a l c u l a t i o n ) 对序列程序产生测试用例。一个测试用例就是一串输入和一个输出，每个 输入和输出都带有域( d o m a i n ) 信息。当测试数据输入时，输入的域空间会根据程序 中的条件来分解域信息。在每个输出点，我们都获得一个表达式，称为i c 表达式( i c e x p r e s s i o n ) ，这个表达式由输入变量，条件，a n d 操作符v ，0 r 操作符a 和序列标 _ 4 浙江理工大学硕上学位论文 号“； 组成。然后对i c 表达式进行分解并提取可行的测试用例。简化所提取的测试用例 后，我们使用b a l a b a n 州提出的算法来检查测试用例的兼容性。以上产生测试用例的 过程称为条件演算。为了对并发程序形成测试用例，我们定义了交互信息覆盖准则， 然后将序列程序之间的交互作为事件( e v e n t ) 来考虑，因此程序的输入和输出都是 事件。每个序列程序的测试用例都可以产生一个能够覆盖部分或者所有序列程序的同 步序列事件( s y n s e q u e n c ee v e n t s ) 。执行这些同步序列可以激活测试过程。因为测 试用例的产生过程都是基于程序语义的，所以所有得到的测试用例都是可行的。对算 法复杂度的分析显示我们的方法不会产生状态爆炸。所以与现有的产生测试数据的方 法似1 】3 7 1 2 4 1 2 9 1 进行比较，我们的方法可以避免不可行路径( i n f e a s i b l ep a t h ) 和状态爆 炸问题。 1 3 本文的组织结构 本文的具体组织结构安排如下： 第二章定义了流语言的语法和语义。 第三章介绍条件演算规则，包括条件演算基本规则，程序分片规则以及计算d 信 息的精化规则。 第四章描述了如何通过条件演算对序列程序生成测试用例。 第五章首先定义了同步序列的概念，然后对西的不确定性进行了分析，最后通过实 例研究介绍了如何从得到的序列程序测试用例形成同步序列。 第六章介绍了序列程序生成测试用例的算法以及并发程序生成测试用例的算法， 并对这两个算法的复杂度进行了分析。 第七章针对实际例子来产生测试用例，并对结果进行分析来评价我们所提出的方 法。 第八章为本文研究工作的总结和对下一步工作的展望。 5 一 浙江理工大学硕士学位论文 第二章基于流的语言 基于控制流，h s h m 和j a u c o p i n i q 证明了任何序列程序都是三种结构的组合：顺序 结构( s e q u e n c e ) ，分支结构( b r a n c h ) 和循环结构( 1 0 0 p ) 。控制流允许系统的部分 语句控制其他语句的执行，因此这个结构定义了程序语言的执行顺序。 2 1 流语言语法 我们给出一些定义： s t m t 表示基本语句，如初始化语句等， s e g 表示程序段， c o n d 表示条件， b ( c o n d ) s e g 表示分支语句， l ( c o n d ) s e g 表示循环语句。 这样我们就可以对序列程序定义以下语法； 其中 s e g ：= s t r u ts e g ；s e gib ( c o n d ) s e g rb ( c o n d ) s e g ll ( c o n d ) s e g ， c o n d ：= c o n d li1 c d 佗d llc o n d lac o n d 2 c o n d lvc o n d 2 ： 表示两个段语句之间的顺序关系， t 表示两个分支之间是可选择关系， a 表示与操作， 一6 一 浙江理工大学硕士学位论文 v 表示或操作。 序列程序可以通过以上语法表示。然而，上述结构并不足以表示多线程控制的复 杂系统。因为当前的控制仅仅表示执行过程中某一时刻执行一种操作。为了克服以上 缺点，我们需要在以上结构中添加了新的结构，这样我们就可以用来描述多个s e g 之间 的控制传递。 我们考虑两个序列程序之间的交互是通过信息传递( m e s s a g ep a s s i n g ) 进行的。消 息传递有紧耦合( t i g h t l yc o u p l e d ) 和和松耦合( l o o s e l yc o u p l e d ) 两种，也称为同 步信息传递( s y n c h r o n o u s ) 和异步信息传递( a s y n c h o n o u s ) 。同步信息传递就是发 送方需要等待接收方发回的确认信息才能继续执行，如进程调用( p r o c e s sc a l l ) 。异步 信息传递就是发送方不需要等待确认信息就可以到达它的目的地，如信号，时钟和异 步进程调用( a s y c h r o n o u sp r o c e s s ) 。在这两种情况下，发送方都被阻塞了( b l o c k e d ) 。 我们用s t m t o 来表示语句s t r u t 被阻塞并且需要输入信息，用s t r u t 表示语句s t r u t 发送出一个信息。注意到条件可以包含语句，我们将语法修改为： s e g ：= s t r u tis t r u t0ls t m t i s e g ；s e gib ( c o n d ) s e g t1 3 ( c o n d ) s e g il ( c o n d ) s e g ， c o n d ：= c o n d ll - _ 1 c o n d lfc o n d las t r n t0ic o n d lac o n d 2 i c o n d lvc o n d 2 其中、c o n d l 为c o n d l 的补集。我们从k e r n i 曲a n1 2 1 的文中引用了一个c 程序例子， 并用我们定义的语法用来描述该例子。函数“g o t o p 给“c a l c u l a t o rp r o g r a m ”获取下一 个操作符或操作数。这是一个执行时需要等待输入的序列程序，但是如果函数g e t c h a r 0 和r e t u r n 被其他函数调用，那这个过程就是多个序列程序之间的交互情况。我们之所 以选择这个例子是因为它含有三种控制结构，并且它可以用来作分片，精化以及条件 演算。这个程序也曾被用来做路径选择m 。 g e t o p ( s ll i m ) | g e tn e x to p e r a t o ro ro p e r a n d | 一7 一 浙江理工大学硕士学位论文 c h a rg 口；i n tl i m ； i n ti 。c ； w h i l e ( ( c = g e t c h a r 0 ) = = ii c = = t iic = = n ) ； i 士( c ! ；，是( c 9 ) ) r e t u r n ( c ) ； 8 0 3 = c ； f o r ( i = 1 ：( c = g e t c h a r ( ) ) = 0 皇是c = 9 ；i + + ) i f ( i l i m ) 8 i 】= c ； ) i f ( c = ； ) 幸c o l l e c tf r a c t i o n f i f ( i = 0 始c 9 ；i + + ) i f ( i l i m ) 8 i = c ： ) 】 i f ( i i 。 c o n d l 6 ：z i m i ， c o n d 2 1 ：l i r a i c o n d 2 2 ：2 i msi ， c o r 以2 3 ：c 70 7 a c 79 7 ， c a r d 2 4 ：c ! = 7 n 7ac ! = e o f , c o n d 3 1 ：z i m i 对于后面的讨论，我们假设每个条件c o n d 都有对立条件，记为一c d 们。例如，上面 _ 9 一 浙江理工大学硕士学位论文 存在一些对立条件： - - - c o n d l l ：c ! = ， c = 7vac ! = 7 ， 1 c o n d l 2 ：c = = v ( c 70 a c 79 ) ， - , c o n d l 3 ：c 79 1 c o n d l 4 ：d = 。 - c o n d 2 1 ：i i m i ， - c o n d ：2 ：l i r a i ， - c o n d 2 3 ：c 79 7 ， n c o n d 2 4 ：c = = 7 vc = = e d 只 - 1 c 帆d a x ：z i m i 因为系统是由多个序列程序以及序列程序之间的交互构成，它可以由以上结构表 示。显然，我们提出的代数表达能够用来支持继承和组合。因此可以用来描述大而且 复杂的系统。因为并发程序是由多个序列程序组合而成，所以它能够用我们所定义的 结构表示。 2 2 流语言语义 上面的定义可以看作是静态的表达式。令s e g 为一个程序段。执行时，如果我们 用硒来表示s e g 的状态入口，即初始状态。用s e g 来表示状态出口，即终止状态。那 么我们就可以定义程序的操作语义如下： 顺序语义： s e g t ；b e 9 2 一s e g t ；s e 9 2 s e 9 1 ；曼呈丝一兰竺望! i 皇曼丝 8 e g t s e g i s e g l ；s e 9 2 _ s e g i ；s e 9 2 s e g t _ s e g i s e 9 2 ；s e g l _ s e 9 2 ；s e g i 第一个表达式表示执行s e 9 1 ；s e 9 2 时，先执行s e g t 。第二个表达式表示s e 9 2 在8 e 夕1 执行完毕后才开始执行。第三个表达式表示一旦s e 9 2 执行完毕，贝u s e g l ；s e 9 2 也就执行 一1 0 浙江理工大学硕士学位论文 完毕。最后两个表达式表示如果s 叼1 状态改变为s e 斫，那么任何一个包含s e g ，的序列 化程序都会将s e g l 改为s e 9 。 选择语义： b ( o o n d ) s e 9 ) 召( c d 他d ) s e 9 ) 侈( 历而) s e 9 ) 一召( 盟区) s e 9 ) 召( 丝星) s e 夕) _ 8 ( c d 佗d ) 砑) b ( c o n d l ) s e g l - fb ( c o n d 2 ) s e 眈】一b ( c o n d l ) s e g l tb ( c o n d 2 ) s e 夕2 ) b ( c o n d l ) s e g l tb ( c o r t d 2 ) s e 9 2 _ b ( c o n d l ) s e g l tb ( c a n d 2 ) s e 夕2 ) b ( c o n d l ) s e g l tb ( e _ x m d 2 ) s 坳) 一b ( c o n d l ) s e g l tb ( c o n d 2 ) s e 驼) b ( c o n d l ) s e g l tb ( c o n d 2 ) s e 9 2 _ b ( c o r t d l ) s e g l tb ( c o n d 2 ) s e 9 2 b ( c o n d l ) s e g l _ b ( c o n d i ) s e 9 i b ( c o n d , ) s e g l tb ( c o n d 2 ) s e 9 2 _ b ( c o n d l ) s e g l tb ( c o n d 2 ) s e 9 2 b ( c o n d l ) s e g l _ b ( c o n d i ) s e g i b ( c o n d 2 ) s e 9 2 tb ( c e m d l ) s e g l 一u ( c o n d 2 ) s e 9 2 tb ( c o n d i ) s e 9 i ) 前面两个语句表示当条件进行选择执行语句时，所有分支语句有同样的机会可以 执行。接下来两个表达式表明选择语句执行完毕就表示整个分支语句执行完毕。最后 两个表达式说明了如果某个分支改变了状态，那么任何一个包含该分支的选择都会改 变分支状态。 循环语义： l ( c o n d ) s e g 一l ( c o n d ) s e g l ( 鬲蔼) s e 夕卜哼l ( c o n d ) s e g l ( c o n d ) s e g _ l ( c o n d ) s - - 西g l ( c o n d ) s - - ) 一l ( c o n d ) s e g l ( 僦d ) 型卜，l ( 姗回 s e 夕) l ( c o n d ) s e g 一l ( c o n d ) s e g 第一个表达式表示如果循环语句执行，首先检查条件。第二个表达式表示条件已 经检查完毕。第三个表达式表示如果条件为真，那么执行循环内部的片段。第四个表 1 1 浙江理工大学硕上学位论文 达式表示执行内部片段。第五个表达式表示重新进入循环，第六个表达式表示如果条 件为假，则跳出循环，即结束循环。 条件操作语义： c o n d tac o n d 2 _ c o n d tac o n d 2 c o n d tac o n d 2 _ c o n d lac o n d 2 c o n d lvc a n d 2 一c o n d lvc o n d 2 c o n d lvc o n d 2ac o n d 3 _ c o n d lvc o n d 2ac o n d 3 前面三