HOL中pGCL概率保护命令的机械化及其在分布式随机算法中的应用

理论计算机科学电子笔记112（2005）95-111www.elsevier.com/locate/entcsHOL中机械化的可能受保护命令乔·赫德牛津大学计算机实验室安娜贝尔·麦基弗麦考瑞大学计算机系卡罗尔·摩根新南威尔士大学计算机科学学院摘要概率保护命令语言pGCL[15]包含恶魔和概率非确定性，这使得它适合于分布式随机算法的推理[14]。证明是基于最弱的前提语义，使用实（而不是布尔）值函数的底层逻辑。我们使用HOL定理证明器[4]提出了pGCL[16]的定量逻辑的机械化，包括证明所有pGCL命令满足新条件次线性，标准GCL[1]的合取性机械化理论还支持创建自动证明工具，该工具将带注释的pGCL程序及其部分正确性规范作为输入，并从中导出一组足够的验证条件。这是用来验证拉宾的互斥算法[ 10 ]中的概率投票阶段保留字：pGCL，形式验证，概率程序1介绍概率保护命令语言pGCL扩展了Dijkstra的1571-0661 © 2004 Elsevier B.V. 在CC BY-NC-ND许可证下的O笔访问。doi：10.1016/j.entcs.2004.01.02196J. Hurd等人理论计算机科学电子笔记112（2005）95扩展允许对程序的数量属性进行指定，例如“程序提供正确输出的机会至少为0。九十五。”恶魔的非决定论，被Dijkstra确定为抽象和细化的关键概念，被保留下来。在pGCL中，概率和非确定性的结合允许对不精确行为进行现实的处理，避免了无法实现精确概率的问题。例如，一个程序以至少0的概率正确运行（由ok结果指示）。95在pGCL中可以描述为好的。95磅（<$okHok）。这里0. 95表示概率选择（0。95，0。05）之间的左，右参数分别;另一方面，H代表恶魔的选择，被认为是任意选择的。这种概率选择和恶魔选择的结合意味着程序可以表现出一系列行为，而不是一个：上面，“恶魔”只能在5%的时间内选择结果，然后在任何情况下都最多可以说的是，输出正常的概率在95%和100%之间。1我们描述了概率程序的定量性质，pGCL程序被解释为状态的实值函数，而不是布尔值函数，正是这种普遍性允许对概率选择和恶魔选择做出合理的判断，如上所述。在本文中，我们提出了以下重大创新：• 高阶逻辑中pGCL程序（具有最弱前提语义）的机械化，使用HOL 4定理证明器;• 一个自动证明工具，它将带注释的pGCL程序作为输入，并计算足以证明其部分正确性的验证条件;以及• 这个证明工具的应用，以正式验证的概率- tic投票计划在拉宾一个机械化的理论是一个具有机器可读的逻辑形式化的理论;对于pGCL来说，有一个机械化的理论有两个主要的好处。第一个是逻辑形式化的存在：如果理论是通过下定义然后导出它们的结果（而不是简单地断言公理）而在相容逻辑中形式化的，那么理论就有一个强有力的一致性保证。HOL4定理证明器提供工具支持[1]另一种概率程序语义的方法[8]忽略了恶魔般的非决定论，而是将这些概率区间视为原始的。J. Hurd等人理论计算机科学电子笔记112（2005）9597{ } - -Σ×→对于这种机械化的第二个好处是机器可读性：我们可以使用机械化的pGCL理论来支持使用最弱前提语义进行推理的自动证明工具的创建。例如，验证pGCL程序通常涉及大量的数值计算，这可以通过重写有关实数的相关定理来正式执行由于HOL4是LCF家族中的定理证明器，因此它为用户编写此类工具提供了完整的编程语言（ML）[2]。一致性是由逻辑内核强制执行的，逻辑内核是一个小模块，它只被授权创建类型定理的对象，它通过应用高阶逻辑的推理规则来实现。我们创建了许多小工具来加速机械化和程序验证，包括上面描述的实数重写。我们还实现了一个工具，它将带注释的程序C、前置条件P和后置条件Q作为输入，并生成足以满足部分正确性的验证条件（Hoare三元组P C Q）。 它尽可能多地证明这些验证条件，简化剩余部分，然后将它们作为子目标返回给用户，以便交互式地证明节中2.给出了pGCL在高阶逻辑中的形式化，并以Monty Hall博弈为例进行了说明。节中3我们描述了生成验证条件的证明工具;在第二节中。4.我们将这些理论和工具应用于Rabin互斥算法中的概率投票方案的验证高阶逻辑类型包括布尔B、实数R和整数Z。符号t：τ表示项t具有类型τ。 将函数f应用于参数x可以用并置fx来表示，乘法使用显式运算符×而不是并置。 我们使用符号xt来表示x被定义为t。最后，我们使用变量e在表示状态上的随机变量的实值表达式上进行范围，t在变压器上进行范围，s在状态上进行范围，c在命令上进行范围。2形式化pGCL固定一个（可能是有限的）状态空间α，设α是α上的概率子分布，即函数f：α→ [0，1]使得x∈αfx≤1。然后我们可以将概率命令c视为关系α αB初始状态和最终状态的概率子分布之间的关系。这是一种关系（或操作）语义：程序是从一个有定义的98J. Hurd等人理论计算机科学电子笔记112（2005）95→→初始状态并不产生一个确定的最终状态，而是一个最终状态的概率分布，它反映了它执行过程中的概率分支。恶魔分支通过将初始状态与一个以上的最终分布相关联来表示。下面的例子说明了为什么我们需要关系而不是函数，以及概率子分布。例2.1考虑下面的概率程序Ex1（n：=n+1Hn：=n+2）1/2英寸 任务中止，其中H表示恶魔选择，1/2λ表示对称概率选择，Abort表示Ex 1的状态空间是Z（程序变量n的可能值）;将上述语义应用于Ex 1给出了一个关系，该关系将初始状态n= 0与最终状态上的这两个子分布（·· ·，−1<$→0. 0，0›→0. 0，1›→0. 5，2›→0. 0，3›→0. 0，4›→0. 0，· ··）（·· ·，−1<$→0. 0，0›→0. 0，1›→0. 0，2›→0. 5，3›→0. 0，4›→0. 0，· ··） QpGCL的逻辑具有这种关系语义作为模型：它是最初由Kozen [9]提出的定量最弱前提公式，但增加了恶魔选择[16]。一个程序的最终分布是通过给出它们相对于任意随机变量的期望值来描述的，我们认为这些随机变量是量化成功终结的好处的“奖励函数”。这种方法的结果是简化了最终的证明系统，而不放弃表达性[14]。给定一个概率命令c，确定一个从最终状态到非负实数的奖励函数Q：αR+。给定一个初始状态x，我们可以通过取随机变量Q相对于c的输出分布的期望值来计算重复执行c的平均回报如果c也是最后，如果c不终止，约定是奖励为零。使用这个过程，我们可以计算每个初始状态x的期望回报，因此最终得到从初始状态到非负实数的回报函数P：αR+：Q的最弱前提。例2.2再次考虑概率程序Ex1，假设最终状态的回报函数Q定义为：如果n是奇数，则Qn=初始状态x的期望回报函数P是什么？有一半的时间程序会循环，奖励为零。在剩下的一半时间里，恶魔选择的最小期望值J. Hurd等人理论计算机科学电子笔记112（2005）9599∞≡∞∀×∞− ∞赋值会产生奇数结果，因为这个结果的奖励只有2，而偶数结果的奖励是3。所以期待的报酬是Px 1/2×0+ 1/ 2× 2，即对于每个初始状态x都是1。Q期望回报函数（如P）和回报函数（如Q）被简单地称为期望。在pGCL中，我们将概率命令c视为期望Transformer，将最终状态的期望映射到初始状态的期望。概率论的一个基本事实是，如果后期望是从一个谓词中导出的--一个特征函数，对于满足谓词的状态奖励1，否则奖励0--那么前期望给出了程序在满足谓词的状态中终止的最大保证概率。我们将在本节的剩余部分中给出概率程序的这种最弱预条件式语义的形式化。2.1期望转换器的在pGCL中，期望是从状态空间α到扩展的正实数R+[0 ， + ] 的 函数。实数以前已经在几个不同的定理证明器中被机械化了（例如Ergo中的一个例子见[18]），所以我们有一个坚实的基础来构造扩展的正实数。因此，我们首先创建了一个新的高阶逻辑类型posreal来捕获这个域，并将通常的算术运算提升到它上面。自然，我们必须对提升后的算术运算应该如何表现做出一些选择，下面的恒等式总结了我们的决定：你好X1/0 = ∞1/∞= 0x。x=∞∞ ∞ −x =∞ x。x/= ∞ x − ∞ = 0你好0×x = 0×x。x= 0 ∞ ×x= ∞。加法和乘法都被定义为可交换的，所以上面的规则告诉我们x。X例如，0 = 0。 此外，除法是用乘法和倒数来定义的，所以从上面我们可以推断，∞/∞= 0。 事实上，唯一不受上述规则约束的操作是∞ −∞，我们故意不指定。2为了支持我们后面的发展，我们定义了posreal上的min和max运算，以及一个有用的速记来强制执行有界性：[x]≤1minx 1。我们还证明了一系列定理，可以用来重写，对posreal的元素进行数值计算，减少用户在交互式证明中的负担2.在高阶逻辑中，每个函数都必须是全的，所以必须是的某个元素xposreal，但没有定理给出关于x的任何信息。100J. Hurd等人理论计算机科学电子笔记112（2005）95例2.3posreal计算► （1/ 3− 1/ 5）×6 = 4/ 5且∞−53=∞可以由HOL4简化器自动执行。Q现在我们已经定义了正实数的类型，我们把注意力集中在类型上。（α）期望α→posreal，在状态空间α上的期望。注意，α是一个类型变量，可以实例化为任何高阶逻辑类型，因此我们证明的关于期望的定理不假设状态空间的任何属性。3我们定义了几个关于期望的操作，它们只是逐点的对正实数的相应操作的提升零≡ λs。 0Infty λs。 ∞e1± e2 ≡ 一群人。e 1s≤e 2 s最小值e1e2≡ λs。最小值（e1s）（e2s）麦克斯第一季第二集 ≡ λs。最大值（e1s）（e 2s）条件b e1e 2 ≡ λs。如果BS则E1，否则E 2，林PE1 E2 λs。设x←[ps]≤1，在x× e1 s+（1−x）× e2 s中.类型（α）expect形成一个完整的格，其中Min和Max是满足和连接运算符，Zero和Infty是底部和顶部元素。零期望值为每个状态分配零值，而无穷期望值为每个状态分配无穷值。最后，Lin操作构造两个期望之间的线性插值，Cond根据状态空间上的谓词在两个期望之间切换。在pGCL中，概率程序的语义是将最终状态上的后置条件映射到初始状态上的最弱前置条件的期望期望变换器因此具有高阶逻辑类型（α）Transformer（α）expect→（α）expect。为了推理期望变换，我们从格理论中借用了一些标准概念，特别是单调变换的最小和最大不动点的存在性，我们分别称之为期望lfpt和期望gfpt。2.2形式化最弱前提语义接下来，我们定义一个简单编程语言的pGCL语义。为了具体起见，我们首先定义一个状态空间state_string→Z表示，[3]特别地，状态空间可能是无限的。J. Hurd等人理论计算机科学电子笔记112（2005）95101（→发送从变量名到整数值的映射。下面的定义通过将fs赋值给v，从一个旧的状态创建一个新的状态：赋值v f s<$λw。如果w=v，则f selsesw接下来，我们为pGCL命令定义一个新的高阶数据类型命令“中止”|Skip|指定字符串×（状态→Z）|命令序号×命令|恶魔的命令×命令| （状态→posreal）×命令×命令的概率|当（状态→B）×命令时。Abort命令表示程序的非终止性;从技术意义上讲，它是Demon命令使用恶魔选择来决定执行两个参数命令中的哪一个，Prob命令使用概率选择。由于Prob的概率变元是一个函数state→posreal，选择概率被明确地允许依赖于状态。在编写命令时，我们使用以下语法糖来增强可读性：v：= f≡赋值v fc1;c 2≡序列c1c2c1Hc 2≡恶魔c1c2c1p 2≡概率（λs. p）c 1 c 2如果bc1c2≡概率（λs. 如果bs则1否则0）c1c 2v：= {e1，.， {\fn方正黑体简体\fs18\b1\bord1\shad1\3cH2F2F2F}≡v：=e1H ··· Hv：=env：=e1，·· ·，en≡v：=e11/nv：=e2，.， e nnb 1 →c 1| ··· |bn→ cn≡Biholds中的任何一个（在过程中）Hi∈IciwhilehereI{i|1≤i≤n {\displaystyle{\frac {1}。此外，我们通常在表达式和条件中不提及状态，例如写v：= n +1而不是v：= λs。s n +1。我们现在定义最弱的前置条件语义运算符wp，它是一个命令（状态）转换器（Transformer）类型的高阶逻辑函数，并将命令映射到它们的语义含义作为期望转换器：►（wp Abort = λe. 零）（wp Skip=λe. e）、λ e（wp（Assign v f）= λe，s. e（assign v f s）λ e（wp（Seqc 1 c 2））=λe. wpc1（wpc 2e））λ e（wp（Demonc 1 c 2））=λe. 最小值（wpc1e）（wpc 2e））λ e（wp（Probp c 1 c 2））=λe. 林p（wpc1e）（wpc 2e））102J. Hurd等人理论计算机科学电子笔记112（2005）95当bc =λe时，期望lfp（λeJ. 条件b（wpc eJ）e））。例2.4在这个例子中，期望的最终状态是变量i和j具有相同值的状态，因此我们使用后置条件如果i= j则1，否则0。首先考虑方案pdi：= 0，1;j：={0，1}。对pd的直观解读是，首先通过投掷一枚公平的硬币将变量i设置为0或1，然后恶魔将变量j设置为0或1。有了这种解释，我们永远无法打败恶魔就不足为奇了，事实上，我们可以证明，在最弱的前提条件下，每个初始状态都映射到零：接下来考虑一下这个方案► wp pd post=零。dp_j：={0， 1};i：={0，1}，而分配的方式正好相反首先，恶魔必须设置变量j，然后使用公平硬币设置变量i。在这种情况下，我们可以证明► wp dp post=λs。一半，这与我们的直觉相一致，即恶魔在掷硬币之前并不知道公平硬币的结果，因此平均有一半的时间可以被击败。2.3健康状况对于标准GCL，Dijkstra引入了几个同样，概率程序的期望变换器语义与概率程序的操作解释之间存在对应关系-事实上，如果期望变换器是可行的，则它是健康的，上连续和次线性[16]，其中上连续是格理论的属性，可行t=零scalingtx. t（λs. x×e s）=λs。x× tes次加性t= 1，e = 2。 t（λs. e1s + e2 s）± λs。 t e 1 s + t e 2 s减法t_（max），x. c∞ λs。 t e s − x ± t（λs. e s − x）次线性t- 缩放t-次加法t-减法tJ. Hurd等人理论计算机科学电子笔记112（2005）95103可行性是一个直观的属性，对应于DijkstrapGCL中的次线性是标准GCL中合取健康条件的推广，实际上等价于单个公式次线性测试e1，e2，x1，x2，x.（λs. x1× t e1s + x2× t e2s − x）± t（λs. x1× e1s + x2× e2s −x）我们目前的形式化不包括连接ex-第一个是有关系语义的pectation transformers（这是第一个恶魔，Morgan et. [16]）。 相反，我们简单地定义一个谓词健康测试法 可行性测试法连续性测试法次线性测试法把我们的注意力限制在健康的变压器上。单调性，缩放，线性，减法的属性都是健康的逻辑结果，正如我们在定理证明器中检查的那样。我们形式化的主要定理看似简单：► 200c. 健康（wpc）。它指出，对任何命令应用最弱的前置条件语义操作符wp都会产生一个健康的Transformer。我们的直接证明是对命令的结构化归纳，需要800行HOL4证明脚本作为主要证明。（Dijkstra同样使用结构归纳法进行相应的GCL证明。最困难的部分是证明while循环的次线性;为此我们需要几个引理，例如expect lfp的单调性和减法通过健康的transformer子分布。然而，健康条件的重要性不能被夸大：例如，像这样的属性是我们用来推导下面描述的验证计算器的简化规则的。2.4Monty Hall游戏臭名昭著的Monty Hall游戏提供了一个例子，其中恶魔的角色有三个窗帘，参赛者希望通过猜测窗帘隐藏的位置来赢得奖品。游戏开始时，恶魔选择一个奖品幕pc，蒙蒂·霍尔是1963年至1976年的游戏节目《让我们做笔交易》的主持人;具有讽刺意味的是，这个游戏节目以完全不需要参赛者的技能或智力而闻名。104J. Hurd等人理论计算机科学电子笔记112（2005）95把奖品藏起来。接下来参赛者随机统一选择一个窗帘cc。然后恶魔选择一个与pc和cc都不相等的替代窗帘ac，并打开它。此时参赛者可以选择坚持他原来选择的窗帘，或者切换到剩下的关闭的窗帘。参赛者是否应该转换？我们用以下定义来编码蒙蒂·霍尔的参赛者竞争者交换机{1， 2， 3};cc：= 1，2， 3 mm;pc/= 1cc= 1→ac：= 1| pc= 2μcc/= 2→ac：= 2| pc= 3→cc= 3 →ac：= 3;if <$switchthen Skip elsecc：=（如果cc= 1，则 1，否则如果cc= 2，则2，否则3）定义的左侧包括开关作为参赛者的参数;这在右侧的程序中用于确定是否在最后一步切换窗帘。后置条件是参赛者期望的目标，即，如果cc=pc则1，否则为0，则为win。这个例子足够小，我们可以直接在HOL4中验证它，只需重写所有的语法糖，扩展wp的定义并进行数值计算。这样做的效果是将后置条件推回到程序的开始，这对于手工来说并不简单，因为公式变得相当大。经过22秒和逻辑内核中的250，536个原始推理，验证成功，并得到以下定理：► wp（竞争者切换）win =λs。如果交换则2/3否则1/3。换句话说，通过切换，参赛者赢得奖品的可能性是原来的两倍。3验证条件生成器一般来说，程序通过证明下界来证明具有所需的属性-例如，程序Prog可以被证明以至少0的概率正确运行。95、证明不等式► （λs. 0的情况。95）± wpProg（如果可以，则1，否则0），其中，后期望对状态集合的特征函数进行编码，其中某个布尔ok成立。当然，如果更有力的保证需要（0）。99级的置信度），那么就需要一个更强的定理来建立它。在本节中，我们将展示如何机械化J. Hurd等人理论计算机科学电子笔记112（2005）95105证明这样的下限;事实上，我们集中在最弱的自由前提语义的概括，一个有用的削弱最弱的前提语义。53.1弱自由前提语义学最弱自由预条件算子wp是wp的部分正确性模拟。专注于wlp和部分正确性极大地简化了循环程序的形式验证，因为wp最小固定点语义对于证明前提条件的下限是事实上，在pGCL中证明循环完全正确性的常用方法是首先证明部分正确性，然后证明wp和wlp在while循环上一致-这相当于证明循环以概率1终止。这是众所周知的规则的pGCL完全正确性=部分正确性+终止证明，并在其他地方证明了pGCL[13]。此外，简单的技术的基础上的程序变体也已得出。然而，对于本文的剩余部分，我们将只对部分正确性感兴趣，因此终止问题将不涉及我们。对于部分正确性，如果程序没有终止，那么它满足每个后置条件。由于程序唯一可能出现分歧的地方是Abort和While命令，因此最弱的自由前置条件语义运算符wlp仅在这两个命令上与wp不同：它们分别具有wlp中止 Infty和wlp（While b c） <$λe. expect gfp（λeJ. 条件b（wlpc eJ）e）。完整的HOL形式化基于pGCL的部分正确性理论[13]。3.2wlp验证条件在本节中，我们假设我们有一个pGCL命令c和一个后置条件q，我们希望推导出最弱自由前提的下界如果我们将其视为一阶查询P±wlpcq，那么我们可以使用以下定理和Prolog解释器来求解变量[5]事实上，对于终止程序来说，没有削弱。106J. Hurd等人理论计算机科学电子笔记112（2005）95P.►Infty±wlp中止Q►Q±wlp跳过Q►（Q）±wlp（AssignV F）Q►R±wlp C2 QQ P±wlp C1 R⇒P±wlp（Seq C1 C2） Q►P1±wlp C1 Q P2±wlp C2 Q⇒最小P1P2±wlp（ DemonC1C2）Q►P1±wlp C1 Q P2±wlp C2 Q⇒LinP P1P2± wlp（ ProbP C1C2）Q►P1±wlp C1 Q P2±wlp C2 Q⇒条件B P1P2±wlp（如果B C1C2）Q向后传播条件的优点（这里使用Prolog解释器实现）是可以避免不必要的注释。例如，考虑序列wlp（Seqc1c2）q。这两个命令之间不需要注释，因为Prolog解释器使用这些规则来求解wlpc2q上的下限r，然后再求解下限p，然后返回p作为整个命令的下限wlp（Seqc1c2）q.但是，需要使用注释来部署以下关于while循环的定理：► QRP，Q，b，c. P ± Cond b（wlp c P）Q P ± wlp（While b c）Q.为了插入注释，我们定义了一个断言命令，它简单地忽略作为其第一个参数给出的公式：因此Assertpcc。这是我们给Prolog解释器的精确规则：► R±wlpcPP ±CondbR QP ±wlp（断言P（同时bc））Q因此，用户需要在while循环周围的Assert中提供一个有用的循环不变式P请注意，Prolog策略将在第一个子目标上成功，为while循环的主体导出一个下限，但第二个子目标将失败，因为没有适用的规则。在我们的策略中，失败的子目标不会启动回溯，而是变成验证条件。因此，在这种方式下，程序中的每个while循环将生成一个验证条件，在这种情况下，提供的P实际上是建立Q的正确不变量。嵌套的while循环以完全相同的方式工作：外部循环的不变量将通过主体向后传播，当它遇到内部while循环时，将生成验证条件。完整的wlp策略工作原理如下：(i) 取形式为p±wlpc q的目标作为输入。(ii) 扩展c中的任何语法糖。(iii) 创建查询X±wlpcq并传递给Prolog解释器。J. Hurd等人理论计算机科学电子笔记112（2005）95107±2(iv) 结果将是一个定理►Vir±wlpcq，1≤i≤n其中Vi是验证条件。(v) 应用±的传递性将初始目标简化为子目标p±r和r±wlpc q。(vi) 使用Prolog返回的定理将子目标r±wlpcq简化为子目标V1，.，Vn.(vii) 用±、Min、Lin和Cond的定义扩展所有子目标。(viii) 试着通过简化它们和进行任何数值计算来证明所有的子目标。(ix) 将所有未证明的子目标返回给用户，以进行交互式证明。回到Monty Hall博弈的例子，我们可以应用wlp策略完全自动地证明以下部分正确性定理：► （λs. 如果交换机则2/3，否则1/3）±WLP（竞争者交换机）获胜。因为在竞争者程序中没有while循环，所以没有验证条件，唯一重要的子目标是策略步骤v中生成的p r。然而，这是通过步骤viii中的简化和计算自动证明的，因此没有子目标返回给用户。这个对Monty Hall博弈的自动验证显然比第2.4节中描述的交互式证明版本要简单得多，后者需要18行HOL4证明脚本，但定理的自动版本更弱：它只显示部分正确性。4Rabin's Mutual Exclusion Algorithm（拉宾假设N个处理器同时执行，并且其中一些处理器不时地需要访问代码的关键部分拉宾投票方案背后的想法非常简单：每个处理器都投掷一枚公平的硬币，直到第一个正面出现，6并且需要最大数量的处理器赢得选举。换句话说，每个处理器从几何（1）分布中挑选一个整数108J. Hurd等人理论计算机科学电子笔记112（2005）952在我们的验证中，我们不对同时执行上述投票方案的i个处理器建模，而是对拉宾使用的系统的等效公式建模。前引书]：(i) 用竞争独占访问临界区的处理器数量初始化i(ii) 如果i= 1，那么我们有一个唯一的赢家：返回S成功。(iii) 如果i= 0，则选举失败：返回失败。(iv) 抛硬币：由于每次抛硬币都产生概率为1的正面，因此每个处理器都以该概率退出。我们通过消除所有这些处理器来减少i，因为它们中肯定没有一个赢得选举。(v) 返回步骤（ii）。以下pGCL程序实现了该算法：（1）第一条：（1的概率;invar 2对应于内部循环终止于i= 1的概率。因此，外层循环终止于i= 1的概率p满足p=pinvar 1+invar 2，我们证明了投票算法在p= 2/ 3时有效。为了部署wlp策略，需要一个等价的注释版本的程序，通过使用Assert用上述不变量注释rabin来接下来，wlp策略被应用于生成的结果（一个和往常一样，加上两个由while循环生成的验证条件）。wlp策略自动证明了其中一个，并简化了其他两个。我们应用了一些自定义简化，并留下了三个依赖于指数性质这些由58行证明脚本发送，完成了对拉宾行为规范（1）的验证。5结论和相关工作我们已经展示了如何在高阶逻辑中形式化pGCL的理论，pGCL是一种在公共框架中推理恶魔和概率选择的语言;我们已经实现了一个验证条件生成器来帮助形式化证明程序的部分正确性，并且我们已经在一些小例子上演示了它。这项工作证明了使用定理证明器将程序语义理论机械化的好处。特别是，定理证明器是与验证条件生成器非常好地交互的：如果出现了不能被自动证明的子目标，那么它们可以被传递给用户进行人工证明，而不是导致失败。此外，我们利用了HOL4的LCF设计，它保持了用户定义策略的一致性：验证条件生成器非常复杂，但它创建的任何定理都具有高度的可靠性。未来的工作将集中在形式化wp和wlp语义之间的对应关系 这将另外需要终止的证明，并且提供对概率变体和其他变体的工具支持将是有趣的110J. Hurd等人理论计算机科学电子笔记112（2005）95终止参数。第一位作者在HOL4[7]中机械化了概率程序的语义，但这种语言不支持恶魔选择。第三作者最近扩展了B工具（程序改进的证明助手），使用概率选择构造[6]。概率模型检查器（如PRISM[11]）可以有效地计算包含概率和恶魔选择的有限状态机的最弱前提条件，并且还可以处理循环而无需有用的另一方面，逻辑的有限表达性意味着有时它不能完全通用地建模算法，而是必须限制在固定数量的处理器上。Harrison之前在HOL Light定理证明器[ 5 ]中将Dijkstra的最弱前提语义机械化最后，有几种while语言的验证条件生成器是为了与HOL定理证明器一起使用而创建的，从1989年Gordon的开始确认这项工作完成时，赫德是休假从计算机实验室-在剑桥大学，访问麦基弗的支持奖学金在麦考瑞大学在悉尼举行。他目前是牛津大学马格达伦学院Morgan拥有新南威尔士大学的澳大利亚教授奖学金，并与NICTA有联系。引用[1] E.W. 迪杰斯特拉 程序设计的一门学科。 普伦蒂斯·霍尔1976年[2] M.戈登河Milner，和C.沃兹沃斯爱丁堡LCF，计算机科学讲义第78卷。斯普林格，1979年。[3] M.J. C 戈登 在高阶逻辑中机械化编程逻辑。 In G. Birtwistle和P.A. Subrahmanyam，编辑，硬件验证和自动定理证明的当前趋势，第387-439页。Springer-Verlag，1989.[4] M.J. C 戈登和TF梅尔汉姆HOL（A Theorem-Proof Environment for Higher Order Logic）剑桥大学出版社，1993年。[5] 约翰·哈里森。正式的Dijkstra。In Jim Grundy and Malcolm Newey，editors，Theorem Provingin Higher Order Logics，11th International Conference，TPHOLs斯普林格。J. Hurd等人理论计算机科学电子笔记112（2005）95111[6] Thai Son Hoang，Z. Jin，K. Robinsion，A.K. McIver和C.C. Morgan.概率机器的概率不变量在Proceedings of the 3rd International Conference of B and Z users2003中，卷2651的LectureNotes in Computer Science，第240斯普林格。[7] 乔·赫德。概率算法的形式验证。剑桥大学博士论文，2002年。[8] 迈克尔·胡特区间域：aCTL和aPCTL的匹配器。 在Rance Cleaveland，Michael Mislove和PhilipMulry，编辑，美国-巴西软件系统正式基础联合研讨会，理论计算机科学电子笔记第14卷。爱思唯尔，2000年。[9] 德克斯特·科曾概率PDL。1983年第15届ACM计算理论研讨会论文集[10] Eyal Kushilevitz和Michael O.拉宾随机互斥算法再访。Maurice Herlihy，编辑，Proceedings ofthe 11 th Annual Symposium on Principles of Distributed Computing，第275-283页，温哥华，BC，加拿大，1992年8月Press.[11] M. 夸特科夫斯卡湾Norman和D.帕克Prism：概率符号模型检查器。在PAPM/PROBMIV 2001工具会议记录，2001年9月[12] 安娜贝尔·麦基弗和卡罗尔·摩根。概率系统的抽象、精化与证明Springer Verlag，2004年。http://www.cse.unsw.edu.au/www.example.com[13] A.K. McIver和C.C. Morgan.概率程序的部分正确性。Theoretical Computer Science266（1[14] 卡罗尔·摩根。概率循环的证明规则。在BCS-FACS第七届精炼研讨会上。何继锋，约翰·库克和彼得·沃利斯（编）。Springer VerlagWorkshops in Computing，1996年。[15] 卡罗尔·摩根和安娜贝尔·麦基弗。pGCL：随机算法的形式化推理。南非计算机杂志，1999年。[16] 卡罗尔·摩根，安娜贝尔·麦基弗，凯伦·赛德尔。可能是同品种变压器。ACM Transactions onProgramming Languages and Systems，18（3）：325见[12]。[17] 我是Ni p kow。 HoarelogicsinIsabelle/HOL.在H。 我是一个很好的朋友。Steinbrüggen，编辑，Proof and System-Reliability，第341-367页Kluwer，2002年。[18] 杰米·希尔德，伊恩·J.Hayes和David A.卡林顿在定理证明器中使用理论解释来机械化实数Colin Fidge，编辑，《理论计算机科学电子笔记》，第42卷。Elsevier，2001年。