（计算机软件与理论专业论文）基于抽象状态机的计算模型及应用研究.pdf

上海交通大学博士学位论文摘要 摘要 抽象状态机( a b s t r a c ts t a t em a c h i n e s ，a s m ) 的基本思想可以追溯到上个世 纪8 0 年代。a s m 的发明者y u r ig u r e v i c h 从数学领域转到计算机领域发现这样的 现象：一个程序语言在不同的编译器下有着不同的编译。这就存在一个问题： 究竟一个程序语言的确切语义是什么? 为了上面的问题，y u r ig u r e v i e h 进行研究的初衷是：( 1 ) 为c h u r c h - t u r i n g 论 题引入资源边界的限制；( 2 ) 采用动态结构( d y n a m i cs t r u c t u r e s ) 定义更为抽象的 计算设备。y u r ig u r e v i c h 从数学中得到了启迪，任何静态的数学实体，都可以 表示为一阶结构，因而算法的每个状态为一阶结构。计算( c o m p u t a t i o n ) 就是状 态的进化( e v o l v i n g ) 。可以容易的用一个函数来表示一个关系，使得一阶结构 中可以只含有函数，而只有函数运算的结构在泛代数( u n i v e r s a la i g c b r a s ) q a 称 为代数。因此这种模型最初被分别称为动态结构( d y n a m i cs t r u c t u r e s ) ，动态代 数( d y n a m i ca l g e b r a s ) ，以及进化代数( e v o l v i n ga l g e b r a s ) 。最终，通过多年的研 究，人们发现进化代数实际上是d i j k s t r a 的抽象机( a b s t r a c tm a c h i n e ) 的基本概念 和利用t a r s k i 的结构作为一般的抽象状态( a b s t r a c ts t a t e s ) 的基本思想的完美结 合，最终称为抽象状态机。所以a s m = a b s t r a c ts t a t e + a b s t r a c tm a c h i n e 。 目前，a s m 已经从一种思想发展成一种成熟的模型，一种语言，一种被国 际标准化组织承认的、在软件和硬件规约中广泛使用的工具。同时a s m 的工业 用软件开发环境已经初露端倪，并且已经得到成功的运用。值得一提的是， 在m i e r o s o f l 的大力支持和推动下，已经产生了a s ml a n g u a g e ( f l f l a s m l ) ，并整合 到了n e t 开发环境中。 本文选择抽象状态机作为研究目标，探讨其理论基础与应用环境，主要内 容有如下几个方面： ( 1 ) 从其数学基础出发，综合已有的研究成果，系统的构造基础抽象状态 机，复合抽象状态机，同步多a g e n t 抽象状态机和异步多a g e n t 抽象状态机，从而 为系统与软件提供一个有完善数学背景的设计平台与方法。 ( 2 ) 受g u r e v i c h 的顺序抽象状态机论题( s e q u e n t i a la s mt h e s i s ) 启发，初步系 统地讨论了抽象状态机与算法之间的基础联系。特别是对于顺序算法，综合已 有的理论工作，系统地论证了所有的顺序算法都可以被一个适当的顺序抽象状 态机用同样的步调( s t e pf o rs t e p ) 模拟。同时针对非确定性算法也作了相关的探 上海交通大学博士学位论文摘要 讨。 ( 3 ) 为w e b 月e 务中的b u s i n e s sp r o c e s se x e c u t i o nl a n g u a g ef o rw e bs e r - v i e e s ( b p e l ) 定义了一个分布式抽象状态机( d a s m ) ，基于抽象状态机的理论 背景，b p e l 有更清晰和完备的数学意义。整个模型的执行是由协作与反应行为 来刻画，具备扩充复杂业务过程的能力。 ( 4 ) 通过建立抽象状态机与关系转换器之间的联系，详细探讨了电子商 务中的若干验证问题，并给出了闯题的形式化方式。相对于其他的关系转换 器，a s m 关系转换器具备更强的计算能力。并且利用已有的逻辑与模型验证的 结论。说明了验证问题的复杂性范围，以及为了限制验证问题的复杂性所需要 做的约束。 ( 5 ) 基于抽象状态机来刻画移动对象的语义。基于抽象状态机建立的移动系 统依赖于语义规范单元的交互抽象，移动性通过通讯拓扑结构的动态变化来表 示。并且参考进程代数的形式系统，同样强调通讯的通道可以通过其它通道传 输，从而进程可以动态地获取新通道。相比较于进程代数，基于抽象状态机的 移动系统在软件工程方面易于实现和扩展。 关键词：抽象状态机，计算模型，系统设计。交互计算，电子商务，移动系统 一i i 上海交通大学博士学位论文 a b s t r a c t a b s t r a c t t h eb a s i ci d e ao fa b s t r a c ts t a t em a c h i n e s ( a s m ) c a nb et r a c e db a c kt o1 9 8 0 s i nt h el a s tc e n t u r y y u r ig u r e v i c h ，t h ef o u n d e ro fa b s t r a c ts t a t em a c h i n e s ，o b s e r v e d ap h e n o m e n o nt h a tap r o g r a m m i n gl a n g u a g eh a sd i f f e r e n tc o m p i l a t i o n si nd i f f e r e n t c o m p i l e r s ，s oi ti m p l i c a t e sap r o b l e m ：w h a ti st h ee x a c ts e m a n t i c so fap r o g r a m m i n g l a n g u a g e ? f o rt h ea b o v ep r o b l e m ，t h eo r i g i n a li n t e n t i o no f y u r ig u r e v i c h sr e s e a r c hw a s ：( 1 ) p r o v i d i n gar e s t r i c t i o na b o u tb o u n d e dr e s o u r c ef o rc h u r c h - t u r i n gt h e s i s ；( 2 ) d e f i n i n g a b s t r a c tc o m p u t i n gd e v i c ew i t hd y n a m i cs t r u c t u r e s h eg o ti n s p i r a t i o nf r o mm a t h ，i e a n ys t a t i cm a t h e m a t i c a le n t i t i e sc a nb eao n e o r d e rs t r u c t u r e ，s oe a c hs t a t eo faa l g o - r i t h mi sao n e - o r d e rs t r u c t u r e t h ec o m p u t a t i o ni sae v o l v e m e n to ft h es t a t e s i ti s e a s yt od e n o t ea r e l a t i o nb yaf u n c t i o na n dm a k eao n e - o r d e rs t r u c t u r eo n l yc o n t a i n i n g f u n c t i o n s s i n c eas t r u c t u r eo n l yw i t hf u n c t i o n si sc a l l e da l g e b r ai nu n i v e r s a la l g e b r a s ， t h ec o m p u t a t i o nm o d e l w a si n i t i a l l yc a l l e dd y n a m i cs t r u c t u r e s ，d y n a m i ca l g e b r a so r e v o l v i n ga l g e b r a s e v e n t u a l l y , t h r o u g hm a n yy e a r so f r e s e a r c h ，w ek n o w t h ee v o l v i n g a l g e b r a si sap e r f e c tc o m b i n a t i o no fd i j k s t r a sa b s t r a c tm a c h i n ea n da b s t r a c ts t a t e so f t a r s k is t r u c t u r e 。s oi ti sf i n a l l yc a l l e da b s t r a c ts t a t em a c h i n e s ，i e a s m = a b s t r a c t s t a t e + a b s t r a c tm a c h i n e a tt h ep r e s e n tt i m e ，f r o ma ni d e aa s mh a sb e c o m eam a t u r em o d e l ，al a n g u a g e a n dat o o lw i d e l yu s e di ns o f t w a r ea n dh a r d w a r es p e c i f i c a t i o n s a tt h es a m et i m e ， a s m si n d u s t r i a ls o f t w a r ed e v e l o p m e n te n v i r o n m e n tw a sc r e a t e da n ds u c c e s s f u li n m a n ya p p l i c a t i o n s s p e c i a l l y , w i t hm i c r o s o f t ss u p p o r ta n dp r o m o t i o n ，t h el a n g u a g e a s m lc a m ei n t ob e i n g ，a n dw a si n t e g r a t e di n n e td e v e l o p m e n te n v i r o n m e n t t h i sp a p e rf o c u s e so na b s t r a c ts t a t em a c h i n e s a n ds t u d i e si t st h e o r yf o u n d a t i o n a n da p p l i c a t i o ne n v i r o n m e n t t h ef o l l o w i n ga r es o m em a i np a r t so f t h i sp a p e r ： ( 1 ) b a s e do na b s t r a c ts t a t em a c h i n e s m a t h e m a t i c a lf o u n d a t i o na n dal o to fr e - s e a r c hr e s u l t s ，s y s t e m a t i c a l l yc o n s t r u c t sb a s i ca s m ，c o m p o s i t i o na s m ，s y n c h r o n o u s m u l t i a g e n ta s m a n da s y n c h r o n o u sm u l t i a g e n ta s ms t e pb ys t e p ，s op r o v i d e sad e - s i g nm e t h o d o l o g yw i t hc o n c r e t em a t hb a c k g r o u n df o rs y s t e m sa n ds o f t w a r e s ( 2 ) i n s p i r e db yt h es e q u e n t i a la s mt h e s i s ，d i s c u s s e st h eb a s i cc o n n e c t i o nb e - i i i 上海交通大学博士学位论文a b s t r a c t t w e e na b s t r a c ts t a t em a c h i n e sa n da l g o r i t h m s p e c i a l l yf o rs e q u e n t i a la l g o r i t h m , s y s t e m a t i c a l l ye x p o u n d sa n dp r o v e st h a te a c hs e q u e n d a la l g o r i t h mc a db es i m u l a t e db ya a p p r o p r i a t es e q u e n t i a la s ms t e pf o rs t e p f u r t h e r m o r ed i s c u s s e ss o m er e l e v a n tp r o b - l e m so f n o n - d e t e r m i n i s t i ca l g o r i t h m ( 3 ) s y s t e m a t i c a l l yc o n s t r u c t sad i s t r i b u t e da s m f o rb u s i n e s sp r o c e s se x e c u t i o n l a n g u a g ef o rw e bs e r v i c e s ( b p e l ) ，t h e nb a s e do nt h et h e o r yb a c k g r o u n do fa s m ， p r o v i d e sad i s t i n c ta n dc o m p l e t em a t h e m a t i c sm e a n i n g sf o rb p e l t h ew h o l em o d e l i sc o n s t r u c t e db yc o o p e r a t i v ea n dr e a c t i v eb e h a v i o r s ，a n dw i t ht h ec a p a c i t yo f c o m p l e x b u s i n e s sp r o c e s s ( 4 ) s e t su pac o n n e c t i o nb e t w e e na b s t r a c ts t a t em a c h i n e sa n dr e l a t i o n a lt r a n s - d u c e r , t h e ni nd e t a i l d i s c u s s e ss o m ev e r i f i c a t i o i lp r o b l e m si ne l e c t r o n i cb u s i n e s sa n d p u t sf o r w a r dt h ef o r m a lm e t h o d sf o rt h e s ep r o b l e m s c o m p a r e dt oo t h e rr e l a t i o n a l t r a n s d u c e r s ，t h ea s mr e l a t i o n a lt r a n s d u c e rh a ss t r o n g e rc o m p u t i n gp o w e r b a s e do n s o m er e s e a r c hr e s u l t si nl o g i ca n dm o d e lc h e c k i n g ，g e t st h ec o m p l e x i t ys c o p eo ft h e s e p r o b l e m s ，a sw e l la st h er e s t r i c t i o n sf o rt h e m ( 5 ) s p e c i f i e st h es e m a n t i c so f a c t i v em o b i l eo b j e c t s 晰ma b s t r a c ts t a t em a c h i n e s t h em o b i l es y s t e mi sb a s e do nt h ee x p l i c i ti n t e r a c t i o na b s t r a c t i o nb e t w e e nu n i t so f s p e c i f i c a t i o n ，a n dt h em o b i l i t yi se x p r e s s e db yc h a n g i n gt h ec o m m u n i c a t i o nt o p o l o g y d y n a m i c a l l y r e f e r r i n gt ot h ep r o c e s sa l g e b r a ，a l s om a k e st h ec h a n n e l so f c o m m u n i c a - t i o nc a l lb et r a n s m i t t e do v e ro t h e rc h a n n e l s ，s ot h a ta p r o c e s sc a nd y n a m i c a l l ya c q u i r e n e wc h a n n e l s c o m p a r e dt op r o c e s sa l g e b r a , t h em o b i l es y s t e mb a s e do na b s t r a c ts t a t e m a c h i n e si se a s yt or e a l i z e da n de x t e n d e di ns o f t w a r ee n g i n e e r i n g ， k e yw o r d s ： a b s t r a c ts t a t e m a c h i n e s ，c o m p u t i n gm o d e l ，s y s t e m d e s i g n ，i n t e r a c t i v ec o m p u t a t i o n ，e l e c t r o n i cb u s i n e s s ，m o b i l es y s t e m i v 上海交通大学博士学位论文插图 插图 4 1 抽象状态机函数，关系0 位爱的分类，2 9 6 1 生产单元 6 2 t r a n s p o r t b e l l 的麒硼模硝， 6 3 d e l i v e r p i e c e 的持续动作 6 4 e l e v r o t t a b l e 的肚础槿嚷 6 5 r o b o t 的基础模，魁 6 6 p r e s s 的基础模型 6 7 p a m a s 四元模趔 6 8 异步抽象状念机的令j 0 状念和尚i ! f f 税界 6 9 m u l t i p l e r e a d o n e w r i t e 的旌础抽象状态移l ( a c t = r e a d ，w r i t e ) 6 1 0m a s t e r s l a v e a g r e e m e n t 的a g e n t f f , 3 毖础抽象状态机 6 1 1 c o n s e n s u s 的a g e n t f j 殛础抽象状念机 6 t 2 l o a d b a l a n c e 的a g e n t 的壤础抽象状态饥 6 1 3 e c h o 的a g e n t 的垡础抽缘状态机 7 1 定义在w s d l 顶郜f i q b p e l 7 2b p e l 抽象状态机的t 个层次， 7 3 b p e l 模掣的尚f ，：结构 7 4 a c t i v i t y a g e n t 分卉j 抽象状念机的控制结构 7 5 b p e l 执乱二语义的广，界向 7 2 7 3 7 4 7 6 8 2 钞钉轮们以甜酌卯 上海交通大学 学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究 工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人 或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集 体，均己在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：谢瑾奎 日期：2 0 0 6 年7 月1 0 日 上海交通大学 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定，同意学校保 留并向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借 阅。本人授权上海交通大学可以将本学位论文的全部或部分内容编入有关数据库 进行检索，可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。 保密口，在一年解密后适用本授权书。 本学位论文属于 不保密口。 ( 请在以上方框内打“4 ”) 学位论文作者签名：谢瑾奎指导教师签名：黄林鹏 日期：2 0 0 6 年7 月l o 日日期：2 0 0 6 年7 月l o 日 上海交通大学博士学位论文第一章绪论 1 1 引言 第一章绪论 抽象状态机( a b s t r a c ts t a t em a c h i n e s ，a s m ) 的基本思想可以追溯到上个世 纪8 0 年代 5 8 】。a s m 的发明者y u r ig u r e v i c h 从数学领域转到计算机领域发现这 样的现象：一个程序语言在不同的编译器下有着不同的编译。这就存在一个 问题：究竟一个程序语言的确切语义是什么? 这个问题从指称语义( d e n o t a t i o n s e m a n t i c s ) 和代数规约( a l g e b r a i cs p e c i f i c a t i o n s ) 的方法中并未得到很好的解决， 图灵机( t u r i n gm a c h i n e ) 可以模拟任何的算法( 根据强t u r i n gt h e s i s ) ，但是注意到 图灵机是通过字节模拟一个算法的，对于不同抽象程度的程序利用图灵机模拟 将是一个挑战。是否可以推广图灵机，使得任何抽象层次的算法都可以被忠实 的刻划? 这种思想似乎是难以实现的。 y u r ig u r e v i c h 进行研究的初衷是：( 1 ) 为c h u r c h - t u r i n g 论题引入资源边界 的限制：( 2 ) 采用动态结构( d y n a m i cs t r u c t u r e s ) 定义更为抽象的计算设备【5 8 】。 这时y u r ig u r e v i c h 从数学中得到了启迪。丰富的数学经验告诉他，任何静 态的数学实体，都可以表示为一阶结构，因而算法的每个状态为一阶结 构。计算( c o m p u t a t i o n ) 就是状态的进化( e v o l v i n g ) 。可以容易的用一个函数 来表示一个关系，使得一阶结构中可以只含有函数。而只有函数运算的 结构在泛代数( u n i v e r s a la l g e b r a s ) 中称为代数，因此这种模型最初被分别称 为动态结构( d y n a m i cs t r u c t u r e s ) ，动态代数( d y n a m i ca l g e b r a s ) ，以及进化代 数( e v o l v i n ga l g e b r a s ) 5 1 ，5 7 。最终，通过多年的研究，人们发现进化代数实 际上是d i j k s 仃a 的抽象机( a b s 仃a c tm a c h i n e ) 的基本概念和利用t a r s k i 的结构作为一 般的抽象状态( a b s t r a c ts t a t e s ) 的基本思想的完美结合，最终称为抽象状态机。 所以a s m = a b s t r a c ts t a t e + a b s t r a c tm a c h i n e 7 3 。在此期间，e g o nb 6 r g e r c a 识 到动态结构在实践中的潜力，用其解决了p r o l o g 设计中几年来悬而未决的困 难并定义t p r o l o g 的动态语义( d y n a m i cs e m a n t i c ) 标准f 6 ，2 2 ，7 5 1 。这时，人们了 解到a s m 适合于为变化的情况建模：从一个可靠的基准模型( g r o u n dm o d e l ) 开 始任意进行水平和垂直调整。a s m 已经成功应用于设计包括虚拟机、微处理 器体系结构、协议、嵌入式系统和大型软件需求等在内的众多领域【1 7 】。在微 处理器体系结构中，采用a s m 的例子包括控制处理单元z c p u ，r s i c 机d l x 的 参考结构【2 5 】，d e ca l p h a 处理器系列【4 9 】，t m s 3 2 0 0c 6 2 0 0 系y i j 2 9 1 。虚拟 上海交通大学博士学位论文第一章绪论 机则包括p v m 2 3 ，j v m 2 6 ，9 8 。协议设计中采用a s m 的有l a m p o r t 的互斥协 议【7 2 】，k e r m i t 的f t p 协议 7 1 1 ，处理器间的g r o u pm e m b e r s h i p 协议【6 2 】，u p n p 协议 5 3 1 ，以及k e r b e r o s 认证协议 1 6 ，1 7 】。借助a s m 定义的语言或标准 有p r o l o g ，c ，c + + ，j a v a ，v h d l ，s d l 等 2 2 ，5 2 ，7 7 ，9 2 ，9 4 ，9 9 。 目前，a s m 已经从一种思想发展成一种成熟的模型，一种语言，一种被 国际标准化组织承认的、在软件和硬件规约中广泛使用的工具 3 6 ，9 ，3 5 。 同时a s m 的工业用软件开发环境已经初露端倪，并且已经得到成功的运 用。值得一提的是，在m i c r o s o r 的大力支持和推动下，已经产生了a s ml a n - g u a g e ( b p a s m l ) ，并整合到了n e t 开发环境中 1 0 ，1 2 1 。 本文选择抽象状态机作为研究目标，从其数学基础出发，系统的构造基础 抽象状态机，复合抽象状态机，同步多a g e n t 抽象状态机和异步多a g e n t 抽象状 态机，从而为系统与软件提供一个有完善数学背景的设计平台与方法。针对当 前w 曲应用与电子商务应用的快速发展，基于抽象状态机得到一般通用的构造 模型和性质，利用抽象状态机的数学基础，许多问题和行为都可以得到精确的 描述。而利用抽象状态机对移动系统形式化，同样具有较完备的理论性质和描 述能力。 1 2 论文的结构 本论文的研究内容和章节安排如下： 第一章简述了抽象状态机的起源与理论背景，介绍了相关的研究成果与应 用，并提出了本文研究的目的与意义。 第二章给出抽象状态机关于语法和语义的详细数学定义。我们首先引入抽 象状态的概念，以及数理逻辑中的一些基本定义。然后我们介绍抽象状态机转 换规则的更新集语义，包括顺序执行和调用执行。最后，我们把抽象状态机扩 充为具有储备集的抽象状态机。从而在数学上阐明了，在并行的上下文环境中 相互独立地引入新元素是可以同时发生的。 第三章介绍了顺序抽象状态机论题( s e q u e n t i a la s mt h e s i s ) ，它最初是 由g u r e v i c h 于1 9 8 5 年向美国数学学会( a m e r i c a nm a t h e m a t i c a ls o c i e t y ) 提出。它最 初的的原始形式是：所有的可计算设备，都可以实时的由大致相同规模的适当 的动态结构( d y n a m i cs t r u c t u r e ) 来模拟。以上的动态结构就是现在所说的抽象状 态机。在这里，我们基于几个假定，定义顺序算法( s e q u e n t i a la l g o r i t h m ) ，并推 一2 一 上海交通大学博士学位论文第一章绪论 导以下命题：所有的顺序算法都可以被一个适当的顺序抽象状态机用同样的步 调( s t e pf o rs t e p ) 模拟。此外，对于用抽象状态机来描述算法的非确定性做了分 析，并说明了决定项的性质。 第四章把基础抽象状态机定义为单个a g e n t 的机器，划分不同类型的函数， 并处理潜在的非确定性与并行性。 第五章把抽象状态机扩展到它的复合，包括顺序合成，迭代合成等。定 义了用黑盒( b l a c k - b o x ) 视点看待子机器的增强抽象状态机( t u r b oa s m ) ，以及用 白盒( w h i t e - b o x ) 的视点来看待子机器的抽象状态进程( a b s t r a c ts t a t ep r o c e s s ) 。此 外，根据这两种复合各自的特点，给出若干例子。 第六章把前面的单a g e n t 抽象状态机扩展为支持模块化的多a g e n t 抽象状态 机，区分同步和异步两种模式，并给出相应的应用实例。 第七章为w 曲服务中的b u s i n e s sp r o c e s se x e c u t i o nl a n g u a g ef o rw e bs e r - v i c e s ( b p e l ) 定义了个分布式抽象状态机( d a s m ) 。b p e l 为异步通讯的w e b 服 务定义了一个基础架构，通过发出和接收信息，在一系列连续交互的w 曲服务 的上建立起业务过程( b u s i n e s sp r o c e s s ) 。整个模型的执行是由协作与反应行为来 刻画，其基础行为与结构化行为基于明确的数学结构，具备扩充复杂业务过程 的能力。 第八章研究网络中定义多方交互的事务协议( t r a n s a c t i o np r o t o c 0 1 ) 的可验证 性( v e r i f i a b i l i t y ) 。这些协议通常出现在电子商务环境中，并且可以形式化成关系 转换器( r e l a t i o n a lt r a n s d u c e r ) 。我们基于抽象状态机引入关系转换器，在此基础 上讨论电子商务应用中的验证问题。相对于其他的关系转换器，a s m 关系转换 器具备更强的计算能力。 第九章基于抽象状态机来刻威移动对象的语义，关注的移动性依赖于语义 规范单元的交互抽象，移动性通过通讯拓扑结构的动态变化来表示。相比较于 进程代数，基于抽象状态机的移动系统在软件工程方面易于实现和扩展。 第十章总结了本论文的研究工作，展望了未来的研究方向。 3 上海交通大学博士学位论文第二章抽象状态机的数学基础 第二章抽象状态机的数学基础 在本章中，我们给出抽象状态机关于语法和语义的详细数学定义。我们首 先引入抽象状态的概念，以及数理逻辑中的一些基本定义。然后我们介绍抽象 状态机转换规则的更新集语义，包括顺序执行和调用执行。最后，我们把抽象 状态机扩充为具有储备集的抽象状态机。从而在数学上阐明了，在并行的上下 文环境中相互独立地引入新元素是可以同时发生的。 从最初y u r ig u r e v i c h 弓i 入动态结构定义 5 8 ，5 9 开始，再到e g o nb s r g c r 利 用抽象状态机为p r o l o g 和j a v a 等程序语言定义语义 2 2 ，2 6 ，9 8 ，以及a n d r e a s b l a s s 对抽象状态机与纯数学之间进行的相关研究 1 9 ，2 0 ，抽象状态机的数学基 础在不断扩展。本章系统地概括了其数学背景，特别是对具有储备集的抽象状 态机作了更详细的性质推导和说明。 2 1 抽象状态和更新集 抽象状态机的状态是一个代数结构( a l g e b r a i cs t r u c t u r e ) 。代数结构可以看 作是抽象的内存( m e m o r y ) ，函数的参数就是内存的位置o o c a t i o n ) ，而函数的 值( v a l u e ) 就是其中的内容( c o n t e n t ) 。同样的，关系结构( r e l a t i o n a ls t r u c t u r e ) 有 时可以看作是数据库。 定义2 1 基调( s i g n a t u r e ) 。一个基调是函数名的有限集。每一个函数名有 一个自己的变元数量( a r i t y ) ，它是一个非负整数。无参函数( n u l l a r yf u n c t i o n ) 被 称之为常量( c o n s t a n o 。函数名有静态的( s t a t i c ) 和动态的( d y n a m i c ) 两类。不作 进一步说明，都假定每一个基调都包含u a e f ，t r u e ，f a l s e 这三个静态常量。 基调有时也被称之为符号集( v o c a b u l a r y ) 。我们后面会看到，动态无参函数 在从一个状态到另一个状态的转换中会有变化，因此它对应着程序中的变 量 3 l ，5 8 ，5 9 ，6 4 ，7 3 。 例如，布尔代数的基调酬包含两个静态常量0 和l ，一个一元函数名 “一”，以及两个二元函数名“+ ”和”。 定义2 2 状态( s t a t e ) 。在基调中，一个状态9 1 包括一个非空集x ，即疆的超 底集( s u p e r u n i v e r s e ) ，以及对中函数名的解释( i n t e r p r e t a t i o n ) 。如果，是中的 一个n 元( n a r y ) f q 数名，则它的解释产是一个从x ”到x 的函数：如果c 是中的 常量，则它的解释一，是x 中的一个元素。状态嘎的超底集x 用i 疆i 表示。状态 4 一 上海交通大学博士学位论文第二章抽象状态机的数学基础 的超底集也被称为状态的基础集( b a s es e t ) 。状态中的元素就是其超底集中的元 素 3 1 ，5 8 ，5 9 ，6 4 ，7 3 。 在疆中，n 元函数名，的定义域( d o m a i n ) 是一个n 元组( n l ，) 的集合， 其满足( d 1 ，a n ) i 疆h 且尸( n l ，a n ) u n d e f 疆。一个关系则是一个 取值总为t r u e ，f a l s e 或u n d e f 的函数。一个在n 元组( 1 ，) 的集合上的关 系兄，有r ( a 。，a n ) = t r u e 。在应用中，状态疆的超底集x 通常被划分为更 小的底集( u n i v e r s e ) ，其通过特征函数( 一元关系) 来建模。由关系尼莨示的底集 是诅中所有元素a 组成的集合，其满足r ( a ) = t r u e 。 例子2 1 。考虑基调f 的两个状态疆和臀。状态2 【的超底集是 o ，l 。函数 的解释如下，其中a ，b ：共j o 或l ： 0 q = 0( 零) 1 q = l ( 壹) 一疆a = 1 - a ( 逻辑补) n + 疆b = m a x ( a ，6 ) ( 逻辑或) a 鹱b = m i n ( a ，6 ) ( 逻辑与) 状态毋的超底集是非负整数n 的幂集。函数的解释如下，其中n ，b 为n 的子 集： 0 蕾= 0 ( 空集) 1 = n ( 全集) 一留a = n a( 一个集合，其元素礼n ，且满足n 茌力 a + b = n ub ( 一个集合，其元素1 7 , n ，且满足7 1 a s 戈n 6 ) a $ 毋6 = a n6( 一个集合，其元素几n ，且满足n n 和n 6 ) 状态2 l 和毋都可以称作为布尔代数。 在动态的情形，可以很方便的把抽象状态看作是把位置映射到值的内存。 定义2 3 位置( l o c a t i o n ) 。疆的一个位置是一个偶对( ，( a l ，) ) ，其 中，是n 元函数名，a 1 ，a n 是i 嘎l 中的元素。值，盈( 0 1 ，a n ) 被称作疆中位置 的内容。位置的元素( e l e m e n t ) 就是集合 o ，o 。) 的元素。对于吼中位置f 的 内容，我们记作g ( 0 1 3 l ，5 8 ，5 9 ，6 4 , 7 3 。 定义2 4 更新与更新集( u p d a t ea n du p d a t es e t ) 。疆的一个更新就是一个偶 对( 2 ，移) ，其中f 是q 的位置，而口是1 2 【l 中的元素。如果u 是在2 【中f 的内容，则称 一5 一 上海交通大学博士学位论文 第二章抽象状态机的数学基础 此更新是平凡的( t r i v i a l ) 。更新集就是一个更新的集合 3 l ，5 8 ，5 9 ，6 4 ，7 3 。 更新的含义就是，在2 【中位置f 的内容被改变为值口。如果两个更新引用了同 一个位置，却又相互各异，则更新冲突( c l a s h ) 。 定义2 5 相容更新集( c o n s i s t e n tu p d a t es e o 。如果一个更新集u 不包含冲突 更新，则称之为相容的，即是，对任意的位置f 和所有的元素u ，t ，若有( z ，t ，) u 和( f ，牡7 ) u ，贝0 t ，= w 3 l ，5 8 ，5 9 ，6 4 ，7 3 。 如果一个更新集u 是相容的，则它可以在给定的状态中启动。得到的结果 是一个新的状态，其中动态函数名的解释根据u 做相应的改变，而静态函数名 的解释如同以前的状态。 定义2 6 更新的启动( f i r i n go f u p d a t e s ) 。在状态囊中启动一个相容更新集得 到的结果，是一个新的状态2 【+ u ，它和疆有着相同的超底集，并且对2 【中的所 有位置f 有【3 l ，5 8 ，5 9 ，6 4 ，7 3 】： c 巍堋，2 ，黧篡毓班u 状态射u 被称作疆对应于u 的后续( s e q u e l ) 。 给定两个有相同超底集和基调的状态疆与缈，总存在一个唯一的非平凡更 新，使得在状态组中启动得到状态孵。更新集被称作毋与疆的差玛2 【。 定义2 7 差( d i f f e r e n c e ) 。令2 【和孵是两个有着相同超底集的状态【3 l ，5 8 ，5 9 ， 6 4 ，7 3 。则孵一2 【= ( f ，孵( f ) ) i 毋( 2 ) 疆( z ) 。 两个状态的差钙一疆总是相容更新集。因此它在状态吼中启动后，结果是状 态毋。 引理2 1 。暖+ ( 毋一2 t ) = 易。 抽象状态的超底集的内在结构并不是很重要，抽象状态的元素的内在表示 是被隐藏的。这种信息隐藏的原则是通过同构( i s o m o r p h i s m ) 来表达的。如果两 个抽象状态的超底集可以相互一一映射，而且函数的解释在对应的元素取得一 致，这两个状态视为同一。 一个定义域为1 2 【l 的函数q ，其巍的位置和更新集如下： 如果f = ( ，( 0 1 ，o 。) ) ，则d ( f ) =