没有合适的资源?快使用搜索试试~ 我知道了~
297URL:http://www.elsevier.nl/locate/entcs/volume 70. html14页s精化排序及其相关模拟规则Christie Bolton,Jim Davies克里斯蒂·博尔顿,吉姆·戴维斯1,2牛津大学计算实验室WolfsonBuilding,Parks Road Oxford OX13QD,England摘要在本文中,我们将基于状态的规范语言(如Z和Object-Z)的精化排序及其相关的模拟规则与基于事件的规范语言(如CSP)的精化排序进行了比较。我们用一个简单的反例证明,使用Z的标准模拟规则建立的数据细化并不意味着CSP中的故障细化。这与公认的结果相矛盾。在探讨了用于建立数据精化的仿真规则与用于建立动作系统和状态转换系统的精化的仿真规则之间的区别之后,我们提出了一组新的数据类型仿真规则,其中精化等价于CSP中的故障这些替代规则对于稳定失效的细化排序都是合理的和联合完备的。此外,我们提出了CSP的另一种精化排序,其中精化等价于Z中的数据精化1介绍在大型复杂系统的开发过程中,通常需要构建一系列模型,每个模型解决前一个模型中的模糊性或不确定性在这样的方法论中,我们可能希望正式证明每个模型都是由下一个模型来细化的我们的直觉告诉我们,如果一个模型满足第一个模型所施加的所有属性和约束,那么第二个模型就被另一个模型所细化正如我们将要说明的,精化的精确定义取决于我们选择的形式主义。在本文中,我们重点讨论了用基于状态的规范语言Z [22]和Object-Z [10]表示的抽象数据类型的精化,1电邮地址: christie@comlab.ox.ac.uk2电子邮件地址:jdavies@comlab.ox.ac.uk2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。298用基于事件的规范语言CSP表示的过程的细化Z和Object-Z中的细化通常使用模拟规则集[14],尽管它可以通过考虑Z中的关系语义或考虑Object-Z中的历史语义我们揭示并讨论了CSP的稳定故障模型[18]中数据细化[8]和细化之间的差异,我们表明,虽然两个模型都给出了有关可能的相互作用序列的信息CSP中的稳定故障和故障-分歧[18]模型给出了关于事件组合可用性的信息,而Z的关系语义仅给出了关于单个操作的拒绝信息因此,数据细化并不意味着故障细化。在第2节中,我们提出了一个简单的反例,证明了导出的模拟规则与Z中表示的数据类型的关系语义[5]的阻塞解释精确对应,对于CSP的稳定故障模型[18]来说从这一点可以立即得出,数据细化并不意味着稳定的故障细化,这与公认的结果相矛盾[21,6,5,11,9]。在探索了这两种细化排序之间的区别如果我们希望比较基于状态和基于事件的模型,我们有两个选择:要么我们必须为CSP确定一个语义模型,它具有与数据类型的关系语义相同的信息内容,要么我们必须为CSP确定一组对应于稳定故障模型的模拟规则我们在第5节中采用了前一种方法,并且在第3节中探索了用于建立数据精化的模拟规则与用于建立动作系统精化[1]和状态转换系统精化[17,16]的模拟规则之间的本文的主要贡献如下:• 我们证明了Z3中的数据细化并不意味着CSP4中的稳定故障细化;• 我们提出了一组Object-Z5中表示的数据类型的模拟规则,这些规则对于CSP的稳定故障细化排序是合理的和联合完备的• 我们描述了CSP的另一种语义模型,它的信息内容正是数据类型的关系语义;[3]如[4]所示,该结果扩展到Object-Z。4.在本文中,我们假设Z,Object-Z和CSP的知识。 不熟悉这些符号的读者应该分别参见[22,23,9]和[20]和[13,18]5我们选择Object-Z而不是Z作为范例,因为对于无发散系统,这些模拟规则精确地对应于Object-Z的已建立历史模型。299s:0.. 4美国s = 1 μ m sJ= 0美国s∈ {2, 3}<$sJ = 0美国s∈ {2, 4}<$sJ = 00000001111112222223333334一44B44C4Fig. 1. 描述数据类型P和Q上的操作A、B和C的关系。• 最后,我们用一个表格来区分那些提供关于事件或操作组合的可用性的信息的细化排序和模拟规则集,以及那些仅在逐个操作的基础上提供拒绝信息的细化排序和模拟规则集。2数据细化并不意味着故障细化我们用一个简单的例子证明了数据精化不等价于稳定失效精化。让数据类型P和Q定义如下:两种数据类型具有相同的内部状态空间State,包含从0到4的整数;给定包含单个元素e的环境Env,两种数据类型具有相同的终结操作,将整个状态空间映射到Env上;状态并且两种数据类型共享如图1所示的操作A、B和C操作A将状态1映射到状态0;操作B将状态2和3映射到状态0;操作C将状态2和4映射到状态0。更正式地说,A BC这两种数据类型之间的区别在于它们的初始化关系的范围:数据类型P最初可以处于状态1或2,而数据类型Q最初可以处于状态1、3或4。最终状态;环境J3000123401234PInit环境;状态JsJ∈ {1, 2}QInit环境;状态JsJ∈ {1, 3, 4}Retr图二. 从状态Q到状态P的反向关系Retr。在下面的引理2.1中,我们通过证明P在阻塞语义6的上下文中模拟Q来证明数据类型P由数据类型Q限定;更具体地,我们识别检索关系Retr,使得对应于阻塞语义的向后五月一号,全部待命。 由于模拟规则的合理性,数据修正自动进行[5]。引理2.1数据类型P由Q定义,其中P和Q如上定义。证据 为了清楚起见,我们在语法上区分数据类型的共享组件;我们定义StateP和State Q等于State; AP和AQ等于A,等等。然后让从Q的状态空间到P的状态空间的检索关系Retr如图2所示,并在下面正式定义:Retrp:状态Pq:状态Q(q∈ {0,1,2}) p = q) (q∈ {3,4}) {1, 2})我们只需要证明以下谓词为真。(i) 状态PJ;状态QJ·QInit(ii) (a)州Q·(州P·RetrpreAP)preAQ(b) 状态Q·(状态P·返回前BP)返回前BQ(c) 状态Q·(状态P·返回前CP)返回前CQ(iii) (a)国家PJ;国家Q;国家QJ|A QRetr J·(State P·Retr A P)[6]我们在分块框架内工作,以便于第3节中的比较。301∀·⇒(b) 状态PJ;状态Q;状态QJ|B QRetr J·(State P·Retr B P)(c) 状态PJ;状态Q;状态QJ|C QRetr J·(State P·Retr C P)(iv) 状态Q;环境|最终Q·状态P|Retr·Final P第一条规则简化为pJ,qJ:状态·((qJ= 1<$pJ = 1) ((qJ= 3<$qJ = 4)<$(pJ= 1<$pJ = 2)(pJ= 1这就等于真。在操作A的情况下,第二规则的内部子句,或者更精确地说,谓词StateP RetrpreAP,等价于州名:State((q= 0<$p = 0) ∨ (q= 1,p = 1) ∨ (q = 2,p = 2) ∨(q= 3<$(p= 1<$p = 2))<$(q= 4< $(p= 1< $p= 2)⇒p= 1这简化为(q/= 0)<$(q/= 2)<$(q/= 3)<$(q/= 4),因此q= 1.在操作A的情况下,第二规则因此等同于q:状态· q = 1 q= 1这当然是真的类似地,在操作B的情况下,第二规则的内部子句等价于州名:State((q= 0<$p = 0) ∨ (q= 1,p = 1) ∨ (q = 2,p = 2) ∨(q= 3<$(p= 1<$p = 2))<$(q= 4< $(p= 1< $p= 2)⇒(p=2p= 3)这简化为(q/= 0)<$(q/= 1)<$(q/= 3)<$(q/= 4),因此q= 2.在操作B的情况下,第二规则因此等同于q:状态·q= 2<$((q= 2)<$(q= 3))这也是事实此外,通过对称性,可以立即得出第二个规则对于操作C也必须为真。302→→→我们已经证明了规则1和规则2对数据类型上的每个操作都接下来,我们来看第三条规则。在操作A的情况下,该规则简化为:p J,q,q J:状态|q = 1 <$q J= 0 <$p J= 0·p:状态·p= 1这就等于真。在操作B的情况下,第三条规则简化为p J,q,q J:状态|(q = 2 <$q = 3)<$q J= 0 <$p J= 0 ·p:状态·p= 2∨p= 3pJ= 0 false这也等同于真。我们再一次诉诸对称性来立即建立第三规则对于操作c也必须为真。最后,观察到第四个模拟规则是平凡真实的,我们得出结论,所有的向后模拟规则成立,因此P模拟Q。因此,通过模拟规则的合理性[5],我们推断出数据类型P由数据类型Q定义。将阻塞上下文中的数据类型的自然转换应用于CSP进程(更多细节请参见[24]),我们得到进程b(P),该进程对应于数据类型P。过程b(P)= letP(s)=(s== 0)停止(s == 1)&op. a P(0)(s == 2&)b→P(0)op. c→P(0))(s == 3)&op. b P(0)(s == 4)&op. c P(0)最后。e→停止内e:{e} · Hs:{1,2} ·初始化。e→P(s)303稍微重新排列和一些明显的重命名,这个过程可以等效地写为下面的过程ProcP:ProcP= i→((a→f→停止H(b→f→停止)(c→f→停止))f→停止)应用类似的技术,我们可以得到对应于数据类型Q的进程ProcQ。ProcQ= i→((a→f→停止Hb→f →停止Hc→f→停止)f→停止)观察结果1在稳定故障模型中,对应于P的过程未被对应于Q的过程细化,其中数据类型P和Q如上所定义。证据我们看到,在事件i之后,进程ProcP可以拒绝任何不包含f且不包含a和b或a和c的事件集,而在事件i之后,进程ProcQ可以拒绝任何不包含f且最多包含a、b和c中的两个的事件集。特别是,ProcQ可以拒绝集合{a,b}和{a,c},而ProcP不能:跟踪拒绝对(i,{a,b})和(i,{a,c})都存在于ProcQ的失败中,而不是ProcP的失败中。我们已经证明了对应于Q的过程的失败集不是对应于P的过程的失败集的子集。因此,对应于P的过程在稳定失效模型中没有被对应于Q的过程所细化。定理2.2数据细化并不意味着稳定失效细化证据 我们已经确定了两种数据类型P和Q。在引理2.1中,我们证明了P被Q所精化,在观察1中,我们证明了在稳定失效语义模型中,对应于P的过程没有被对应于Q的过程所精化。由此可见,数据精化并不意味着稳定故障精化:数据精化和稳定故障精化是不等价的。我们证明了这一结果的上下文中的阻塞语义。在非阻塞语义的上下文中,可以显示类似的证明来建立相同的3043Josephs、He、Woocock和Morgan的模拟规则用Z表示的抽象数据类型的模拟规则可以根据定义数据类型的组件(状态空间、初始化、终结和命名操作)的模式给出,也可以根据底层关系给出。 此外,可以导出模拟规则以对应于阻塞或非阻塞语义模型(参见[6])。无论我们选择什么样的上下文都将呈现两组模拟规则,向前和向后(有时称为向下和向上)如果一些非确定性已经解决,那么我们希望建立一个正向模拟,而如果两种数据类型中更抽象的一些非确定性已经推迟,那么我们希望建立一个反向模拟。模拟规则的非阻塞和阻塞版本分别在[23]和[5]中被证明是合理的和联合完整的在本节中,我们将在Z中建立数据精化的模拟规则的信息内容与Josephs[15],He [12]以及Woocock和Morgan [25]的模拟规则进行Woodcock和Morgan约瑟夫规则是为了建立状态转换系统的细化。这些模型都采用了分块的方法,因此我们在第2节中选择了上下文约瑟夫斯、他、伍科克和摩根都证明了,他们的模拟规则对于罗斯科的失败-分歧细化排序是合理的和联合完备的;由此可见,对于无分歧系统,他们对于罗斯科的稳定失败细化排序是合理的和联合完备的除此之外,这些规则与Z中对应于数据细化的规则之间的区别在于,约瑟夫、He、Woocock和Morgan的规则都捕获了操作组合的可用性,而从Z的关系语义中导出的模拟规则只提供了关于单个操作的可用性的信息。这种差异只发生在一个规则中,即关于操作可用性的向后模拟规则。约瑟夫斯、贺、伍科克和摩根的相关规则确保,如果更具体的模型中的一个状态位于任何给定的一组动作或转换的前提条件(域的联合)之外,那么在更抽象的模型中一定有一个相应的状态数据类型的相应规则更弱:它要求如果更具体的模型中的状态位于单个操作的域之外,那么在更抽象的模型中必须有一个相应的状态也位于该单个操作的域之外再次考虑第2节中介绍的数据类型P和Q状态7.我们假定知道动作系统形式主义和状态转移系统。不熟悉这些符号的读者应该看[7]。3053 在数据类型Q上的操作位于操作A和C的域之外。我们识别出数据类型P上的对应状态2位于操作A的域之外,以及P上的对应状态1位于C的域之外;因此第三个向后模拟规则成立。然而,如果我们被要求识别位于这两个操作域之外的单个对应状态,我们就会失败:不存在这样的对应状态。如果我们把P和Q转换成适当的形式,约瑟夫斯、他、伍德考克和摩根的模拟规则就不成立了。4Object-Z历史地震模型对应的模拟规则在本节中,我们将介绍用于验证一种数据类型在稳定故障模型中被另一种数据类型所定义的规则 我们在Object-Z [10]的上下文中这样做,因为传统上已经给出了与Roscoe的失败-分歧语义模型[19]等效的历史语义。这些规则是在[2,4]中引入的。如果A和C是具有相同的操作名称集合X的Object-Z类,则给定与两个类的状态空间相关的检索关系Retr,对应于历史语义模型的前向/向下和后向/向上模拟规则分别如下。C. 泰特·C。我不知道。泰特·A。INITRETR)(FOZ−h1)P:X; A. STATE; C. STATE·(FOZ−h2)Retr(pre A. OPprec. OP)P:X; A. STATE; C. STATE; C. STATEJ·(FOZ−h3)Retr C. OPA. STATE J·Retr j A. OPA. STATE; C. 泰特·C。我不知道你是谁。INIT(BOZ−h1)C. S·泰特·库尼亚。STATE·(BOZ−h2)P:X·Retr(pre A. 奥普雷角OP)P:X; A. STATE J; C. STATE; C. STATE J·(B OZ−h3)Retrj C. OP A. STATE·Retr A.A.OP这些规则的可靠性和连接完备性直接来自Josephs规则的相应结果他们从站起来,306标准[9] Object-Z的模拟规则,如附录B中所述,仅在规则B2中。不同之处在于量化的范围:在规则B OZ−r2中,我们有所有抽象状态的存在量化上的所有运算的泛量化(XO P:X·X A)。S TATE·.. . ),而在规则B OZ−h2中,我们有一个更强的谓词,即所有抽象状态的存在性量化超过所有运算的泛量化。S·TATE·BERGO P:X·.. . ).5单例故障语义模型确定了数据细化和稳定故障细化之间的差异,并确定了Object-Z的模拟规则,这些规则对于Roscoe的故障分歧细化排序来说既合理又联合完整,现在我们提出了CSP的单例故障语义模型的简化版本-一个定义为它的信息内容正好是数据类型的关系语义的这个模型被引入,并被证明等价于[3,2]中数据类型的关系语义。单例故障语义模型反映了数据类型的关系语义的信息内容,在单个基础上记录事件的可用性。语义函数本质上是稳定故障语义函数的投影,只记录拒绝集的基数至多为1的那些跟踪拒绝给定集合Refusal1包含基数为1的事件的集合s,并且集合Trace包含所有可能的事件序列,语义函数S定义如下:S[[P]]=F[[P]](Trace×Refsal1)。其中P是一个基本进程,即仅使用操作符Stop、→、H和XY构造的进程。与CSP中的其他模型一样,细化是反向遏制。给定任何基本过程P和Q,P±SQ惠S[[Q]]<$S [[P]]。此外,所有适用于稳定失效模型的定律,当应用于基本过程时,只能用基本操作符来表示,这适用于单例[8]例外是隐藏运算符,为了简单起见,我们将不关心它。我们在这张纸上。 有兴趣的读者可以看[3,2]。3076结论本文中包含的新思想都源于数据细化不等同于稳定故障细化的观察我们给出了一个简单的例子,揭示了模型之间的差异:数据类型的关系语义记录了操作的可用性,而稳定故障语义模型记录了事件组合的可用性。如果我们希望比较基于状态的模型和基于事件的模型,我们要么必须采用一组模拟规则,这些规则对于稳定故障或故障-发散模型都是合理的,并且是共同完整的(我们在第4节中采用了这种方法,为Object-Z提供了这样一组规则),要么我们必须采用一个CSP的语义模型,它具有与数据类型的关系语义相同的信息内容(我们在第5节中采用了这种方法,介绍了单例故障语义模型)。我们用一个表格来总结本文,该表格提供了我们在本文中考虑的细化排序和模拟规则的信息内容之间的比较我们将它们分为两类:一类是在单个基础上提供拒绝信息,另一类是为事件或操作的组合提供拒绝信息。精化模型模拟规则数据细化,例如[8]个人拒绝信息Z中的数据细化例如[23,5,9]CSP的单例失效模型,例如[3,2]Z eg [23,5,9]Object-Z例如[21,9]组合拒绝信息CSP的稳定故障模型,例如[18]Object-Z的历史模型,例如[19]状态转移系统,例如[15,12]行动系统例如[25]Object-Z的并发规则,例如[4]308AZ的模拟规则在本节中,我们在阻塞语义模型9的上下文中呈现Z的模拟规则。给定具有状态空间AState和CState的数据类型A和C,分别具有初始化和最终化AInit和AFinal,以及CInit和CFinal,并且具有对应的操作AOp和COp,并且给定检索关系Retr,正向模拟规则为:CState J·CInit |AInit·Retr(F Z1)国家|前AOp·DCState |Retr·pre COp(F Z2)联系我们|Retr·(FZ3)国家J|缔约方会议|AOp·Retr J呼吸道状态;环境·视网膜静脉曲张(FZ 4)类似地,阻塞向后模拟规则的模式版本如下。AStateJ;CStateJ·CInitCSTATE·(CSTATE·RetrCSTATE·Retr CSTATE·Retr CSTATE·RetrCSTATE·(CSTATE·RetrCSTATE·RetrCSTATE)CASTATE J; CSTATE; CSTATE J|COp返回值J·(BZ3)(COp状态·返回值AOp)环境状态|公司简介|Retr·AFinal(B Z4)BObject-Z的模拟规则在本节中,我们将介绍Object-Z的模拟规则这些规则对于Object-Z的关系语义来说是合理的和完整的:参见[9]。 如果A和C是具有相同操作名称集合X的Object-Z类,则给定将两个类的状态空间(向前/向下和向后/向上)关联的检索关系Retr,9为了更详细地描述该模型和模拟规则的推导见[5,2]。309Object-Z的模拟规则,如[21,9]所示,分别如下:C. 泰特·C。我不知道。泰特·A。(FOZ−r1)P:X; A. STATE; C. STATE·(FOZ−r2)Retr(pre A. OPprec. OP)P:X; A. STATE; C. STATE; C. STATEJ·(FOZ−r3)Retr C. OPA. STATE J·Retr j A. OPA. STATE; C. 泰特·C。我不知道你是谁。INIT(BOZ−r1)P:X; C. STATE·(BOZ−r2)A. STATE·Retr(前A。奥普雷角OP)P:X; A. STATE J; C. STATE; C. STATE J·(B OZ−r3)Retrj C. OP A. STATE·Retr A.A.OP引用[1] R. J.R. 巴克和R. 库尔基-苏尼奥 过程网络的分散化集中控制。第二届ACM SIGACT-SIGOPS分布式计算原理研讨会,1983年。[2] C.博尔顿基于状态和基于事件的模型的改进。 博士论文,牛津大学,2002年1月。提交检查。[3] C.博尔顿和J.戴维斯。通信顺序进程的单例故障语义,2001年。提交到计算的形式方面[4] C.博尔顿和J.戴维斯。在Object-Z和CSP中进行细化。In M. Butler,K. Sere和L. Petre,编辑,集成形式方法会议录(IFMSpringer Verlag,2002年。出现。[5] C. Bolton,J. Davies,and J. Woodcock.关于数据类型和过程的细化和模拟。在K。Araki,A. Galloway,andK. 田口,编辑,集成形式化方法(IFMSpringer,1999年。[6] H.鲍曼和J.德里克。基于状态和行为规范之间的结合点。以. Fantechi P.Ciancarini和R. Gorrieri,编辑,开放式基于对象的分布式系统的形式化方法(FMOODSKluwer,1999年。[7] M. J·巴特勒一个CSP方法的行动系统。牛津大学博士论文,1992年。310[8] W.-- P. de Roever和K.恩格尔哈特数据精化:面向模型的证明方法及其比较。剑桥理论计算机科学,1998年。[9] J. Derrick和E.煮一下 Z和Object-Z中的细化。 Springer,2001年。[10] R. Duke,G. Rose和G.史密斯Object-Z:一种用于描述标准的规范语言。计算机标准与接口,1995年,第17期[11] C.费舍尔过程与数据的结合与实现:从CSP- OZ到Java。奥尔登堡大学博士论文,2000年。[12] J. 他外过程细化。 在j. McDermid,编辑,精炼的理论与实践。巴特沃斯,1989年。[13] C. A. R. 霍尔通信顺序进程。普伦蒂斯·霍尔1985年[14] C. A. R. Hoare,J. He和J. W. 桑德斯数据细化中的预处理信息处理快报,1987年。[15] M. B. 约瑟夫一种基于状态的进程通信方法。分布式计算,3:9[16] L. 兰波特一 简单 方法 到 指定 并发系统ACM通讯,32(1),1989年。[17] A.普努埃利反应系统的规范和发展。在H.- J. Kugler,editor,Proceedings of(),IFIP,North Holland,1986.信息处理.[18] A. W.罗斯科并发的理论与实践。 Prentice Hall计算机科学系列,1998年。[19] G.史密斯Object-Z类的完全抽象语义。 计算的形式方面,1995年7月。[20] G.史密斯Object-Z语言。Kluwer Academic Publishers,2000.[21] G. Smith和J. 德里克 改进和验证 Object-Z 和CSP 中指定 的并发In M.Hinchey和Shaoying Liu,编辑,第一届IEEE形式工程方法国际会议论文集(ICFEMIEEE计算机学会,1997年。[22] J. M. 斯皮维Z符号:参考手册。普伦蒂斯·霍尔1992年[23] J. C. P. Woodcock和J. 戴维斯使用Z:规范,证明和细化。Prentice HallInternational Series in Computer Science,1996年。[24] J. C. P. Woodcock,J. Davies和C. 博尔顿抽象数据类型和过程。在J. Davies,A. W. Roscoe和J.C. P. Woodcock,编辑,计算机科学的千禧年前景:纪念Tony Hoare爵士的研讨会论文集。帕尔格雷夫,2000年。[25] J. C. P. Woodcock和C.C. Morgan. 基于状态的并发系统的改进In D.比约纳角A. R. Hoare和H.Langmaack,编辑,VDM和Z:软件开发中的形式化方法。Springer,1990年。
下载后可阅读完整内容,剩余1页未读,立即下载
![docx](https://img-home.csdnimg.cn/images/20210720083331.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 京瓷TASKalfa系列维修手册:安全与操作指南
- 小波变换在视频压缩中的应用
- Microsoft OfficeXP详解:WordXP、ExcelXP和PowerPointXP
- 雀巢在线媒介投放策划:门户网站与广告效果分析
- 用友NC-V56供应链功能升级详解(84页)
- 计算机病毒与防御策略探索
- 企业网NAT技术实践:2022年部署互联网出口策略
- 软件测试面试必备:概念、原则与常见问题解析
- 2022年Windows IIS服务器内外网配置详解与Serv-U FTP服务器安装
- 中国联通:企业级ICT转型与创新实践
- C#图形图像编程深入解析:GDI+与多媒体应用
- Xilinx AXI Interconnect v2.1用户指南
- DIY编程电缆全攻略:接口类型与自制指南
- 电脑维护与硬盘数据恢复指南
- 计算机网络技术专业剖析:人才培养与改革
- 量化多因子指数增强策略:微观视角的实证分析
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)