第3章 原型和图形 3.1原型 3.1.1概述 在自然界，“原型”演化是一种重要的生物进化方式。当环境变化显著或发生跃迁时，原来适应的生物面临生存压力，其生存方式必须做一些改变。开始时，生物生存行为上的转变可能仅仅引起生理结构的细微变化，后来经过长期进化的修修补补，生物才产生适应新环境的有效生理结构。与后来定型了的生理结构相比，原始的、简略的最初结构便是后来成熟结构的原型。在功能意义上，我们也可以说原型结构模拟了定型后结构的行为。例如，始祖鸟是现今鸟类的原型，作为生物飞行的最初尝试，它的行为是对飞行的模拟。 在知识界，“原型”构造是一种重要的科学研究方式。科学研究者考查科学现象时，往往对科学对象作出适当的理论假设，随机构造简易模型对自己的假设进行验证。其中主要的验证方式就是观察在一定的条件下，那个简单模型的“行为”是否像科学对象的“行为”一样，产生相同的或相近的自然现象。这个简易的、原始的模型便是科学对象的原型，它的行为便是对科学对象导致的自然现象的一种模拟。于是，通过原型，科学研究者便能证实或推翻自己事前所作的关于特定自然现象的科学推理，甚至促进自己研究进一步深入、细化。 在软件界，原型是一种重要开发且测试手段。软件界都喜欢在软件实现之前，构造一个简易原始模型，用以对即将开发产品的（至少是主要的）功能进行模拟。这个原始模型便是未来软件产品的原型。 采用原型方法的关键思想是模拟，它是软件最早的一个能够运行的版本，是未来产品的雏形。如果软件开发组织采用生物进化理念，把原型模型、进化模型和增量模型综合为一个开发模式，那么就可以在某些产品研制过程中，把原型作为蓝本，不断地增加或修改、进化它的功能。在软件产品的研制过程中，作为产品探索式开发手段，用户使用“构成”原型生存环境，在用户反馈驱动下，迫使原型不断变更，犹如生物进化一般，最后或者弃之不用，或者仅以它实现的主要功能作为核心保留在定型的最终版本中。这种开发方式比事前把什么都规划完整，“按部就班”地生成软件产品方式要快，而且容易应对来自客户对需求的变更以及创造市场尚未展示的需求“商机”。 即使不以快速原型开发方式开发软件，软件开发过程也会从软件原型构造中受益。因为Gordon和Bieman通过对39个原型系统的调查研究，发现使用原型构造有如下好处： ①改善了系统的可用性； ②使系统更加贴近用户的需求； ③改善了设计质量； ④改善了可维护性； ⑤减少了开发人力。他们发现，原型构造只是在软件开发的前期阶段需要增加费用，但是会使后期的代价减少。主要原因在于避免了开发过程中很多返工，而这又是由于客户请求系统变更的减少［33］。 一般地，原型系统只是被用来探讨需求和选择设计，作为开发的一种科研方法，原型最后并不移交出去，它是一个抛弃式原型。这是由于构造原型时往往忽略了许多“细节”，特别是非功能需求。例如，目标产品是用于处理应付款、应收款和库存等业务事项，而开发的原型可能只是用于完成数据捕获的屏幕处理和报表打印，并不进行文件处理和错误处理等操作。通常，这些被忽略的功能不能通过调整原型系统得到满足。如果最终软件版本使用了低效的原型代码或甚至就是那个理应被抛弃的原型，那么总的系统性能可能有所退化以致得到一个不完整、质量差、维护困难且昂贵的系统。尽管一般情况如此，但是原型能够快速地模拟系统（至少是主要的）功能，原型构造已经成为一种开发手段和验证手段，在软件界得到广泛使用，并获得很好的效果。 在软件开发早期，客户对自己的需求表述往往模糊不清，甚至需求之间还存在矛盾。有时客户所说的需求并没有表达出他们真正希望的东西，以致客户在整个开发周期中任何时候都会产生新的想法，从而要求系统做出变更，以满足他们心中的真正要求。同样，开发者通常也不能确切地把握客户的真正想法。客户和开发者都无法肯定能够满足客户心中所求的软件能否实现。 这时，最理想的做法是，开发者深入了解了客户的需求后，进行快速分析，理清客户的关键想法，确定初步规格说明，把最重要的功能通过原型构造展示出来。原型是软件最早一个能够运行的版本，客户使用它，就会看到即将开发出来的软件是怎样的“面貌”以及是如何支持他们的工作的。他们就会用眼前的“实现”去印证自己心中真正“期待”，一方面发现自己所提出来的需求中的一些错误和遗漏之处； 另一方面也会对需求产生新的想法，从而找出软件中的优点和不足。特别是，用户最初认为自己对需求的功能给出了有用且是完整的描述，但是当某些功能通过原型结合起来运行的时候，用户通常会发现他们的最初想法是不正确的或不完整的。通过用户的反馈，需求描述得到修改，这些修改反映了用户在需求理解上的变化，也是关于开发者在需求工程中的工作的正确性的有效验证测试。通过用户使用原型的反馈信息，对原型进行修改，如此迭代式开发，可以减少花在完成用户文档和今后培训用户使用软件的时间。更重要的是，以此方式写出的需求文档（产品规格说明）会是准确的，且事后被用户要求变更系统的可能性较小，至少在主要功能上用户的需求已经稳定，不再发生变化了。 作为开发方式，原型可以用来演示概念，把客户需求抽象理念真实地、生动地呈现在人们面前，使开发者和客户在需求洽谈中达成一致。这同时增强了客户和开发者对软件制造的信心。这种在早期阶段就引进的开发和验证的双重活动，促进了随后系统设计和实现阶段的顺利进行，并使开发成本得到很好的控制。 作为科学研究方式，原型也是软件组织在系统设计阶段进行的兼具开发和验证的双重活动。 作为开发活动，原型可以用来演示概念并尝试设计选择，可以用来发现更多的问题和可能的解决方案，明确系统设计和实现的方法和途径。在系统设计阶段，甚至细微到某个具体算法，也可能是通过对算法原型的改进加以实现的。虽然软件界一般主张建立快速原型，在软件开发过程早期就应该抛弃。但是存在允许精炼一个快速原型的做法，特别是快速原型的某些部门。当部分快速原型是由计算机生成的时候，这些部分就可以用在最后的产品中。例如，用户界面经常是快速原型的一个重要方面。因为用户界面的动态性，文字描述和图都难以表达用户的界面需求。这时开发软件系统图形用户界面原型是最有效的方法。当用屏幕生成器和报表生成器等计算机辅助软件工程（ComputerAided Software Engineering，CASE）工具生成用户界面时，该快速原型的那些部分确实可以用作产品质量软件的一部分［22］。 作为验证活动，系统设计可以利用原型执行设计实验，以检验所提议的设计的可行性。例如，某个数据库设计可以通过原型构造和对原型的测试来检查，看它是否能对绝大多数的普通用户查询提供最高效的数据访问。虽然原型最后抛弃，但是构造原型使我们对即将实现的功能有深切体验，这种直观体验不仅帮助我们设计有效的测试用例去测试今后研制的实际系统，而且还可以实施一种所谓的“背对背”测试。当我们把相同的测试用例既提交给原型，又提交给待测试的实际系统时，如果两个系统给出相同的结果，测试案例可能没有检查出缺陷； 如果结果不相同，则意味着系统存在某个缺陷，出现不同的原因有待进一步调查。背对背测试是原型在系统测试中的一种运用［33］。 综上所述，快速构造原型用在需求阶段。它能让用户尽早看到未来系统的概貌，并让客户通过不断反馈参与其中，它是直接捕获用户（恰当的）需求手段。因此，它也是需求验证和确认的一种机制。客户的反馈是对需求的确认机制，也是开发人员验证自己是否“真实地”获取需求的机制，从而能编写正确的需求文档。在系统设计阶段，快速构造的原型可以作为设计选择、算法演示、制定设计方案的手段，这时原型是系统运行的一个蓝本，因而是对系统可行性和正确性的一个“粗略”验证，以后可以应用于“背对背”测试中，作为解决系统测试有效性问题的一种方式。 3.1.2示例 1. 原型支持用户界面设计 在软件的系统设计中，用户界面设计是最适合且最应该采用原型构造方式进行的开发活动。通常，用户界面的设计和实现都是开发人员的工作。在软件产品质量的因素中，可用性是至关重要的。人机交互界面友好与否，牵涉到人的因素，理所当然地应该以用户体验为准。与其产品完成后由于用户可用性要求（如他们觉得屏幕令人困惑甚至令人烦恼）而不得不修改人机界面，还不如在用户界面设计之时，让用户参与进来。这时系统设计的最好选择便是快速构造原型，让用户使用用户界面与计算机进行交互，并把自己的感觉告诉开发人员。这样，开发人员便可以发现普通用户的思维逻辑、习惯、直觉和偏好，从而设计出与未来用户所具有的技能、经验和他们的期待一致且容易使用的界面。用户自己的亲身体验是别人代替不了的，开发人员仅凭“深思熟虑”抽象思考企图准确地描述什么是用户所想要的人机界面是极其困难的，而以用户为中心的进化式和探索式原型构造却能容易达到预期目标。由此观之，每个软件产品都要建造与其相应的用户界面的快速原型。 《实战需求分析》［19］对界面设计进行了专门讨论。书中提出设计出的人机界面不要让用户难以学习，不要让用户感到厌烦、恐惧和难以捉摸，进而强调以人为本,优化用户界面，使其具有易学性、易用性、健壮性，使系统在执行中能与用户进行友好沟通，让用户得到准确的自己能理解的消息，并能让计算机对用户提供的消息作出良好反应。在以人为本的理念下，除了详细讨论了界面设计过程以外，这本著作对原型设计方法也进行较完整的介绍，如手画法（即在纸面上构造原型）、使用Microsoft Office工具设计法、使用原型设计工具设计法以及使用开发工具设计原型等方法，并对每种方法的实施都列举若干案例加以阐述。 许多文献都讨论了怎样建立用户界面的原型，如《软件工程》（第8版）［33］指出，在理想情况下，原型构造可以采取两步原型构造过程。 (1) 在过程的最早阶段，应该在纸面上规划“屏幕设计”模型并与未来用户一起探讨这个“原型”。 (2) 继而要对设计进行提炼并逐渐地开发复杂的自动化的原型，再将它们呈现给用户，接受测试和活动模拟。 在纸面上构造原型，是既便宜又容易做的事。开发人员无须开发任何可执行软件，只要清楚、直观地画出用户将要与之交互的系统屏幕样式就可以。然而，要想获得“活动”原型起到的演示效果，还必须有一组用来描述系统是如何使用的脚本。 通常，人们理解事物的抽象描述时，喜欢把它与实例联系起来。如果把人如何与软件系统交互用脚本的方法描述，人们就很容易理解并且评论它的好与坏。开发人员从用户对场景的评论中得到信息，不断地修改和增加交互细节，就可以写出需要在屏幕上显示出的信息以及可供用户选择的选项。类似地，可以使用“情节串联图板”表述界面设计。情节串联图板是一系列描述交互序列的草图，虽然实用性较差，但当向一组人而不是单个人表述界面提案时，它是一个较方便的方法。 在初始“纸上谈兵”以后，我们需要实现一个软件界面设计原型。由于我们需要得到某些用户可以交互的系统功能，因此在系统开发的最初阶段就对用户界面“如实”地进行原型构造，往往是不太可能的。避开这个问题的方式，需要使用Wizard of Oz（人冒充机器演示）原型构造方法。《绿野仙踪》里，有个影子很大的巨人，吓跑了很多人，后来发现他原来是一个瘦小的巫师，站在幕布后用灯放大影子。Wizard of Oz原型构造方法的基本理念是先做简单的、容易做的事情，而当比较复杂的事情一时难以实现时，就先用一个人在后台冒充机器处理系统。这时，用户的输入被引导到一个隐藏的人，通过这个人仿真系统的响应。用户认为自己是与计算机系统正在进行交互，在如此“逼真”的界面感觉下，用户愿意给出他们“真实”的意见和想法。实际上，在仿真系统的真实行为时，也可以通过使用某些其他系统计算所要的反应。总之，该方法的要点是除了要提出的用户界面以外，无须拥有任何可执行的软件。实验结束时，除了感谢参与实验的用户以外，还要告知他们真实情况，以示对他们的尊重。 界面设计中会存在缺陷和错误，利用与用户交互设计方法能够帮助开发人员发现问题。快速原型构造方法支持界面设计，不仅使开发人员更多地了解到自己的产品逻辑，从而确定用户界面最好式样，而且帮助开发人员预见未来的设计趋势，如用Wizard of Oz方法，现在就去设想当更多传感器和硬件加到设备上以后，怎样设计适应未来用户使用设备行为的用户界面。 在用户界面原型构造中，还可以使用脚本驱动、可视化编程语言以及基于因特网的原型构造等方法创建或提供用户界面。当然，我们要在迭代式原型构造及其实验中，寻找改善界面的方向和道路，当原型变得更完善，要对它进行评估。于是，可以采用抛弃式方法或进化式方法进行进一步的原型构造及其实验。 2. 原型支持算法研究 大部分科学活动（如果不是全部的话）都是基于一些“真知灼见”，并首先在极端理想化条件下，构造原型或思想实验，然后将条件尽可能一般化，构造“逼近”自然或实际情况的模型，从而得到理论体系，获得科学结论。 例如，爱因斯坦基于光速不变原理和洛伦兹变换，利用思想实验方法创立狭义相对论； 后又基于等效原理（即引力和加速度等效原理）和广义相对性原理，又一次利用思想实验方法创立广义相对论。爱因斯坦基于“光量子”假设，发现光电效应。这些思想和方法引发了20世纪两大物理学革命。 在计算机科学中，原始思想和原型方法也是重要的科学研究和开发成熟软件的手段。从广义角度来看，图灵计算模型便是现代计算机的一种“思想实验”，是现代计算机的虚拟“始祖鸟”。德国数学家、计算机科学家C.A.Petri在年仅13岁时便萌生了现以他名字命名的Petri网的想法，他当时只是想用该网描述化学过程。1962年，Petri在他的博士论文Kommunikation mit Automaten中正式提出了Petri网理论，当时他是用该网描述自动机通信过程。因此，Petri网最初只引起自动控制理论工作者的兴趣。后来在性能评估、操作系统以及软件工程等领域，也开始应用Petri网描述它们各自的问题，特别是Petri网可以有效地描述并发关系活动。目前Petri网已经在计算机科学中得到广泛运用，如可以用于设计，它是说明隐含定时问题的系统的一个功能强大的技术。 1975年，van Emde Boas提出（现在以他名字命名的）van Emde Boas树数据结构初步想法。不久，他和Kaas、Zijlstra等对该想法加以精炼并发表，随后还得到Mehlhorn和Nher的扩展以及Dementiev等的新实现。Ptra瘙塂cu和Thorup得到了查找前驱操作的一个下界，并说明了van Emde Boas算法在查找前驱操作上是最优的，即使允许引入随机化方法，仍是最优的。 现以van Emde Boas算法为例，说明原型在算法研究中的作用。基本理念是： 人们在研发新算法时，可以遵从一般科学研究方法，先从理想情况着手，构造算法原型，再推至一般情况，形成完整算法。本节取材于《算法导论》［27］一书。 假设只关注存储关系（不允许重复的）关键字，要存储的关键字的全域（Universe）为{0,1,2,…,u-1}，u为全域的大小。van Emde Boas树数据结构维护一个u位的数组A［0 ..u-1］，以存储一个关键字动态集合，其中的位来自全域{0,1,2,…,u-1}。也就是说，以位向量方式存储一个动态集合，若值x属于动态集合，元素A［x］为1； 否则，A［x］为0。例如，u=16，全域为{0,1,2,…,15}，存储关键字的动态集合为{2,3,4,5,7,14,15}，则在A［0..15］中，当x=2,3,4,5,7,14,15时，A［x］=1； 当x=0,1,6,8,9,10,11,12,13时，A［x］=0。van Emde Boas树支持在动态集合上运行时间为O(lg lg u)的操作： SEARCH、INSERT、DELETE、MINIMUM、MAXIMUM、SUCCESSOR和PREDECESSOR。 1) 原型van Emde Boas结构 考虑理想情况，设全域大小u=22k，其中k为整数。对于全域{0,1,2,…,u-1}，定义原型van Emde Boas结构或protovEB结构，记作protovEB(u)。由于u=22k，使用结构递归方法，每次递归都以平方根大小缩减全域，因此u,u1/2,u1/4,…,4,2都为整数。于是原型结构可以递归定义如下： 每个protovEB(u)结构都包含一个指明全域大小的属性u和另外若干特征。这些特征如下。 （1） 如果u=2，即u=22k，k=0时，那么它是基础大小，只包含一个两位的数组A［0..1］。也就是说，protovEB(2)由全域大小属性2和数组A［0..1］组成。 （2） 如果u≠2，即对某个整数k≥1,u=22k，这时有u≥4。除了具有全域大小属性u以外，protovEB(u)还具有以下属性（见图3.1）。  一个名为summary的指针，它指向一个protovEB(u)结构。  一个数组cluster［0..u－1］，存储u个指针，每个指针都指向一个protovEB(u)结构。 当u≥4时,protovEB(u)中的数组cluster［0..u－1］中每个指针都指向一个protovEB(u)结构。protovEB(u)结构的域{0,1,2,…,u－1}、它包含的关键字集合以及位向量A［0..u-1］都与protovEB(u)的全域{0,1,2,…,u}、包含的关键字集合以及位向量A［0 .. u-1］有关。protovEB(u)是protovEB(u)的递归结构，直观上，前者是后者的子结构。也就是说，protovEB(u)的所有信息便分别递归存储在由数组cluster的u个指针指向的u个簇中，每个簇保留原先u个信息中u个信息。于是，全域中的元素x（无论它是否为关键字），x（0≤x2时，一棵vEB(u)树中的信息结构包含大小为u的全域元素min和max、指向一棵vEB(↑u)树的指针summary，以及指向vEB(↓u)树的↑u个指针数组cluster［0..↑u－1］。（转摘于文献［27］图205) 因为基础情形u的大小为2，一棵vEB(2)树中对应的prorovEB(2)结构并不需要数组A。这是由于可以通过其min和max属性确定它的元素。在一棵不包含任何元素的vEB树中，不管全域的大小u如何，min和max均为NIL（无值）。 图3.3所示为一棵vEB(16)树V，包含集合{2,3,4,5,7,14,15}。因为最小的元素是2，所以V.min=2。根据上述构造方法，它不出现在cluster数组任意指针指向的簇中。也就是说，即使high(2)=0，元素2也不会出现在由V.cluster［0］所指向的vEB(4)树中。注意到这时V.cluster［0］.min=3，果然元素2不在这棵vEB树中。 类似地，因为V.cluster［0］.min=3，虽然在V.cluster［0］中“理应”包含元素2和3，但根据结构表示约定，V.cluster［0］内的vEB(2)簇为空。 min和max属性以及关于min元素存储的“古怪”做法是减少vEB树上一些操作的递归调用次数的关键。这些操作原先在protovEB结构上大都要进行多次递归。min和max属性有以下4方面的作用。 （1） 查找最小数和最大数操作甚至不需要递归，因为可以直接返回min和max的值。 （2） 查找后继和前驱操作也得到简化。例如，查找x的后继操作可以避免一个用于判断x的后继是否位于high(x)簇中的递归调用。这是因为x的后继位于x簇中，当且仅当严格小于x簇的max。 （3） 通过min和max的值，可以在常数时间内知晓一棵vEB树是否为空、仅含一个元素或两个以上元素。这种能力将在插入一个元素和删除一个元素操作中发挥作用。如果min和max都为NIL，则vEB树为空； 如果min和max都不为NIL但相等，则vEB树仅含一个元素； 如果min和max 都不为NIL但并不相等，这时vEB树则包含两个或两个以上元素。 图3.3对应于图3.1中protovEB树的一棵vEB(16)树它存储集合{2,3,4,5,7,14,15}。斜杠（/）表示NIL值。存储在vEB树中的min属性的值不会出现在它的任何一个簇中。这里的深阴影与图3.1的表示一样。（转摘于文献［27］图206） （4） 如果一棵vEB树为空，那么只要更新它的min和max值就可以在常数时间内实现插入一个元素。类似地，如果一棵vEB树仅含一个元素，也只要更新min和max值就可以在常数时间内删除这个元素。这些性质可以缩减递归调用链。 3） 两个结构操作对比示例 vEB(u)树上的所有操作，在最坏情况下，运行时间至多为O(lg lg u)。这与protovEB(u)相比，确实达到了最优。现在以查找最小数和查找后继两个操作为例在两个结构上进行对比。 （1） 在原型van Emde Boas结构上查找最小数。 过程PROTOvEBMINIMUM(V)返回protovEB结构中V中的最小元素，如果V代表的是一个空集，则返回NIL。 PROTO-vEB-MINIMUM(V) 1.ifV.u==2 2.if V.A［0］==1 3.return 0 4.elseif V.A［1］==1 5.return 1 6.else return NIL 7. else min-cluster=PROTO-vEB-MINIMUM(V.summary) 8.if min-cluster==NIL 9.return NIL 10. else offset==PROTO-vEB-MINIMUM(V.cluster［min-cluster］) 11. return index(min-cluster, offset) 第1行判断是否为基础情形； 第2~6行平凡地处理基础情形； 第7~11行处理递归情形。首先，第7行查找包含元素的第1簇号。因为V.summary是一个protovEB(u)结构，它包含V.cluster指向的各簇中是否有存储集合中元素的信息，所以在V.summary上递归调用PROTOvEBMINIMUM过程就可以找到最小数所在的簇号，第7行表明把递归调用的结果（即最小数所在的簇号）赋值给变量mincluster，如果集合为空，那么递归调用返回NIL； 如果集合非空，第7行递归调用的结果表明集合的最小元素就存在于编号为mincluster的簇中。第10行中的递归调用是查找最小元素在这个簇中的偏移量，该偏移量指明最小数在它所在簇中的“位置”。最后，第11行调用函数index（），通过最小数所在的簇号以及它所在簇中的偏移量计算出它的值，并返回。 查询summary信息允许我们快速地找到包含最小元素的簇，这是summary属性在结构中重要性的体现。虽然如此，由于查询最小数操作需要两次调用（第7行和第10行）protovEB(u)结构，所以根据算法理论，在最坏情况下运行时间会超过O(lg lg u)。可以推出，这个操作的运行时间为Θ(lg u)具体推导参见《算法导论》［27］第313页。。 （2） 在vEB树上查找最小数。 因为最小数存储在min属性中，所以查询最小数操作只有一行代码。 vEB-TREE-MINIMUM(V) 1.return V.min 顺便提一下，因为最大数存储在max属性中，所以查询最大数操作也只有一行代码。 vEB-TREE-MAXIMUM(V) 1.returnV.max 显然，这两个操作的运行只耗费常数时间。 （3） 在原型van Emde Boas结构上查找后继。 查找后继操作取一个参数x和一个protovEB结构V作为过程PROTOvEBSUCCESSOR的输入参数，过程PROTOvEBSUCCESSOR(V,x)便返回protovEB结构V中大于x的最小元素； 或者当V中不存在大于x的元素时，返回NIL。注意，过程不要求x一定属于该集合，但假定0≤x0，还需要考虑sk的下一个状态sk+1，由N3可知存在jk+1（0≤jk+1≤jk）在sk的下一个状态sk+1成立，对sk+1不断重复这一过程，从逻辑角度考虑一般情况，可以推知： φr,φr-1,…,φ1在状态区间序Ir,Ir-1,…,I1上分别成立，且它要么在一个φ0成立的状态终止，要么为无限序列。再结合N2，便可以得到结论。 注意，pωq意为p“等待/除非”q； pq意为由p可以推出q。 3） 响应性规则 响应性规则比较多，我们只介绍单步响应性规则和链式规则，其他规则只是这两个规则的扩充或变形。 （1） 单步响应性规则如下。 J1. p→(q∨φ) J2. {φ} T {q∨φ} J3. {φ} τ {q} J4. φ→En(τ)p◇q 其中，τ∈T。 J1： p→(q∨φ)是状态有效的，即在所有状态上，p→(q∨φ)成立。 J2： 在φ成立的某个状态，执行T中任意一个迁移,q∨φ在下一个状态成立。 J3： 在φ成立的某个状态，执行迁移τ(∈T )，q在下一个状态成立。 J4： 在φ成立的所有状态，τ是使能的，即En(τ)表示τ能够执行。 考虑结论p◇q，其中◇是时态运算符，指“终将”，即◇q意为“某个时刻”q。于是，从上述前提可以看出，如果p在状态si成立（i≥0），q也在状态si成立，那么可以直接得出结论。如果p在状态si成立，但是q在状态si并不成立，这时根据J1，φ必在状态si成立。然后根据J2，只要φ在状态si成立，经过T中任意迁移，在其转换到的下一个状态，q∨φ必定成立。但是根据J3，T中有一个迁移τ，却能从使φ成立的状态转换到使q成立的某个状态，再根据J4，凡在φ成立的状态，τ是能使的。综上可以得出结论。 （2） 链式规则如下。 J1.p→∨mj=0φj J2. {φi}T{∨j≤iφj} J3.{φi}τi{∨j0。因为φ0→q，若j=0，就与假设矛盾。由J2可知，φj在状态st成立，执行任意迁移后，便有φk在状态st+1成立，其中k≤j，而且k>0（与j>0同理）。重复此过程，为清楚起见，把上述迭代过程产生的φ序列记为φjk,φjk+1,…，其下标满足jk≥jk+1≥…>0。因此,由J2可以推知，必定存在一些jk（jk≥t），序列不再递减。这样，由J2便得φjk在（某）状态sk后一直成立。由J3可知，因为序列是递减的，故τjk在状态sk后是不能执行的。但由J4可知，τjk在状态sk后是使能的，这违反了τjk的公平性，所以反证得到结论成立。 2. MannaPnueli验证图方法 为了并发程序演绎验证可视化，1983年，Z.Manna和A.Pnueli首次提出并发程序演绎证明规则的图形表述，即验证图（Verification Diagrams）。1994年，他们系统地阐述了验证各类时序属性的验证图，这就为并发程序演绎验证提供了一种直观、可视化的方法［36］。 验证图是一个带标记的有向图，由节点和边组成。节点与断言绑定，表示一个验证条件。边表示节点的转移。验证图中可能存在这样的节点，没有边再从它引出。这种节点称为终止节点，与它绑定的是“目标断言”，指示演绎证明的结束。在验证图中，边用有向弧表示，节点用长圆角矩形表示，但终止节点的矩形要加粗。我们用m,…,0表示节点，对应的断言为Assertm,…,Assert0，其中m>0。 验证图可分为下几种类型。 1） 不变图 没有终止节点的验证图，可以包含循环。不变图可应用于不变性的证明。图3.9（a）所示的验证图即为一个不变图。 图3.94类验证图示例 2） Wait图 0是图中终止节点，并且图是非循环的，即无论何时从节点i引一条边到节点j，i≥j时，称该验证图为Wait图。Wait图用于优先性证明。图3.9（b）所示的验证图即为一个Wait图。 3） Chain图 当验证图满足以下条件时，称该验证图为Chain图。 (1) 0是终止节点； (2) 从节点i引一条单线边到节点j，则i≥j； (3) 从节点i引一条双线边到节点j，则i>j； (4) 从节点i（i>0）有一条双线边从i引出，该边称为断言i的“帮助”； (5) 同一变迁不允许既是单线边又是双线边。 Chain图可应用于响应性证明。图3.9（c）所示的验证图即为Chain图。 4） Rank图 当验证图满足以下条件时，称验证图为Rank图。 (1) 0是终止条件； (2) 对于每个节点i（i>0），有一条双线边从节点i引出，该边称为断言i的“帮助”； (3) 同一变迁不允许既是单线边，又是双线边。 Rank图也可应用于响应性证明。图3.9（d）所示的验证图即为Rank图。 注意，在Rank图中，当j>i时，也许节点j连接到节点i，这一点不同于Chain图。 3. MannaPnueli证明规则和验证图应用示例 例3.1响应性规则和验证图应用示例［36］ ANYY程序如图3.10所示。程序包含两个进程P1和P2，共享变量为x，初始值为0。进程P1中，只要x=0，y就增加1； 进程P2中，只有x∶=1这一条语句。显然，一旦将x赋值为1，进程P2就终止； 同样，只要x≠0，进程P1也会终止。 图3.10ANYY程序 （转摘于文献［36］图86） 现在，利用链式规则和验证图证明Θ◇( at_l2∧at_m1)。其中，初始条件Θ为： at_l0∧at_m0∧x=0∧y=0，为了使用链式规则证明它成立，建立该规则的4个前提。为此，首先建立4个断言及其相应的迁移集： φ3: at_l0,1∧at_m0∧x=0τ3:m0 φ2: at_l1∧at_m1∧x=1τ2:l1 φ1: at_l0∧at_m1∧x=1τ1:l0 φ0: at_l2∧at_m1 I={m0,l1,l0} 如果令p=at_l0∧at_m0∧x=0∧y=0，显然p→φ3成立，由此得到链式规则中的前提J1:p→V3j=0φj。 下面再来验证链式规则中前提J2~J4也是成立的。 关于φ3: at_l0,1∧at_m0∧x=0，验证J2~J4成立如下。 at_l0,1∧at_m0∧x=0φ3τat_l0,1∧at_m0∧x=0φ3,τ≠m0 at_l0,1∧at_m0∧x=0φ3m0at_l1∧at_m1∧x=1φ2∨at_l0∧at_m1∧x=1φ1 at_l0,1∧at_m0∧x=0φ3→at_m0En(m0) 关于φ2: at_l1∧at_m1∧x=1，验证J2~J4成立如下。 at_l1∧at_m1∧x=1φ2τat_l1∧at_m1∧x=1φ2τ≠l1 at_l1∧at_m1∧x=1φ2l1at_l0∧at_m1∧x=1φ1 at_l1∧at_m1∧x=1φ2→at_l1En(l1) 关于φ1: at_l0∧at_m1∧x=1，验证J2~J4成立如下。 at_l0∧at_m1∧x=1φ1τat_l0∧at_m1∧x=1φ1τ≠l0 at_l0∧at_m1∧x=1φ1l0at_l2∧at_m1φ0 at_l0∧at_m1∧x=1φ1→at_l0En(l0) 因此，根据链式规则，可以得到结论Θ◇(at_l2∧at_m1)。验证图如图3.11所示。 图3.11证明Θ◇( at_l2∧at_m1) （转摘于文献［36］图87） 例3.2优先性规则和验证图的应用示例［36］ 图3.12所示为Peterson算法，该算法主要用于解决互斥问题。假设有两个进程P1和P2，Peterson算法通过布尔变量y1和y2控制它们访问一个共享的单用户资源行为，从而避免发生访问冲突情况。算法基本机制如下： 若进程Pi（i=1,2）试图进入临界区，则将该进程相应的yi设为T； 离开临界区时，将yi设为F。但是当两个进程同时处于等待状态，即算法中P1和P2分别在l4和m4处，这时y1=y2=T，若只有yi控制进程，那么会出现死锁情况。因此，还需要变量s（s={1,2}）作为签名。当y1=y2=T时，在下一个语句中，每个进程将自己的下标数字赋给s作为签名。也就是说，P1执行s∶=1； P2执行s∶=2。增添签名机制，当两个进程都处于等待状态时，若Pi（i=1,2）首先到达等待区，则s≠i，设j为另一个进程的下标，则s=j，它是最后到达等待区的进程，因此Pi具有优先权，即可以进入临界区。 图3.12Peterson算法 （转摘于文献［36］图88） 现在，我们尝试证明 at_l4(瘙綈at_m5,6)ω(at_m5,6)ω(瘙綈at_m5,6)ω(at_l5,6) 上述公式表达的程序属性可以直观描述为： P1在l4位置，P2可能先于P1进入临界区，但最多只能出现一次。也就是说，如果P1正在l4位置，那么有可能一段区间内P2不在m5,6，接着一段区间P2在m5,6，然后P2又不在m5,6，P1进入l5,6。任何一个区间都有可能为空，特别是P2在m5,6的区间内，在P2没有先到m5,6时，允许P1进入l5,6。另外，任何一个区间都有可能是无限的，在这种情况下，不能保证有紧接着的区间和P1进入l5,6。然而，这种情况是不会发生的。实际上，上述公式也是进程之间公平性属性的表述。由于这个公式牵涉到进程执行的次序问题，是一个优先公式，所以我们用优先性规则证明它。 令P=at_l4，显然，若把上式作为结论，对照前面所述的优先性规则，有： q0=at_l5,6，q1=瘙綈at_m5,6，q2=at_m5,6，q3=瘙綈at_m5,6。下面建立4个断言，让它们满足优先性规则的3个前提条件。令4个断言为 φ0: at_l5,6 φ1: at_l4∧(at_m0..3 ∨(at_m4∧s=2)) φ2: at_l4∧at_m5,6 φ3: at_l4∧at_m4∧s=1 注意，P=at_l4表示进程P1处于等待区间，而在整个等待区间内P1从位置l4开始，到l5处结束。在此等待区间，进程P2可在任意处，所以上述φ1、φ2、φ3都采取了与at_l4合取的形式，表明在P1等待时，P2进程的“作为”。同样，q1、q2、q3也可采取与at_l4合取的形式。 φ0是用at_l5,6本身表示的，因为很显然它将终止等待。φ0也是进程P1处在等待区间时的“目标”，因此q0=φ0。 显然，φ1→q1，即φ1→瘙綈at_m5,6。然而,φ1断言在P1处在等待区间时，P2不是处在m0..3就是在m4，但由于s=2，它比P1后“签名”，以致无法进入m5,6。现在，φ1是P2到达at_m4∧s=2状态的完整形式，于是它便体现了φ1的作用，在所有状态中，只要φ1成立，则下一个进入临界区的将是P1，即在所有状态中，P1比P2具有绝对优先权。于是N3中φ1I{φ1∨φ0}成立。实际上，从φ1成立的状态唯一能转换到的状态是at_l5,6。 显然，φ2→at_m5,6，即φ2→q2。从φ2成立状态，程序下一个状态是使φ1∨φ0，即φ2 I{φ2∨φ1∨φ0 }成立。 因为φ1、φ2、φ3表示在P1处于等待区间时，P2所有的状态，也是程序所有状态。鉴于φ1和φ2的直观意义，φ3的直观意义是，在等待位置l4，P2比P1具有优先权，于是虽然φ3→q3，即φ3→瘙綈at_m5,6，但是，下一状态可能是φ2，即φ3I{∨j≤3φj}成立。 显然，p→φ0∨φ1∨φ2∨φ3，所以优先性规则前提全部成立，根据这个规则，得到结论： at_l4(瘙綈at_m5,6)ω(at_m5,6)ω(瘙綈at_m5,6)ω(at_l5,6)。 最后用验证图验证上述属性，如图3.13所示。 图3.13证明at_l4(瘙綈at_m5,6)ω(at_m5,6)ω(瘙綈at_m5,6)ω(at_l5,6) （转摘于文献［36］图89）