（计算机软件与理论专业论文）基于b语言与tpn集成的形式化方法.pdfVIP

华东师范大学计算机系硕士学位论文 学位论文独创性声明 本人所呈交的学位论文是我在导师的指导下进行的研究工作及取得的研究成果。据 我所知，除文中已经注明引用的内容外，本论文不包含其他个人已经发表或撰写过的研究 成果对本文的研究做出重要贡献的个人和集体，均已在文中作了明确说明并表示 矗l 意。 作者签名：盔塑缝 日期：垒丛丘，f 学位论文授权使用声明 本人完全了解华东师范大学有关保留、使用学位论文的规定，学 校有权保留学位论文并向国家主管部门或其指定机构送交论文的电 子版和纸质版。有权将学位论文用于非赢利目的的少量复制并允许论 文进入学校图书馆被查阅。有权将学位论文的内容编入有关数据库进 行检索。有权将学位论文的标题和摘要汇编出版。保密的学位论文在 解密后适用本规定。 学位论文作者签名：喜萝视 名：批戈 日期：立型：垡： 日期：卅6 s 。6 1 仁东帅弛人学汁算机系坝j 。学位论文 摘要 随着人们对软件系统的要求不断地提高，形式化技术得到了充分的发展。过 去人们依赖于优秀的软件工程师来对软件系统可靠性和安全性提供保证，而如 今，人们可以使用已有的形式化技术，按照一定的步骤逐步来开发出满足市场高 要求的软件系统。 然而，目前的形式化技术还比较单一，它们只能满足开发人员对软件系统设 计的某些方面，因此，这种满足有一定局限性和限制。随着研究人员对这些形式 化技术的研究的深入，人们逐渐发现了这些技术和方法本身存在着固有的缺陷。 于是，人们开始对形式化方法的集成这一研究思路的探讨，己有的集成的例子， 如c s p 和b 方法进行的集成，c s p 和z 语言进行的集成。 本文研究的对象的基础有两个，分别是时问p e 仃i 网( t p n ) 和b 方法。t p n 是 一种图形化的形式化技术，它主要应用于实时系统，分布式系统或者并发系统， 它建立在普通的p e t r i 网基础之上，并加以时间约束，和普通p e t r i 网一样，它缺 乏数据建模能力和函数定义能力。b 方法是一种形式化方法，它包含了自己的形 式规格说明语言和验证系统，它适合描述一些顺序系统，但是它也有缺点，它不 适合描述实时系统和并发系统。鉴于以上两种方法各自的缺陷，我们考虑将t p n 和b 方法结合在一起，用b 方法作为t p n 底层的形式化模型，这一点和众多高 级p e t r i 网有非常多的相似之出。将b 方法作为底层模型之后，将b 方法中的某 些元素替换原有t p n 中的概念，从而建立t p n 和b 方法之间映射关系。这种关 系是静态的，我们还需要定义t b 网的动态映射，描述t b 网的动态性质。t b 网是一种高级的p e t r i 网，需要搞清楚这种网的构造方法，它的可达图的构造， 它的活性的定义，本文对于这些问题都进行了探讨。另外，由于t b 网是一种集 成的形式化方法，它应该能够描述实时系统，我们需要指出如何能够证明构造出 来的系统能够满足时间约束。 t b 网是一种集成的形式化方法，它能够使用的领域应该包括了t p n 和b 方 法各自使用的领域，这是因为在集成的过程中，我们使用b 方法来解决t p n 不 能够描述数据类型和定义函数，同时，使用t p n 来解决b 方法不能够描述实时 系统，不能够描述那些t i m e c r i t i c a l 的系统，所以，我们有理由认为t b 网是一 个使用更广泛的形式化方法。 关键词：形式化方法，集成，t p n ，b 方法，t b 网，可达图，时制约束，活性 有界性 华东师范人学计算机系硕i ：学位论文 a b s t r a c t n o w a d a y sp e o p l eb e c o m em u c hm o r es t r i c tw i t hs o f m a r ea n d i t sq u a l i t y ，t h e yn o t o n l y g i v eh i g hs t a n d a r dw i t hm es o r w a r ew h i c hm a k et h es o r w a r em u c hm o r e s o p h i s t i c a t e da n da l s om u c hp e r s o n a 】t ou s e r s b u ta l s ot h e yw a n tt h a tt h es o f l w a r ed o n o tc r a s hv ，h i l et h e ya r eu s i n gt 1 1 e m i nt h ep a s tp e o p l ed 印e n do ne x c e l l e ms o r 、v a r e e n g i n e e rt om a k eas a f ed e s i g n ，b u tn o wt h e yu s ef o r m a lt e c h n i q u e st od e v e l o p s o 建w a r et h a tn e e d sh i g hs a f 文y n o ww h a tp e o p l ew a n tl od oi st od e v e l o pa ss t e p s t l l a tt h ef o m a lm e t h o do rf o m l a ll a l l g u a g et e l l sm e m h o w e v e rf b n n a it e c h n i q u c sa r eb a s e do ns i n g i ef b u n d a t i o n ，t h e ye i t h e rc a n d e s c r i b ed a t as t r u c t u r eo rd a t aa b s t r a c t i o n ，o r t h e yc a nd e s c r i b et h eo p e r a t i o ns c k m a o ft h es o n w a r e w i mt h er e s e a r c h e r s d e e ps t u d y i n g ，t h e yf o u n dt i l a tt l l e s ef o n t l a l t e c 上l i l i q u e sk l v en a t u r a l l yt h e i ro w ns h o n c o m i n g s s op e o p l eb e c o m ei n t e r e s t e di n f o m a lm e l h o da n di t si n t e g r a t i o n ，s u c c e s s f u le x 啪p l el i k ec s pa n dbm e t h o d ，c s p a n dz l a n g u a g e i nt 1 1 i sp a p e r ，w ew a n tt oi i m d d u c et bn e t sw h i c hi n t e g r a t e st p na n dbm e t h o d t bn e t si sh i g hl e v e lp e t “n e t s j u s ta st h es a m ea so t h e rh i g hl e v e ip e t f in e t s ，t b n e t sm a k e st h ebm e t h o da su n d e r l y i n gf o r m a lm o d e lw i t ht p na si t su p p e rm o d e l _ s ow i t hbm e t h o d ，w ec a nd e f i n es o m ed a t as t r u c t u r ea n df u n c t i o nd e f i n i n gi nt b n e t s ，a n dw i t ht h et p n ，w eh a v ea b m t yt od e s c r i b er e a l - t i m es y s t c m so rc o n c u r r e n c y s y s t e m s i nt h i sp a p e rw ea l s ow a n tt oh a v es o m e1 1 9 】1 t si nt b n e t s sp m p e n i e s ，6 r s t l y w ew a n tt oa n a l y z et h er e a c h a b i l i t yo ft bn e t s ，俄曲a b i l i t yi sa ni m p o n a l l tt o o it o a t l a l y z et h ep e t r in e t s ，s ow ew o u i dl i k et oh a v eal o o ka tt l l i sp r o b l e m b e s i d e sw e a l s ow a n t t od e n n et h e1 i v e n e s sa n db o u n d e d n e s so ft bn e t s ，t h e s ep r o b l e m sh a v e v e r yc l o s er e l a t i o nw i t hr e a c h a b i l i c y t h el a s tp m b l e mt 1 1 a tw ew a n tt oh a v ea1 0 0 ka t i st i m ec o n s t r a i n l s a st h et bn e t sh a v et h ea b i l i t yt od e s c r i b er e a l t i m es y s t e m s ，s oi t i sa l s on e c e s s a r yt od i s c u s st h ep r o b l e mo ft i m ec o n s t r a i n t si no r d e rt om a k es u r et h e r e q u i r e m e n ta b o u tt i m ei ss a t i s n e d g e e r a l l ys p e a l ( i n g ，t bn e t sh a v eal a 唱eu s a g et h a l lt p n a n dbm e t h o d ，汀i ti s i m e g r a t e dw i t ht h et w om e t h o d sa n di th a sa d v a n t a g eo ft h et w om e m o d s ， k e yw o r d s ：f o 玎n a lm e t h o d ，i n t e 掣a t i o n ，t p n ，bm e t h o d ，t bn e t s ，r e a c h a b i l i t y ， l i v e n e s s ，b o u n d e d n e s s ，t i m ec o n s t r a i n t s 华东师范大学计算机系硕十学位论文 第一章形式化方法 1 1 形式化方法概述 1 。1 。1 形式化方法基本概述 随着软件系统复杂度的不断增长，软件开发的正确性、可靠性和健壮性成为 软件开发过程中必须加以解决的问题，这就需要种不但在应用上，而且在方法 上，甚至理论上解决问题的手段。因此，形式化方法作为一个引人关注的技术。 形式化方法以数学为基础，其目标是建立精确的、无二义性的语义，对系统 开发的各个阶段进行有效的描述，使系统的结构具有先天的合理性、正确性和良 好的维护性，能较好地满足用户需求。 软件系统的开发过程是问题从客观世界到认识世界再到程序世界的转化过 程，从本质上讲，程序设计过程就是一个等价变换的过程，就是形式化的数学演 算过程。而软件工程就是完成从认识世界到程序世界的转换的方法论。为了实现 符合要求的软件系统，软件规约作为软件工程各个阶段共同遵守的基本规范，应 具有可理解性和精确性以作为程序实现的基础。 一般说来，形式化方法是具有坚实数学基础的方法，通常有推理工具的支持， 可提供一个用于模型分析设计和验证的严格而有效的途径。g r a i n g 对形式化方法 是这样定义的：“以数学为基础的方法，通常有推理工具的支持以便能提供严格 有效的建立计算机系统的模型“1 。”由此可见形式化方法的根本目的是帮助软件 工程师构造正确可靠的计算机系统。它的基本特点是利用数学的概念、方法和工 具来解决设计的f 确性问题。 1 1 2 形式化方法的使用 形式化方法可以两种不同的方式束使用。首先，它可用于生成规范，然后将 此规范作为传统系统开发的基础：第二，形式规范以上述方式产生，然后将其作 为验证程序正确性的依据。 在第一种情况下，数学将被作为生成规范的主要工具。形式化规范的好处在 于：精确、抽象、简明和可操作。操作可以包括规范的一致性检查。原型的自动 生成或通过证明的方法推出规约的一些特殊性质。 在第二种情况下，除上述优点外，还可以利用形式化方法证明规约及其相应 毕东师扎大学计算机系坝i j 学位论文 程序的正确性，以表明程序和其规约的一致性。这样可以使规约具有可能与数学 证明一样的确定性。具有数学精确性的形式化方法最适合子用来设计s a f e t y c r i t i c a l 的系统。使用形式化方法的作用如下： 1 在将非形式化的需求转换成形式化规约的过程中，二义性、需求的增量和矛 盾较易发现； 2 形式模型将导致层次化的半自动甚至是自动化的系统开发方法； 3 和通常的用例测试相比，形式化方法可以用数学的方法验证其正确性； 4 一个经过验证的子系统可以并入一个形式或非形式的大的系统中，这将增加 系统符合规约的可信度； 5 使得开发者可以评估、比较各种不同的设计： 1 1 3 形式化方法发展 自然语言都不是形式化的。真正系统的研究形式化方法是从f r e g e ，罗素等 研究符号逻辑和数理逻辑开始的。计算机出现以后形式化语言超出数学或逻辑学 的范畴开始表示实际工程中的问题。 从1 9 6 7 年f l o y d 发表其论文“a s s i g nm e a n i n g st op r o g r a m s ”以来，程序自 动验证方法的研究己持续了数十年。f l o y d 在文中用“断言式方法”证明程序的 正确性，其特征是将程序或其中完整的子部分的形式语义表示为一阶逻辑的断 言。其中之一是程序必须满足的前提条件，称为酊置条件( p r e c o n d i t i o n ) 或前 置断言( p r e a s s e r ti o n ) ”1 ，另一个则是程序执行之后，其结果必须满足的终结 条件，称为后置条件( p o s t c o n d i t i o n ) 或后置断言( p o s t a s s e r t i o n ) ”1 。程序 是正确的，当且仅当，在前置条件被满足后开始执行，在它执行到终点时，其后 续条件办被满足。对于循环，即程序流程中的回路，存在切点，在此设罱一个 断言，若回路开始执行时，切点上的断言为真，则当循环恢复到该切点时，其断 言仍应为真，即所谓的“循环不变式”。 1 9 6 9 年，h o a r e 发表了“计算机程序设计的公理基础”一文”1 ，针对高级语言 整理出成套的具有自然推理性的推理规则，现在人们称这一方法为h o a r e 逻辑。 这是一种含有程序公理和推理规则的形式逻辑推理系统，由于这种逻辑可在计算 机上实现，人们使用它来证明程序的部分正确性。这种程序正确性验证方法称为 “公理化方法”。这是迄今关于程序验证最为完整并为计算机界所普遍接受和肯 定的方法。 华东师范大学汁算机系硕i ! 学位论史 1 1 4 与形式化方法相关的若干个术语 半形式化方法1 1 4 l ：在软件开发过程中，人们可以使用许多方法，但它们中的 大多数并不包含了软件开发过程中的所有步骤，而是包含了其中某些步骤，例如： s a d t ( s t m c t u r e d a n a l y s i s d e s i g n t e c h n i q u e ) ，u m l ，o o a 等，人们可以使用这些 技术来分析系统的需求，但是分析的结果却是一个半形式化的规格说明，也就是 说它包含了形式化的概念，非形式化的概念以及图形化的概念，然而它们没有包 含形式化的语义。使用半形式化的方法分析问题会给我们带来混淆和二义性，因 为非形式化的规格说明不具有明确的语义。因此，半形式化工具不能够用来进行 形式推理，对于形式化开发而言，采用这种方法并不好。 形式化语言| 1 4 l ：形式化语言是一种精确定义得语法和语义，例如，z 语言， 代数规约语言( a l g e b r a i cs p e c i f i c a t i o nl a n g u a g e ) ，人们可以使用这些语言编 写系统的规格说明，描述系统的模型或者行为。 形式化系统i 】4 l ：形式化系统由形式化语言和验证系统( 或者说形式化推理系 统) 组成。 形式化方法| 1 4 l ：形式化方法主要有形式化语占和形式化推理系统或形式化证 明系统组成，其中还包含精化系统，例如，c s p ( c o m m u n l c a t i n gs e q u e n t j a l p r o c e s s e s ) ，c c s ( c a l c u l u so fc o m m u n i c a t i n gs y s t e m s ) ，v d m ( v i e n n a d e v e l o p m e n tm e t h o d ) ，b 方法( bm e t h o d ) 。 形式化的开发1 1 4 l ：开发的过程包括了从非形式化的需求和可执行代码整个阶 段。他也包括了形式化的推理。形式化开发指的是通过使用预定义好的规则( 重 写，精化，综合) 等手段将系统的规格说明转换成代码的系统转换。 1 2 形式化方法研究内容 通过前面的小节，我们知道形式化方法优点，使用方法和作用，但是我们还 需要知道形式化方法的研究内容，它包含了形式化规约和形式化验证两部分。 1 2 1 形式规约 形式化方法的一个重要研究内容是形式规约( f o r m a ls p e c i f i c a t i o n ) ，也称 形式规范或形式化描述或形式化说明) ，它是对程序“做什么”( w h a tt od o ) 的 数学描述，是用具有精确语义的形式语苦书写的程序功能描述，它是设计和编制 程序的出发点，也是验证程序是否正确的依据。对形式规约通常要讨论其一致性 华东师祀人学计算机系硕 学位论文 ( 自身无矛盾) 和完整性( 是否完全、无遗漏地刻画所要描述的对象) 等性质“1 ”3 。 不同的形式规约方法要求不同的形式规约语言，即用于书写形式规约的语言 ( 也称形式化描述语占) ，它们有一个共同的特点，每种规约语言均由基本成分和 构造成分两部分构成。前者用来描述基本规约，后者把基本部分组合成大规约。 构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。 1 2 2 形式验证 形式化方法的另一重要研究内容是形式验证( f o r m a lv e r i f i c a t i o n ) ”。 形式验证与形式规约之间具有紧密的联系，形式验证就是验证己有的程序( 系统) 是否满足其规约的要求，它也是形式化方法所要解决的核心问题之一。 传统的验证方法包括模拟( s i m u l a t i o n ) 和测试( t e s t i n g ) ，它们都是通过实 验的方法对系统进行查错。模拟和测试分别在系统抽象模型和实际系统上进行， 一般的方法是在系统的某点给予输入，观察在另一点的输出，这些方法花费很大， 而且由于实验所能涵盖的系统行为有限，很难找出所有潜在的错误。基于此早期 的形式验证主要研究如何使用数学方法，严格证明一个程序的征确性( 即程序验 证) 。目前常见的形式验证方法主要可分为两类：演绎验证( d e d u c t i v ev e r i f i c a t i o n ) 和模型检测( m o d e lc h e c k i n g ) 。 1 3 形式化方法的集成 现实世界的系统并不是将系统的特点分割开来，大多数时候，给定的一个系 统往往要处理不同的方面，因此，在作系统开发和设计的过程是，仅仅通过使用 单一的形式化方法来完成系统的分析、设计、丌发、验证等任务是不现实，也是 很困难的，由于软件系统的复杂性和多面性，在丌发过程中使用集成化的形式化 方法是很有好处的。 形式化方法集成与之前的单一的形式化方法相比，区别在于，原有的形式化 方法可能使用在一个相对比较单一的环境中，然而通过集成，两种或两种以上的 形式化方法被联系到一个统一的环境中，相对于原有单一的形式化方法，这种集 成后的形式化方法可能使用面更广，它能够反映现实系统的不同特点，例如，数 据，行为和并发性等等。许多贴近现实世界的系统往往捌有许多特点，很长时间 以来，开发技术专注于某一个特点，并且在这一特点上进行加强( 结构化分析， 抽象数据类型等等) 。这导致只是对软件部分特点进行了描述，不利于全面了解 软件系统的特点。现在研究人员在集成化方面做了很多工作，将它们集成到一个 统一的环境中。这方面的例子有，j s d 集成了结构化分析和c s p ，原有的结构化分 华东帅越人学汁算村【系倾i 学位论文 析并没有考虑到函数本身是否可行”“，通过集成开发人员可以通过c s p 考虑方 法的可行性。另外还有r a i s e ，它集成了v d m 和p e t r i 网，c s p 2 b 集成了c s p 和b 方法 1 ，等等。 在形式化方法中，有些侧重描述系统的状态( s t a t e o r i e n t e d ) ，例如z 语言， b 方法，v d m ，有限状态自动机；有些侧重描述系统过程和并发性( p r o c e s s o r i e n t ed ) ， 例如p e t r i 网，c s p ，c c s 等等；有些侧重描述系统的属性( p r o p e r t y o r i e n t e d ) ，例 如a s l ，o b j 等等。我们将形式化方法集成的几种形式综合如下： 状态和行为的结合 zo rb 午| i a l g e b r a i cf o r m a l i s m 状态和状态的结台 z 雨ib 状态和过程的结台 zo rb 年r l c c so rc s po rp e t r i n e t s 行为硐i 过程的结台 a l g e b r a l cf o r m a li s m 年u c s po rc c so rp e t r i n e t s 表1 1 几种集成的方式 本文将要介绍的是t p n 和b 方法集成的形式化方法，t p n 是一种图形化的形式 化工具，它能够用来描述一些实时系统，反映系统的时间需求，而b 方法是一种 形式化方法，它包含了形式规格说明语言、精化和形式化验证等内容。将两者结 合，能够弥补b 方法不能描述实时系统和分布之系统的缺点，同时b 方法能够弥补 t p n 不能够定义数据结构，不能够定义操作的语义的缺点。在集成了t p n 和b 方法 之后，许多原来在t p n 中研究过的性质可以在集成后的形式化方法中加以研究， 比如可达性，可调度性。同时原有t p n 的概念由于引入了b 方法，必然要发生变化， 所以需要对这些基本的概念作修改或者重新指出新的含义，比如，变迁的使能、 激发，激发后的标识等等；同样，原来在b 方法中研究的问题也可以在集成后的 形式化方法中进行研究，原来在b 方法中不能研究的问题现在也能够研究了，比 如，时间约束性质等等。 1 4 本文的结构 从第二章开始将进入正文阶段，其中第二章描述了b 方法，主要介绍b 方法的 一些基础知识。第三章介绍p e t r i 和时间p e t r i 网。第四章介绍了t b 网，主要介绍 t p n 如何b 方法结合，讨论如何构造一个t b 网，以及如何改造。第五章介绍t b 网的 若干性质，比如可达性，活性，有界性。最后一章是总结本文的内容，并对今后 的工作一个描述。 华东师范大学计算机系硕士学位论文 2 1b 的历史 第二章b 方法 2 0 世纪8 0 年代初期，研究人员丌始了有关规格说明语言z 的研究，这一研 究形成了b 语言一方法的背景。 对b 语言一方法和抽象机符号表示法( a m n ) 的研究开始于1 9 8 5 年至1 9 8 8 年，由牛津大学程序设计研究组( p r o g r a i t l i i l i n gr e s e a r c hg r o u p ，p r g ) 在一项 为期三年的r & d 项目研制开发的】。j - ra b r i a l 在a m n 和b 语言一方法方面 起了最特殊的重要作用，除此之外，c c m o r g a n ，p g a r d i n e r 以及其他从事b 项 目的人员也对该项目做出了有影响而且重要的贡献。 在法国，随着g e c a l s m o n 公司和m a t r a 运输公司使用b 方法开发铁路安 全警报应用系统，b 方法的应用还在不断发展，这些应用还包括一个地铁速度控 制系统，以及个第二期的速度控制系统1 6 】。 1 9 9 3 年，b ，c o r e ( 英国) 公司接管了b 方法的进一步丌发工作，并于1 9 9 4 年获得b t o o i k i t 以及相关语言的全部知识产权。b t o o i k i t 于1 9 9 4 年投放市场。 b t o o l k i t 是由一系列的软件工具组成，是为了支持构建健壮或者形式化的软件 系统开发【1 2 1 。 2 2b 方法简介 从软件系统的需求定义，到软件的规格说明，到最后的可执行软件组件的实 现，b 方法可以使程序和程序的规格说明处于一个统一的数学框架之下，以一种 基于集合理论的符号表示法来书写。这种数学框架是通过用谓词变换和扩展的 e w d 日k s t r a 最弱f j i f 置条件演算提供的。 通常最初的需求是以自然语言表示，或者使用图表，逻辑表格，p e t r i 网络等 方法共同描述，b 方法用于开发的过程主要在于构造反映需求的所有描述模型， 描述系统的主要状念，这些状态需要满足的属性( 不变式) ，以及这些状态通过 服务( 操作) 的变化。由此得到的模型就是反应了系统需要做什么( 即实现系统 的功能) 。 然后，我们就可以对这样的模型迸行精化，这是一个迭代的过程，直到得到 该软件系统的完整实现。b 方法中存在几种实现规格说明的精化可以通过各种标 准选择解决方案，这些标准可以是处理速度，计算的精确性证明的简洁性等。 也可以将精化作为一种规格况明技术，在精化过程中逐步包含形式化开发问题中 牛东帅范人学计算机系硕i j 学位论文 的细节。形式化规格说明是逐步而不是直接形成的。 因此，在系统开发中使用的b 方法，包括以下几方面： 消除需求说明中的歧义性， 构造与需求相致的规格说明，也就是模型， 对软件系统的开发过程当中，对每一步都形式化的规范其规格说明， 通过数学的证明保证了模型的连贯性，以及最终程序与模型的一致性。在具 体的应用中，这些证明过程只能使用自动证明工具来实现。 2 。3b 方法的基础 2 3 1 谓词 b 方法中使用的谓词( p r e d i c a t e ) 是一阶谓词逻辑吲的一部分。 谓词首先表达的是个公式，其次表达的是与某些数据相联系性质。 在b 方法中直接使用谓词来表示与组件数据相联系的性质 谓词既可以作为证明的前提，它表示的是解决问题的先决条件，谓词也 可以是证明的目标，它能够被证明也能够被否定，它表示的目标的结果。 b 方法使用的谓词有： ( 1 ) 简单谓阋操作得到新的谓词( 合取，析取，否定，蕴含，等价) ， 给定谓词p 和q ，分别为p 八q ，p v q 、尸，p jq ，p q ( 2 ) 量化谓词( 全称谓词，存在谓词) ， 给定一个变量x 和一个谓词p ，vx p 称为是一个全称量化谓词，表 示无论用什么表达式替换p 罩的x ，得到的推演式一定可以是一个断言。 给定一个变量x 和一个谓词p ，j x p 称为是一个存在量化谓词，表示 存在一个表达式替换p 里的x ，得到的推演式可以是一个断言。 ( 3 ) 包含谓词，如元素e 属于集合s 的谓词表示为：e s ( 4 ) 算术比较谓词。 2 3 2 表达式 表达式【5 】( e x p r e s s i o n ) 是操作数据的一种公式，b 方法中使用的表达式有以下 几种： ( 1 ) 基本表达式； ( 2 ) 布尔表达式； 华东师范人学计算机系硕= 匕学位论文 ( 3 ) ( 4 ) ( 5 ) ( 6 ) 代数表达式： 集合表达式( 空集，) ： 集合构造表达式( 子集集合，集合的并，集合的交， 关系表达式( 同一，取反，投影，合成，定义域，值域， 其中常用的关系是取反关系，定义域，值域的表达式 给定关系r u h v ，其定义如下 r - = d f ( b ，a ) 1 ( b ，a ) v u 八( b ，a ) r d o m ( r ) = d f a ja u j b ，( b v ( a ，b ) r ) ) r a n ( r ) = d f d o m ( r “) ( 7 ) 函数表达式( 偏函数，全函数，单射，满射，双射，) ； 偏函数：s + f d f ff s 七t ( vx sy 1 ，y 2 t ( f ( x ) = y 1 八 f ( x ) = y 2 ) j y l = y 2 ) 全函数：s 斗t = d f f i 拈s + t 八d o m ( f ) = s 单射：s 一 t = d f ( f 【f s + t 八( v x l ，x 2 d o m ( f ) j f ( x 1 ) f ( x 2 ) ) ) 满射：s _ t = d f f l f s + t 八r a j l ( d = s ) 双射：s 一 t = 邯s t 八s 一 t ( 8 ) 函数构造表达式( 常函数，x 表达式等) ：x 表达式提供一种给定表达式 表示函数的方法。 2 3 3 组件 b 组件包含了抽象机，精化和实现。在一个组件中，通过使用子句来标志抽 象机的动念描述和静态描述。下面是一些子旬的说明f 1 0 】： 组件头 m a c h i i n e 该子旬描述了抽象机的名称和抽象机所拥有的参数。 r e f n q e m e n t 该子句描述了精化说明。 l m p l e m e n m t a t l o n实现名称说明。 r e f n q e s 被精化组付的说明。 可见性子旬 i m p o i u s 该子句包含了一个( 可能重命名的) 被引入的机器的列表，只能在实 现中使用，_ l _ j 来输入抽象机的操作，而不是数据。 s e e s 描述了组件之间的“查看”关系，查看是指能够引用的属性。 i n c l u d e s 描述了组件之间的“包含”关系，包含是指能够引用的属性和操作。 定义子句： 描述数据的子旬( 静态方面) 华东师范人学计算机系倾l 学位论文 s e t s 列举集台的说明。 p r o p e r t i e s对抽象机内的常带属性说明。 v a r l a b l e s 变鼙的说明。 t n v a r l a n t 对变 茎 不变式的说明。 c o n s t a n t s 抽象机内的常量说明。 描述操作的子句( 动态方面) r n i t i a l l s a 丁l o n 变量初始化说明。 p r o m o t e s 说明被包含或被输入的机器中组件欲使用的操作。 o p e r a t i o n s 包含操作头和操作体的操作说明 2 4 抽象机 抽象机是b 方法的一个基本机制它是与程序语言中模块、类或抽象数据类 型非常接近的概念。 抽象机包含变量和操作两部分内容，变量首先描述了抽象机的静态行为，它 们构成了状态的组成部分，其次是有关不变式的部分，这是一个逻辑语句，它清 楚的表达了系统的静态逻辑规则，这种不变式是基于有关变量并利用谓词演算和 集合论的形式语言描述的。 抽象机中另个包含的要素是操作， 扮演的角色就是修改抽象机器中的状态 操作描述了抽象机的动态行为，操作所 当然这种修改必须是在不变式的限制范 围之内。需要注意的是一部抽象机的定义只给了其潜在“用户”去激活这些操作 的能力，而不允许它们直接去访问机器的状态，因为它使得能够修改变量并相应 修改操作的方式去精化机器，同时又能够保证操作的名字不变。 一个普通的抽象机可以写成如下形式f 5 】： m a c h l n e n ( p ) c o n s t r a i n t sc s e t ss t c o n s t a n t sk p r o p e r t i e sp v a r l a b l e sv d e f i n l t i o n sd 附v a r i a n t si i n l t j a l l s a t l o nt a s s e r t l o nj o p e r a t l o n s y o p ( x ) p r e q t h e n s 华东师范大学计算机系硕卜学位论文 e n d e n d 下面分别介绍各个子句： 在m a c h i n e 子句中给出抽象机的名称n ，同时在机器名称的旁边有自己的 输入赋值标量参数( 以小写字母书写) 或者以赋值集合的列表( 以大写字母书写) ， 这些参数的逻辑特性在该机器的c o n s t r a i n t s 子旬中得到说明。我们假设这 些参数彼此是独立的，因此它们和其它各集合参数彼此是不关联的。 如果s e t s 子句出现了，那么该子句的形式为： s e t d e ；s e t d e 矗； 每个s e t d e 都对应于b 中枚举集合或者延期集合( d e f e r r e ds e t ) ，枚举集合的 表示方式如下：s = f v a l l ，v a l 2 v a l n 采用这种形式时，枚举集合s 将集合定义成为具有n 个元素的集合，并将它 们列举出来。也可以将集合的表示抽象化，只是定义出一个集合名：s ，这里s 代表的是一个延期集合，它表示的是一个非空有限集合，其具体形式需要在后面 的精化和实现过程中确定。无论是枚举集合还是延期集合，这种给定集合都与抽 象机的集合参数一样，他们表示的都是独立的类型。 c o n s t a n t s 子旬定义的是抽象机中的常量，表示为c o “l ，c o n 。它说明了 这n 项数据在抽象机中只是以只读的形式被引用，换句话说，c o n 。不能出现在广 义代换的左侧或者操作调用的左侧。 p r o p e r t i e s 子句定义了集合和常量的逻辑特性。它包含谓词，通常是一个 合取公式，只包含有常量和集合，而且是那些在当前作用域内的常量、集合和参 数标志符。对于列在c o n s t a n t s 予旬中的每个c o n s t a n t ，必须提供类型约束 c o n s t a n t t y p e 或者c o n s t a n 仁v a l u e ，其中v a l u e 的类型应机械的确定。这一子句 对常量的作用就像r n v a r i a n t 对变量的作用。另外，p r o p e r t i e s 子句不能引 用机器的形式参数，这限制基本上是为了避免循环的引用。 机器变量列于v a r i a b l e s 子旬中。它是用逗号分割的标志符v a r l ，v a r 2 这些标志符属于机器的可写数据，但是它们不能够出现在任何其它机器表达式的 左端。 定义( d e f i n i t i o n s ) ：该予句的表示形式由如下表达式组成：d a t a = d f v a l 。其 中d a t a 。是一个标志符或带参数的函数名f ( p a r a m s ) ，v a i 包括范围变量、常量和函 数参数。这些等式在机器的其余部分起着宏定义的作用。 不变式是对变量起约束作用，包括变量类型的定义，在机器的n n ，a r i a n t 子句中说明。和p r o p e r t i e s 一样，它也是由谓词组成，通常是多个谓词的合 取式，式中包括变量标志符、常量、集合和机器参数，以及及其作用域内的那些 华东师范大学计算机系硕l 一学位论文 数据项。 机器在i n i t i a l i s a t i o n 中进行初始化操作。它是一个单一的广义代换，对 、r i a b l e s 子句中的每一个变量进行说明，定义初始值的可能范围。 o p e r a t i o n s 给出了机器的操作定义，该部分是操作的定义列表： o p h e a d e 。1 2 d p p d e “ o p h e a d e r n = d f o p d e f n o p h e a d e r 的一般表示形式为： y 一o p n a m e ( x ) 输入参数x 列在操作名之后，输出参数y 列在从操作名开始的箭头左侧。如 果操作无输入和输出，则y 一和( x ) 都可以省略。o p d e f 是一个广义代换，机器变 量和列表y 中变量可出现在o p d e f 中的赋值或操作访问的左侧，机器的作用域内 的任何数据以及变量x 也可以出现在代换中的任何地方。 下面给出一个抽象机的基本例子： m a c h l n e b o o k i n g ( m a x s e a t ) c o n s t r ar n t s m a x - s e a t n a t v a r i a b l e s s e a i i n v a r l a n t s e a t 0 m a xs e a t i n i t i a l i s a t i o n s e a t ：= m a xs e a t o p e r a t i o n s b o o k = p r e 0 s e a t t h e n s e a t ：= s e a l 1 e n d c a n c e l = p r e s e a t m a x _ _ s e a t t h e n s e a t ：= s e a t + 1 e n d e n d 这个例子定义了一个简单的作为座位预定抽象机，完成座位的定购和取消。 抽象机的输入参数m a x _ s e a t 定义了座位的总数，两个操作b o o k 和c a n c e 】的定义 1 乍东师范人学汁算机系顺i 。学位论文 体现了操作的规格说明，它们表达的只是操作要完成的任务，而不是操作的具体 实现细节。其中的p r e 子句可以看作是操作执行的前条件。 操作的行为规格说明使用一种广义代换的伪代码，从谓词转换的角度对代换 进行形式化的定义。抽象机的操作包括一个前置条件，是一个表示操作执行的前 条件的表达式。操作同时包含一个动作，是一个表示抽象机变量如何进行处理的 代换。抽象机的规格说明阶段定义，但是不允许出现具体的代换。在规格说明阶 段要描述的是做什么，也就是，操作需要完成的动作，而不是如何完成。在并发 的多个代换中。没有给出几个代换的确切应用顺序，这种不确定性是有好处的， 它为后续的丌发留下一一个选择余地。 下面我们给出以下广义代换的证明义务( p r o o f o b l 堙a t i o n ) ，如下： ( 1 ) “参数存在”法则：保证存在可能的机器变量参数值，需要满足如下约 束：j p c ( 2 ) “常量和集合参数存在”法则：假定机器的约束条件，存在满足机器的 特性的集合和常量。 c j j ( s t ，k ) p ( 3 ) “不变式保持”法则：如果操作总在前置条件内被调用，则每一操作都 保持其不变式为真。 c 八p 八i j 八q j v 】i ( 4 ) “初始化”法则：初始状态在机器的约束和特性下建立不变式。 c 八p j 【t 】i ( 5 ) “断言保持”法则：需要建立起断言的证明义务。 c a p 八1 j j 在上述给定的b 0 0 k 机器中没有a s s e r t i o n s 子句和常量c o n s t a n t s 子 旬，所以满足上述证明义务中三条法则： js e a t ( s e a t o m a ) 【一s e a l ) m a ) ( 一s e a t na ：r 八s e a t o m a x s 毛a t 八( 0 s e a t v s e a t p ( s ) ，为集合s 上的变换，因此s t r ( s ) 可以作为集合变换 器的转换。 然后是精化的形式化定义：在抽象机m ( 变量x 和对于集合s 得不变式x s ) 的两个通用代换s 和t 对于s 的任意子集a ，集合变换器s t r ( s ) 在a 处的值均包 含于s t r ( t ) 在同样集合a 处的值，如下： s t = d f va ( a s = s t “s ) ( a ) s t r ( t ) ( a ) 用户需要以机器能理解的规格说明的方式同这些机器进行交互，给出规格说 明，如果实际机器满足这些期望，并与规格说明描述的动作一致，那么机器就能 将这些规格说明转化为最后的实现，而且这些实现与用户无关，这其实就是形式 化方法的根本。 另一方面，编程