概率持续时间演算中 QoS契约推理，基于组件的软件开发中的拓展理论计算机科学电子笔记

理论计算机科学电子笔记238（2010）41-62www.elsevier.com/locate/entcsQoS契约的推理在概率持续时间演算中迪米塔山口Guelev Guelev2，3保加利亚科学索菲亚邓文雄1，4联合国大学Macau，P.R. 中国摘要契约的概念被引入到基于组件的软件开发中，以促进组件的语义正确组合。我们扩展了这个概念的形式，在设计上捕捉执行时间的概率要求。我们展示了如何推理这样的要求，可以在一个无限间隔为基础的系统的概率持续时间演算。关键词：组件，合同，服务质量，持续时间计算介绍将现成组件和专用组件相结合已成为实现重用、模块化、生产率和可靠性的既定方法。合同促进组件的正确使用。合同是一个需求的集合，这些需求是根据组件接口编写的。组件的实现应满足合同要求，前提是从其他组件导入的项目也满足合同中出现的要求。在[1]中确定了四个级别的合同这些是语法1本工作得到国家自然科学基金项目（60603037）的2本文的工作是在D.Guelev于2007年8月至9月访问联合国大学/软件技术研究所。3电子邮件：gelevdp@math.bas.bg4电子邮件：dvh@iist.unu.edu1571-0661 © 2010由Elsevier B. V.出版在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.06.00442D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）41联系我们级别、行为级别、同步级别和服务质量级别。服务质量（QoS）是非功能性需求的集合术语，作为最坏情况和平均执行时间，以及资源消耗， 如存储器、功率、带宽等。组件模型是围绕概念的适当形式化构建的接口、契约、组件可组合性、组合等。基于[12]中的设计概念的组件契约理论已在[13，14]中提出，并已被称为rCOS模型。由于设计捕获输入输出关系，因此该模型主要是关于组件的功能需求，而忽略了[1]中的QoS级别。在我们之前的工作中，我们扩展了rCOS模型，以捕获对时间和资源的要求[3，11]。我们已经考虑了硬性要求，例如，错过最后期限被认为是致命的。 我们使用持续时间演算（DC）作为我们的符号。QoS主要涉及软要求，其中，例如，稍微错过最后期限是可以容忍的，但不要太频繁。对QoS的处理要求涉及对概率的推理在本文中，我们扩展了设计以捕获执行时间的概率需求，并开发了一种技术来使用基于无限间隔的概率DC（PDC）系统来推理实时嵌入式系统的QoS，该系统是在[10]中提出的，作为具有无限间隔的概率间隔时态逻辑（PITL）的相应系统的扩展。无限区间PDC包含了[17，5，9]中的PDC系统，并且有一个相对完整的证明系统来支持形式推理。（非概率）DC对于实时系统推理的适用性已经被许多案例研究所证实[25，4，21，2，16]。由于DC是基于时间间隔的，因此在DC中对整个方法执行的行为（包括它们的执行时间）进行推理是相对简单的。通过使用DC的概率扩展，我们在推理QoS要求时也能够享受这一优势。1预赛在PITL和PDC中，我们只考虑实数的扩充集R = R作 为 时 间 的流。为了便于描述重复行为，我们在非概率公式中引入了一个最小固定点算子，该算子在[18]中引入并在[8]中进行了研究。 无限区间的ITL [23，20，21，22]是PITL和PDC的基础非概率逻辑。它通过二元模态（. ;。），称为chop。5非逻辑符号分为刚性和非柔性，这取决于它们的含义是否要求在所有参考区间都相同。个体变量是刚性的。词汇表L的解释是L上的函数I，它根据符号的类型和类别将符号从L映射到R上的成员、函数和谓词。I（s）在以下情况下，将从IUI中获取一个输入值作为附加值[5]许多作者的写作都是用“”代替（;）。D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）4143∈|∞∫∈ ∈∪⊥ ⇒∃不 ∧ ⇒ ⇔∀联系我们|∈联系我们I σ<$S∞σ ∈[S|我的天X1，.，Xn∫是不灵活的。我们用区间的集合Ifinn={[τ1，τ2]：τ1，τ2∈R，τ1≤τ2}，Iinf={[τ，∞]：τ∈R}且I=IfinnIinf。G i venσ1If inandσ2Ifin suchthatmaxσ1=min σ2，σ1;σ2代表σ1σ2。在解释I中，项t的值Iσ（t）在i intervalsσI中以通常的方式定义，其中参考区间是可变符号的附加参数。满意度=根据解释和参考区间定义灵活关系符号也是将引用区间作为参数的解释谓词。和的分句是常用的分句。用于（的子句。;。）是I，σ|=（;）i I，σ1|=和I，σ2|对于某些σ1∈Ifinn和σ2∈I所以σ1; σ2= σ。0、、+和=在国际交易日志词汇表中是必不可少的，通常有通常的解释。 强制可变常数l总是计算参考区间的长度。 用fix表示+和=， 、、、和都是以通常的方式使用的。国际交易日志专用缩略语包括（注1;. ;n−1;n）（注1;. （n− 1; n）.. . ）Q（T;; T）（T;），Q <$Q <$。Q和Q结合得更紧密，并且（。;。）的连接比布尔连接词的连接更不紧密。 一个完整的证明系统，国际交易日志与无限的时间间隔在[22]中提出了一个合适的持续时间的抽象域具有无限间隔的DC的词汇表另外包括状态变量P、Q、. . 状态表达式S是状态变量与写为0和1的逻辑常数的布尔组合，并且反过来作为持续时间项S的参数出现，持续时间项S是DC项语法中的DC特定构造DC中的公式与ITL中的相同。状态变量的值为R0， 1类型的分段常数函数状态表达式S在时间τ处的值Iτ（S）以通常的方式使用所涉及的状态变量P的I（P）（τ）来定义。持续时间项的值由等式Iσ（IS) 为mmaxσIτ（S）dτ最小σ（）可以我的INF 在DC中，表达式“i”= 0= 0和“l”可以被看作是1的缩写。相对于实时ITL（无限间隔）中的有效性，DC（无限间隔）的公理和规则是完整的，已在[15]中给出（分别为[10]）最小固定点运算符如果n =1，...，n没有命题变量X1，.的负出现，n和i1、......、n，则μ i X1. X n.1，.，n是良构的，并且I，σ= μ i X1. X n.1，.，ni<$σA i，其中A1，.，A n是满足等式的最小子集Ai={σ∈I：Iλ σ. σ∈A1，.，λ σ。σ∈An， σ|i=1， . ，n.44D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）41∃∈∈∈∈∈∈× ×→•∈ττ迭代，也被称为Kleene星，可以通过以下等式使用μ来定义：X.l= 0. I，σ|可以通过以下条件独立定义：min σ= max σ或σ=σ1;. ; σ n和I，σ i|i = 0，i= 1，.，n，对于某个n<ω，σ1， . ，σn∈ψI.在[18，8，7]中提出了DC中μ和μ的公理和规则高阶量化器我们使用通常意义上的可伸缩常数和状态变量来描述局部变量的语义。在[24，8，7]中已经研究了某些公理和规则对于这种用法的演绎能力.ProbabilityITL和DC with infinitite intervals（PITL）扩展了ITL项由形式p（k）的概率项表示，其中k是一个公式。式语法与ITL相同，包括μ和更高阶的量化器 PITL模型基于对给定词汇L的解释的集合。每个解释都是为了描述建模系统的可能行为。考虑一个非空集W，一个W上的函数I到L的ITL解释的集合中，一个W型函数PR2 W[0， 1]。设Iw和Pw表示I（w），λτ，X.P（w，τ，X），对于所有wW. I w和P w，wW旨在表示L的PITL模型中每个τ ∈ R的行为集和相关概率分布。定义1.1设τ ∈ R。 那我就Iw（s）=Iv（s）对于所有刚性符号sL，可能除了个别变量;I w（s）（σ，d1，.，d#s）= I v（s）（σ，d1，.，d#s）对于所有可伸缩s ∈ L，所有d1，.，d#s∈R和所有的σ∈τI使得maxσ≤τ;Pw（τ J，X）= Pv（τ J，X）对所有X <$W和所有τ J≤ τ。显然，对于所有的τ ∈ R，<$τ是W上的等价关系。W的τ-等价的成员在时间τ之前模拟相同的行为。如果τ1>τ2，则τ1 <$τ2和w <$∞v保持i <$P w=P v，并且I w和I v在所有符号上一致，除了可能的一些个别变量。[w]τ 是那些v的集合W表示w从时间τ向前的概率分支。定义1.2 L的一般PITL模型是一个形式为W，I，P的元组，其中F，W，I和P如上所述，并且对每个w ∈ W满足以下要求：W在各种解释下是封闭的。 如果wW，x是来自L和R的单个变量，则存在vW使得Pv= Pw，I v=（I w）a，其中（I w）a将x映射到a，并且与其他符号上的I w相同。X x• 函数P w是概率测度。对任意w∈W和τ∈R，函数λX. Pw（τ，X）是布尔代数<$2W，<$2，<$3，<$4，W<$4上的概率测度。此外，λX.Pw（τ，X）需要集中在[w]上：Pw（τ，X）=P w（τ，X <$[w]<$$>）对所有X <$W。一般地说，X∈[w]τ中的一个粒子被选中的概率是P（τ，X）。W满意|=在PITL中定义，关于模型M = W，I，P，a w ∈ W，D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）4145∞|x1，.，xn∈⟨⟩⟨⟩∈∈∈∈∫L和aσ∈<$I。如果这是一个句子，那么[[]] M，w，σ={v ∈ [w]<$max σ：M，v，[min σ，∞]|{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}.这意味着M，w，σ由maxσ-等价于w并且在从minσ开始的无限区间上满足σ的解释v组成。如果CPU有自由变量x1，...，x n，M，v，[min σ，]=0应使用I w（x1），.，I w（xn）作为x1，.，x n，以保持预期的含义。则[n] M，w，σ由满足条件的v ∈ [w]<$max σ组成（vJ∈ W）（P vJ= P v <$I vJ=（I v）Iw（x1），.，Iw（xn）<$M，vJ，[min σ，∞]|= 0）。使用这种符号，概率项t的项值wσ（t）可以通过下式定义：w σ（p（n））= P w（max σ，[[n]] M，w，σ）.其他形式的术语值的定义与（非概率性）国际交易日志相同。在一般PITL模型M=W，I，P中，w W和τ T的概率函数λX，Pw（τ，X）是必需的，因为它们为概率项提供了值。这就是为什么我们接受W，P，I形式的结构及其概率函数λX. PW（τ，X）仅定义在（一般较小的）代数<${[w]]M ，w，σ：<$∈L， σ∈<$I，maxσ=τ}，<$，[w]<$τ<$上作为一般PITL模型也PITL是ITL的保守扩展。 将ITL的证明系统以无限间隔扩展到PITL的系统的公理和证明规则示于[10]对于基于R的语义的推广是完整的，其中R被一个抽象域所取代，并且概率测度只需要是有限自适应的。在PITL的一般模型中，概率函数λX.Pw（τ，X）不需要彼此相关，而应用通常导致具有时间原点τ0=minT和不同的w0的W满足[w0]<$τ0=W，λX，Pw0（τ0，X）可视为全局概率函数。 然后，给定对于任意的wW和τR，概率函数λX.Pw（τ，X）应表示条件概率，条件是与wτ-等价.因此，我们应该（一）Pw0（τ，A）=w∈[w0]<$τPw（τ J，A）d（λX. Pw0（τ，X））.下面的规则使得能够在PITL中以任意精度近似（1校样：（P）（;l=0）l= 0p（p（）x; T）= 0p（（; T）p）≥x.p（; T）<（P）（;l=0）l= 0p（p（）>x; T）= 0p（（; T）p）≤x.p（; T）[10]中PITL的证明系统是最小的。使用缩写h46D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）41LL1L2和[ET<$∈ [l，h]]xl= 0 <$p（n; T）= 1 <$p（n; h; T）=x，我们可以写出导出规则（Seq） α<$（α;l=0）/，β<$（β;l=0）/，[ETα∈ [l1，h1]]x1，[ETβ∈ [l2，h2]]x2，l= 0 <$p（α;β; T）= 1 <$p（αh1;βh2; T）=x1x2这对我们的例子来说尤其重要本文中所使用的无限区间概率DC系统（PDC）是通过将状态变量和持续时间项添加到PITL中来获得的，其方式用于从ITL获得（非概率）DC。相对于基于R的PITL模型的有效性，无限区间DC的公理和规则对于PDC是完整的。2一种玩具并发程序设计语言及其无限区间DC我们提出了一个玩具语言来说明我们的方法。它是在那之后形成的，[6] 并限制了方法调用的形式，以便为使用组件和契约奠定基础。程序由导入和/或导出方法的组件组成。它们的语法是：component：：=组件名称{导入方法}{导出方法}结束名方法：：=name（parameter list）[code];只有导出的方法才需要零件代码它的语法D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）4147/代码：：=停止|（线程）终止语句返回[e]|返回控制和可能是一个值X延拓（x：= e; code）|分配（delayr; code）|延迟指定的时间（call [x：=] name（parameter list）; code）|调用方法，获得值如果最佳则编码否则编码|条件语句letreccodewhereX：code;. ; X：代码|相互递归语句var x;代码局部变量声明代码并行合成我们不允许var出现在其他控制语句的作用域中。分配是原子的。参数按值传递。相互递归语句可以触发无限计算。组件是被动的。程序的活动部分只是一段代码，通常是并发运行的交错线程的集合控制语句的语法故意使尾递归成为重复行为的唯一可表达形式。我们没有给出类型系统的细节，而是默认了DC的一个适当的多排序系统。代码的执行可以根据其信号、变量和参数的值作为时间的函数来描述 语义功能[。]将每段代码映射到DC公式，该公式定义了其可观察行为的集合。我们通过一对相应的可变常数v和v j来模拟每个程序变量v，v和vj表示v在参考区间开始和结束时的值，因此满足公理x（vJ= x; v = x），其中x是刚性个体变量。我们对方法m进行建模，这些方法通过相应的可伸缩函数符号返回一个值 形式为vJ= m（e1，...，e n）意味着参考区间描述了m的完整调用，其中e1，...，e n作为输入参数，vJ作为值。对于不返回值的方法，我们使用一个可伸缩的谓词符号。我们使用专用的状态变量R和W来指示线程当前正在运行，或已终止，分别。在[19，6]的工作基础上，我们使用状态变量N来标记计算时间，这与执行延迟语句所消耗的时间不同，等待环境的反应等， 被认为是可忽略的，以简化计算。R、W和N满足公理T（R，W）[R N |[R |Q<$（[W|;[<$W|）的情况下，48D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）41∫⎜[W惠W1]W2|[R惠R1]R2| ∧⎞⎟电子邮件⎟11111V其表示计算时间是可忽略的，进程永远不会既运行又终止，并且一旦终止，就永远不会重新激活。一对专用的状态变量R和W描述每个线程的状态。N标记所有线程的可忽略时间公式K（V）XJ=x和KR（V）K（V）[R|.x∈V这意味着V中的变量保持其值不变。KR（V）还意味着线程在整个参考区间内都是活动的以下条款定义[。]]V，其中V是给定代码中范围内的程序变量的集合。[[stop]] V[W|[[returne]] V（[<$R|; KR（V）<$rJ =e）[[return]] V[<$R|[[X]]VX[[(C1;C2）]]V（[[C1]]V; [[C2]]V）[[x：= e]] V （[<$R|; KR（V\ {x}）<$xJ=e）[[delay r]] V[<$R|N =N[[ifbthenC1else C2]] V（[<$R|;（b <$KR（V）;[C1]] V）<$（<$b <$KR（V）;[C2]]V））[[callv：= m（e1，.，e n）]] V（[R|; K（V\ {v}）v\J = m（e1，.， e n））[[调用m（e1，.， e n）]] V（[<$R|; K（V）m（e1，.， e n））[[letrecC其中X1：C1;. X n：C n]] Vμn+1X1. Xn Y。[[C1]] V，.，[[Cn]]V，[[C]]V[[varv;C]]Vv|vJ = v）<$$> x <$（vJ = x; v = x））<$$>[[C]] V<${v}[[(CC）]]R[€ R1R2| ∧1 2伏1 212（R，W）[R/R， W/W][[C]]∧⎟T（R2，W2）[[导出m（p1，.，p n）代码]]Qp1. p np n）惠[[code]]惠），如果m返回一个值;[[导出m（p1，.，p n）代码]]Qp1. n（m（p1，.，p n）惠[[code]]惠），D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）4149∫∫∫¬∫如果m不返回值。组件的语义是公式[导出m（p1，.，p n）code]用于其导出的方法。导入方法的声明只携带类型信息。3PDC中定时程序的推理：模式与实例假设C是一段代码。然后公式[C]]V包含了C中调用方法的可伸缩函数和关系符号。假设m是这样一个方法;为了简单起见，让m不返回值。 设B是m的身体。 通过替换我们可以推导出[[导出m（p1，.，p n）B]]<$[[C]] V<$[B]]<$/m][[C]] V，其中替换[B]] n/m]分布在布尔连接词、chop和quantifier上，并且[B]] n/m] m（e1，.，n）定义为[e1/p1，...，n/p n][[B]]假设C在DC中编写的需求ReqC的满足被表示为等价[[C]]要求C并且，根据合同，m应该满足要求Reqm，即，[[B]]要求对每个可接受的B都有效。那么公式[要求m/m][[C]] V VV要求C声明C将满足ReqC，前提是m的导入实现满足要求M.此设置还支持对调用导入方法的代码的执行时间的概率分布进行推理。C和m的值如上所述。则C在d个时间单位内终止的概率可以表示为PDC项p（[[C]] VN≤d; T），其中，我们使用N来衡量延迟或其他进程执行所花费的不可忽略的执行时间。现在设Fm是一个刚性函数符号，使得Fm（x）表示m在时间x内终止的概率的下界。设Pm是m成功执行的前提条件。令p表示p1，...，p n. 然后<$x（l= 0 <$p（Pm（p）<$m（p）<$$>N>x; T）1−Fm（x））<$PITLN>x; T）1−Fm（x））<$PITLd; T）<1 −F C（d，F m）.一般来说，FC表示从分布到分布的映射，但如果Fm的形式直到数值参数如均值和方差都是已知的，那么FC可以定义为从它们的数值域而不是分布空间例3.1考虑下载电子邮件，它包括与服务器建立连接，然后进行实际下载。让代码C调用两个导入的方法，connect（）和getMail（）：varok;callok：=connect（）;ifokthen（callgetMail（）;stop）else stop设Fconnect（t）是在时间t内连接的概率。 让量电子邮件也是概率分布的，并且在时间t下载它的概率是FgetMail（t）。则C的执行时间分布的下界FC满足公式：l= 0 N>t; T）1−Fconnect（t），l= 0 N>t; T）1−FgetMail（t）<<►PITLp（[[C]] N>t; T）<1 − F C（t）.由于可以假设连接时间和下载的电子邮件数量是独立的，（二）yF C（t）=Fconnect（yt）dFgetMail（t）。0F C只能近似地在PITL中导出，因为PITL并不包含在（2）中定义积分时所涉及的极限。这与分布的数值近似的既定用途相对应除了一些深入研究的分布，累积概率函数很少有一个封闭的形式。使用合约可以很自然地使用下限而不是精确的概率。后者也可能不存在。这使得近似令人满意。 为了在PITL中导出（2）的这种近似，我们找到一个序列A k，k = 0，1，. . ，对于涉及Fconnect、FgetMail和t的项，p（[[C]] <$<$N>t; T）1−Ak<对于所有k，可以在PITL中导出，并且通过定义，limkAk=FC（t）。以这个限制为例，我们将离开PITL。 PITL中的推导部分是标准计算的形式化让（3）第2章N>t1N≤t2每 个 方 法 调 用 最 多 只 能 终 止 一 次 。 这 意 味 着 公 式 的 有 效 性 连 接（connect;l=0）和getMail（getMail;l=0），并且使得Seq的应用能够导出D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）4151{−}Kt1KKKp连接ltkK不KKKKΣK6≤ −ǁl= 0p（connect;getMail; T）= 1（l+1）tp（连接ltkK（m+1）t;getMailmtkK; T）=（Fconnect（（L+1）t）−Fconnect（Lt））（FgetMail（（m+1）t）−FgetMail（mt））对于所有的l，m0，...，k1。现在，通过重复应用PITL公理P+，并使用Fconnect（0）=0，我们得到p（（connect;getMail）连接<$N≤t; T）≤L+m≤k−1（l+1）tp（连接ltkK（m+1）t;getMailmtkK; T）+（l+1）t（;L+m=k（m+1）t（请输入）=Fconnect（（k−m+1）t）（FgetMail（（m+1）t）−FgetMail（mt））+BkMK1`Skx其中B k≤ max L≤ k − 1Fconnect（（L+1）t）− Fconnect（Lt），因此lim kB k= 0。通过利用Stieltjes积分的定义，我们有limkSk=FC（t）。因此我们可以取Ak为≤的右边的表达式。请注意，Seq是用C2H42配制的。 代表的是t1≥t1t1≤t2，但它也适用于（3示例3.2考虑尝试快速连续下载5个文件。 如果服务器允许最多4个文件同时下载，则第5个请求可能会因超时而被浏览器取消。 我们有兴趣取消的可能性。下面是相关浏览器代码的一个非常简单的变体：letrecX，其中1X：ifuserRequestthen2（userRequest：=false;3）等待呼叫处理：=requestDownload（url，timeout）;等待4（四）如果处理！=null5⎜ ⎟XtgetMailmtkK⎜52D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）41hen（calldownload（handle）;stop）else（callsignalelse（url）;stop）⎠⎟7）8其他X9假设有一个单独的进程通过设置共享变量userRequest并将URL放在共享变量中D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）4153⎜⎝R⎜⎟⎜⎝[¬R|K|∧⎜⎛KR（V\{handle}）返回handleJ=requestDownload（url，timeout）;33⎟⎠URL.让（[<$R|; KR（V）用户请求）和α（R，T） [<$ |; KR（V）用户请求;[<$R|;KR（V\{userRequest}）验证userRequestJ=false⎛⎜[¬R|;N=T⎞⎟;R（V）手柄！= null;[R|;KR（V）下载（手柄）N = T;[W|根据（4）的语义，α（R，T）描述了重复执行第2-3行和第9行直到userRequest变为真，其中T表示总执行时间，并且β（R，W，T）对应于第4-6行的执行，其中R和W描述了为了完成所请求的下载而创建的线程的状态，并且T表示下载时间。启动五个下载的场景涉及六个线程：一个用于每个下载，另一个用于保持系统准备好进一步的请求。 设R1，...，R6，W1，...，W6描述了六个线程的状态. 然后 这种情况可以用以下公式来描述：（五）1 6 16[EURR... R... ∃W⎜6优惠i=1W i|[R]6优惠i=1R i| ∧⎞⎟[1≤i0，F（al，at）=F（l，t在l超过最高传输速率v的情况下，F（l，t）= 0。 设l i为长度在第i次下载中，i= 1，...，5. 设l i>v（T1+T2+T3+T4），其中i= 1，.，4中为了简单起见，在所有下载都被启动之前，没有一个下载可以结束 那么对于i1，...，4 第一次下载完成，并且在等待的第五次下载超时之前完成，{1，.，q4：Li−qi≤Lj−qj，j=1，.，（四）F（q，t）（l i− q i，timeout）.4k=1FJ（qk，4S=kT s）dq1.DQ4，第五次下载不被取消的概率是P1+. +P4。上述积分的Ap-近似可以在PITL中使用Seq导出，非常类似于例3.1。使用一个合同，其中下载的执行时间近似于一个分布，只取决于要传输的数据量是太粗糙了。如果将竞争性交易的数额考虑在内，则可能进行更准确的计算，但我们建议的合同形式并不允许这样做。4概率定时设计一个设计P，R，通常写为PR，描述了一个由前提条件P，一个输入输出关系R的计算。P约束变量的初始值v，R是v和变量的最终值vJ之间的关系，如果v初始满足P，则R成立。概率定时设计P、R、F还包括执行时间分布F。F（v，t）是计算在时间t内终止的概率的下限，前提是P（v）成立。执行时间上的硬界限d可以由满足F（DJ）= 1的F来表示，对于所有DJ≥ d。Σ超时+D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）4155⟨⟩−⟨⟩⟨⟩× →∈∈4.1在PDC由P、R、F编码的方法m的性质可以写成PITL公式：m<$（P（v）<$R（v，vJ））和l = 0 <$p（P（v）<$m<$l> t; T）<1 − F（v，t）。第一个是m的函数行为。第二个条件是，如果P（v）成立，则mto需要多于t个时间单位，且概率小于1F（v，t）.F只是一个下界，因为不需要存在精确的概率4.2概率定时设计的改进设计D1=P1，R1，F1设计D2=P2，R2，F2，写作D1±D2，如果<$x（P2（x）<$P1（x））、<$x <$XJ（R1（x，XJ）<$R2（x，XJ））和<$x <$t（F2（x，t）≤ F1（x，t））。这意味着D1有一个较弱或等价的前提条件和一个较强或等价的输入-输出关系，并且平均而言至少和D2一样快地终止。显然，如果D1±D2，则P1（v）<$m<$R1（v，vJ）和<$x（l= 0 <$p（P1（v）<$m<$l>x; T）1−F1（v，x））使 x; T）<1 − F2（v，x））。5概率定时合同方法的执行时间取决于在其主体中调用定义5.1 [组件声明]组件声明是一对M i，M e，其中M i和M e分别是导入和导出方法的不相交声明集。定义5.2[概率定时合约]设M i，M e是一个分量分解，V m是声明m的变量的赋值集，m ∈ M iM e。元组C = D m：m ∈ M iM e是M i，M e的合约，如果Dm的形式为<$Pm，Rm，Fm<$，其中(i) <$Pm，Rm<$是对m，m∈Mi <$Me的（非概率）设计。(ii) F m是V m型变量R+[0，1]用于方法声明mMi并且意味着表示M的实现的执行时间的分布。(iii) 对于声明mMe，Fm，给出了概率设计中声明m的实现的执行时间分布的表达式，n∈Mi.我们用Ci，m表示{n∈Mi：Fn发生在Fm中}.语义上，如果m∈Me，则56D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）41∈⟨⟩i，mr+1 mod2si，mreMe我neMMM我eeeMMe我我e我eMMe我我M我我eee我e我ni，mMeenFm的类型为n∈Ci，mVn×R+→[0，1]→（Vm×R+→[0，1]）。在句法上，我们假设Fm是一个表达式，例如，（二）、 契约C表示如果方法m M i满足其相应的设计Dm，并且分布变量F m被赋予其执行时间分布的下界，则来自M e的方法满足其相应的设计，并且表达式F m也评估其执行时间分布的下界。若Ci，m= 0，则Pm，Rm，Fm实质上是一个概率定时设计.定义5.3[概率定时合同的改进]设C和CJ分别是关于Mi，Me j和MiJ，Mej的概率定时合同令C= Pm，Rm，Fm：m∈MiPmJ，RmJCJ±C，如果(i) MiJMi，MejMe;，FmJ<$：m∈MiJ<$MeJ<$. 然后，CJ定义C，写为(ii) <$Pm，Rm<$±<$PmJ，RmJ<$，对于m∈MiJ，<$PmJ，RmJ<$± <$Pm，Rm <$，对于m∈Me;(iii) 对于m∈Me， v∈Vm， t∈R+，FM（v，t）≤Fmj（v，t），Fn，n∈Mi.5.1构建概率定时合约设Ak=<$Mk，Mk<$，Ck=<$$>Pk，Rk，Fk<$：m∈Mk< $Mk <$，k= 1， 2，为2组件声明和概率定时合同，分别为他们。 的1和A2是可合成的，如果M1<$M2=<$.C1和C2是可合成的，如果A1和A2是可合成的，且Dk± D2− k，其中m ∈ Mk <$M2− k，k = 1，2。的组合物C1和C2，记作C1<$C2，是<$$>Pm，Rm，Fm<$：m∈M1 <$M 1<$M2<$M2<$其中：(i) Pm（v）P1（v）<$P2（v），Rm（v，vJ）R1（v，vJ）<$R2（v，vJ）和Fm=F1=M mF2，其中m∈M1<$M2;嗯嗯米伊伊(ii) Pm=Pk和Rm=Rk对m∈Mk<$（Mk\M2−k），k=1， 2;(iii) F m=F k，其中m∈M k\M2−k，k=1，2。为了便于理解，我们首先定义Fm，m∈M1<$M2，在C1和C2不允许方法之间的循环依赖，也就是说，如果没有序列m0，...， m2s− 1使得m r∈ M 1<$M 2，其中r = 1，3，.， 2 s − 1，M r∈ M2<$M 1对于r=0，2，...，2 s−2且m r∈C2− rmod2，r=0，...，2 s-1。 鉴于没有循环依赖，我们可以将m从C1到C2的依赖深度定义为形式为m1，.的最长序列的长度s，ms使得m1∈Ci，m且m r+1∈ Ck，其中k使得m r∈Mk，对于r=1，.，s-1，我们可以通过以下子句对m的依赖深度进行归纳来定义Fm=FK，其中m∈MK，依赖深度为0;Fm= [Fn/Fk：n ∈ Ck]Fk，其中m∈Mk为非零依赖深度。请注意，在以下情况下，替换将Fk替换为来自C2−k的表达式n∈ M 2− k。 否则F k不被这个代换所取代。D.P. Guelev，D.Van Hung/Electronic Notes in Theoretical Computer Science 238（2010）4157MMMMMMXnMMMnni，mMeMMMJMMM如果C1和C2之间存在循环依赖关系，则C1和C2中导出方法的Fms应该是方程组的解Xm= [Xn/Fk：n ∈ Ci，m] Fk.在不限制Fk的情况下求解它可能很难，但如果Fk且单调，则X可以作为序列Xj，jω的极限来获得，其中X000，嗯嗯Xj+1=[Xj/Fk：n∈Ck]Fk，其中m∈Mk.观察到X0 0意味着X1将给出非零终止概率只对m的运行进行调用，不调用其他导入的方法;X2 会给非-零概率的运行与调用导入的方法，这本身导致没有进一步的呼叫等。因为Fk是欠近似的，Fk的单调性需要Xs≤Xs+1 ≤limXj，对于所有sω，Xs可以用作Fm而不是limjj，对于足够大的s，以获得粗略的，但成本较低近似总结发言这里我们只关注执行时间的软需求，但我们相