可在www.sciencedirect.com在线获取理论计算机科学电子笔记319（2015）351-367www.elsevier.com/locate/entcsVPHL：一种概率程序的可验证部分正确性逻辑罗伯特·兰德2 史蒂夫·兹丹切维奇3计算机与信息科学宾夕法尼亚大学摘要我们引入了一个Hoare风格的概率程序逻辑，称为VPHL，已被正式验证在Coq证明助理。 VPHL的特点是命题的，而不是加法的，断言和一组简单的规则，用于使用概率论的标准公理来推理这些断言。VPHLstic）程序终止。底层的简单概率命令式语言PrImp包括一个概率抛出运算符、概率保护和潜在非终止while循环。关键词：Hoare逻辑，形式验证，Coq，概率规划，非终止性1引言霍尔逻辑长期以来一直被用作形式验证程序的一种手段，并且有几篇论文提出了对概率程序进行推理的变体[6，7，10，20]。这些方法之间有很大的差异，但都包含某些设计选择：它们考虑子分布而不是完全分布，并且它们限制了非终止的可能性。第一个限制了我们引入Pr（2= 2）=1这样的断言，它经常在变量赋值之前x：=2，我们的推论。它还阻止我们对概率求补，这对概率推理至关重要。消除while循环，或者将我们限制在那些保证终止的循环中，不仅限制了我们可以分析的程序类型，而且还删除了Hoare逻辑的一个核心特性：部分正确性断言。我们引入了一个验证的概率霍尔逻辑（VPHL），1本材料部分基于NSF资助的工作，资助号为CCF-1421193。2电子邮件：rrand@seas.upenn.edu3电子邮件：stevez@cis.upenn.eduhttp://dx.doi.org/10.1016/j.entcs.2015.12.0211571-0661/© 2015作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。352R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351i=1623专门关于完全分发，并适用于潜在的非终止程序。重要的是，VPHL本身在Coq证明助手中得到了正式验证[9]。随着概率霍尔逻辑越来越多地用于验证关键代码（例如，在Easycrypt项目[2]中），重要的是逻辑本身应该建立在最坚实的基础上。经典的霍尔逻辑推理程序状态，从标识符（或变量）到值的映射。命令是从一个状态到另一个状态的部分函数：例如x：=1将状态θ取为将x映射为1的状态，否则相同。三元组{x= 1}c{z = 3}断言，如果状态将x映射到1，则我们从该状态运行程序c，假设程序终止，结果状态将把z在为概率程序设计霍尔逻辑时，我们希望引入具有概率命题的三元组，如{Pr（x = 1）>1}c{Pr（z = 3）= 2}。由于状态是确定性的（一个状态要么将x映射到1，要么例如，如果我们在确定性状态下投掷一枚公平的硬币T，我们会得到一个状态分布：一个状态将T映射到正面，另一个状态将T映射到反面;每个状态的权重为12在第2节中，我们形式化了分布的概念。 在以下部分中我们介绍我们简单的概率命令式语言PrImp。第4接下来（第8节），我们将讨论如何将终止分析与部分正确性断言相结合，以产生一般不可判定问题的精确特征。最后，我们的逻辑在实践中的一个例子，讨论可能的扩展的逻辑，并在该领域的相关工作的审查我们将偶尔参考本文的扩展版本[21]，其中包括其他示例和对替代If和While规则的讨论。Coq的基础开发在www.example.com上https://github.com/rnrand/VPHL。2分布建模首先，我们需要将分布和状态分布的概念形式化一具有有限支持的分布是元素{x1，x2，...，xn}以及关联权重{w1，w2，...， 其中，每个wi∈ [0，1]且n∈wi= 1。在在我们的开发中，我们将专门关注程序状态上的分布。我们通过加权树结构来归纳地定义分布（范围为θ）。分布的叶子包含状态（从标识符到数值和布尔值的映射），表示为θ，我们使用单位θ来提升状态一元分布。组合运算符θp取两棵树Θ1和Θ2并将它们组合成一棵更大的树，将权重p∈（0， 1）与Θ1相关联，将权重（1-p）与Θ2相关联。例如，假设我们想给θ1和θ2分别赋予1的权重，.R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351353⊕≡Σ.A：：= n|v| A + A| A−A| A AB：：= t|F| A = A| A
p| P P| P PFig. 1. PrImp表达式与VPHL剩下三分之二的重量为θ3。我们可以用下面的树来表示这个分布：1 13 612单位θ1单位θ2单位θ3单位θ115Unitθ2Unitθ3它们对应于（Unitθ1<$1Unitθ2）<$1Unitθ3和Unitθ1<$1（Unitθ2<$12 3 6 5单位θ3）。这就引出了我们的分布等价性概念。 我们说θ1Θ2如果在分布的支撑中赋予每个θ的总权重相等。[4]在我们的发展中，我们使用了以下三个引理，它们对所有分布Θi和p，q，r∈（0， 1）都成立：引理2.1（互补性y）Θ1<$pΘ2<$Θ2<$1−pΘ1引理2.2（结合性）（Θ1<$q Θ2）<$pΘ3< $Θ1<$pq（Θ2<$p（1-q） Θ3）1−pq引理2.3（合并）（Θ1<$q Θ2）<$p（Θ3<$r Θ4）<$（Θ1<$q其中pJ=pq+（1−p）r，qJ=pq，rJ=p（1−q）pq+（1−p）r r（p−1）−pq+1我们现在定义分布上的概率 在一般情况下，对X上的任意分布X和函数f：X→Bool，PrX（f）={wi：f（xi）= t}.我们可以归纳地定义如下：Pr（单位x）如果f（x）=t，则（f）=10 iff（x）=fPr（X1<$pX2）（f）= p·PrX1（f）+（1 − p）·PrX2（f）。[4]在我们的Coq发展中，我们没有证明状态等价的可判定性，因此分布等价是根据状态上的布尔谓词来定义的，我们可以为此陈述等价引理。⊕⊕⊕354R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351≡⇓分配Skipskip/UnitθUnitθθ（a）=nc1/单位θ<$θ′c2/Θ′<$θ ′′序列c1;c2/单位θθ′′θ（b）=b0布尔赋值如果为Truex：=a/单位θ<$单位θ[n/x]θ（y）=tc1/单位θθ′ifythenc1elsec2/Unitθθ′y：=b /单位θ<$单位θ[b0/x]θ（y）=fc2/单位θθ′如果Falseifythenc1elsec2/Unitθθ′而端结合θ（y）=fwhileydoc/Unitθ<$Unitθc /Θ1 θ′1c / Θ2 θ′2c /Θ1<$p Θ2< $Θ′1<$p Θ′2θ（y）=tc /单位θθ′whileydoc/Θ′<$Θ′′L oopwhileydoc/Unitθθ′′p∈（0，1）Tossy：=抛数（p）/单位θ<$θ[t/y]<$pθ[f/y]图二. PrImp的操作语义我们可以使用这个构造来推导离散概率论的所有标准定律（更多细节请参见扩展论文和Coq开发在我们的逻辑中，分布的元素总是状态。 概率函数f是从PrImp提升的布尔表达式B（见图1），其中B（θ）是给定状态下B的值。例如，设Θ是我们的分布，并假设θ1（x）= 2，θ2（x）= 1和θ3（x）= 2。考虑布尔表达式b（x = 2）。则b（θ1）=t，b（θ2）=f，b（θ3）=t。因此，我们认为，PrΘ（b）=1+ 0 +2=5。6 3 63一种简单的概率祈使语VPHL将让我们证明关于PrImp的断言，PrImp是来自Software Foundations [ 19 ]的简单命令式语言Imp的概率变体，增加了一个掷硬币的操作符。我们在图2中给出了PrImp的大步操作语义，其中c /ΘΘJ意味着如果我们在状态分布θ中计算c我们得到新的分布ΘJ。PrImp(i) PrImp应该包含确定性编程语言的嵌入(ii) 确定性命令应该保留概率。(iii) 任何具有非终止分支的程序都不应该终止。我们通过“提升”Imp来满足这些原则，使得每个命令都以其传统的方式在单位（或单状态）分布上运行。 Combine规则递归地将给定的命令应用于支持中的所有状态，当且仅当每个这样的状态都在命令上终止时终止，满足原则（iii）（我们将在下一节中讨论这种指定的基本原理）。 新命令p：= toss（y）将单位分布分为两个单位状态，第一个状态的权重p和y设置为t，第二个状态的权重（1-p）和y设置为f。以下两个引理直接来自我们的操作语义，R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）3513553值得明确指出：引理3.1（分解）对于任意c，p，Θ1， Θ2， ΘJ1， ΘJ2，c/Θ 1pΘ 2θ J1pΘ J2 c/Θ 1θ J1 c/Θ 2θ J2.引理3.2（步决定论）对于任意c，Θ， ΘJ， ΘJJ，c/Θ θ jc/Θ θ j = θ JJ.4霍尔逻辑语义学我们现在有足够的背景来正式定义霍尔三元组。让我们从经典（非概率）霍尔三元组的形式定义这里P和Q是关于状态的断言，或者更正式地说，是从状态到命题的映射：定义4.1我们说经典的霍尔三元组{P}c{Q}是有效的，如果<$θ，θJ：P（θ）<$c/θ<$θJ蕴涵Q（θJ）。我们称P为前置条件，Q为后置条件。在我们的霍尔逻辑中，所有断言都直接与概率相关，使用图1中定义的概率断言。请注意，算术和布尔表达式与我们在上面的状态分布上的概率定义以及PrImp本身的命令中使用的表达式相同特别地，[Pr（B）=p]（Θ）转化为PrΘ（B）=p，并且对于和>也是如此。<和我们表示，给定的布尔表达式b在Pr（b）= 1的分布中为真，我们将[b|，并将这些断言称为非概率性断言。定义4.2我们说一个霍尔三元组{P}c{Q}在PrImp是有效的，如果<$Θ，ΘJ：P（Θ）<$c/Θ<$ ΘJ意味着Q（ΘJ）。如前一节所述，PrImpwhile循环在给定的发行版上终止，当且仅当它在发行版支持的每个状态上终止因此，下面两个程序在我们的语言中不会终止，即使第二个程序传统上以概率1终止：y：= toss（2）;ifythenx：= 4else whiletdoskip（1）y：= toss（1）;whileydoy：= toss（1）（2）2 2这在一定程度上是由于我们采用了霍尔如果规则（见图4在本文中）。我们分别对if语句的每个分支进行推理，然后将它们的结论合并。如果这两个结论中的任何一个只是空真的（因为分支没有终止），并且程序被认为终止，那么我们的合取将是假的。因此，我们也称这样的程序为非终止程序.356R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351ppppyppppp55555P ′→P{P}c{Q}Q→Q′后果{P ′}c{Q′}{P}c1{Q}{Q}c2{R}序列{P}c1;c2{R}{P}跳过{P}Skip{P[z<$→e]}z：=e{P}分配P中的y游离yToss{P}y：= toss（p）{PQp}图3.第三章。霍尔逻辑的基本规则5霍尔逻辑基本规则我们现在可以介绍VPHL本身。图3显示了VPHL的基本规则。if和while命令的规则在图4和图5中给出，讨论将推迟到本文后面。我们将提前展示我们的稳健性结果：定理5.1（合理性）本文中提出的所有VPHL规则对于PrImp的语义都是合理的。我们在Coq发展中证明了这个定理，其中每个规则都被单独验证为合理的。在本文中，我们并不要求完整性（即，可以通过我们的Hoare逻辑推导出所有可能的东西），尽管我们确实通过例子证明了VPHL的可用性（第10节）。基本规则（除了Toss）是从经典Hoare逻辑中保留下来的。 toss命令将标识符y分配给t或f，概率分别为p和（1−p）。对于我们的霍尔逻辑，我们限制y在前提条件P中出现。由于新抛出的y必然独立于所有先前的概率，因此我们可以用Pr（b）=q来更新所有形式为Pr（b）= q的陈述y）=pq.我们定义Py，读作如下所示：（Pr（b）=q） yy）=（1− p）q（Pr（b）q）yy）（1−p）q（Pr（b）>q）yy）>（1−p）q<<<（P1P2）yP1yP2（P1P2）yP1yP2方便的是， 的 所得 规则是无损的。当 我们 适用 的 掷定则{P}y：= toss（p）{Pp}，任何在前置条件中为真的命题在后置条件中仍然为真。为了使其正式化：引理5.2对所有P，Py包含P。我们可以通过简单地在每个原子命题中对y进行边缘化来证明这一点例如，P（by）=1和P（by）=2意味着P（b）=1+2=3。我们我会在整篇论文中使用这种技术，通常是含蓄地使用。yyppR. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351357111 1{P[y|}c1{Q}{P[<$y|）}c2{Q} 确定性如果{P（[y|[|）}ifythenc1elsec2{Q}0q）|y<$Pr（X<$y）>q（P1<$P2）|y P1|y P2|y（P1至P2）|y P1|y P2|y358R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351p∗2 2 21222P→D{P[y|}c{P}{D[y|}c{D（[y|[|D是非概率的，{P（[y|[|）}whileydoc{P<$[<$y|}图五. while规则对于子分布的推理，我们采取将两个子分布都缩放到完全分布的方法，允许我们正常地推理而不必限制我们的逻辑。我们通过缩放算子实现这一点1将前置条件和后置条件中的所有概率按比例放大p或11−p其中p是守卫的概率既然我们子分布（不仅仅是子断言），我们需要以下引理：引理6.2对于任何Θ 1，Θ 2，其中Pr θ1（y）= 1且Pr θ2（y）= 0，[P1|y]（Θ 1<$p Θ 2）当且仅当[1<$P]（Θ1）引理6.3对于任何Θ 1，Θ 2，其中PrΘ1（y）= 1且PrΘ2（y）= 0，[P2|<$y]（Θ 1p当且仅当[P]（Θ）（1−p）我们证明，如果P |y保持完全分布，则p P保持其中y为真的子分布。然后我们就可以分别推理c1和c2对这些分布 为了组合这两个后置条件，我们将|y和|是的。(That是，我们将保护y的值与所有概率表达式结合，确保它们不重叠）。为了防止形式为P（yy）=p的陈述出现在组合后置条件中，我们限制y在c1或c2中被重新赋值。读者可以观察到VPHL的规则是标度不变的这表明，我们可以简单地对P1进行推理，而不是对P1和P2进行缩放|y和P 2|分开。事实上，如果有一些小的限制，这样一个如果规则将是合理的，我们将在扩展文件中讨论这个规则7while规则为了解释和证明我们的While规则的形式（见图5），让我们考虑经典的霍尔逻辑While规则，以及为什么它对概率程序失败{Py}c{P}{P}whileydoc{P<$y}考虑以下霍尔三元组：{Pr（yJ）= 1<$[y→ yJ|}whileydo（yJ：= toss（1）;y：=（yJ<$i5）;i++）{Pr（yJ）= 1<$[y→yJ|[|}R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）3513592232j1J3有两个主要问题与推导这个三元组。第一个是在前提条件Pr（yJ）=1<$[y→yJ]中出现矛盾|[y|则Pr（y）= 且Pr（y）= 1。此外，后置条件为假- 如 果 初 始 i = 1 ， 我 们 运行 循 环 5 次 ， y j 为 真 的 概 率 为 2 − 5 = 1 。这说明，如果分布的不同分支遍历循环不同的次数，则不能保证概率不变量保持不变。因此，我们引入限制（图5），即y的值必须保持非概率性（即，[y|或[<$y|）在每个迭代循环完成时，确保如果循环终止，所有分支同时终止。或者更确切地说，所有分支都应该同时终止，但我们遇到了一些困难：虽然P可能对给定的分布Θ1<$p Θ2成立，并且足以在运行c时保持P和y的确定性，但然而，我们有一个很好的非概率断言子集（也就是说，每个概率为零或一的断言）确实满足这个属性。引理7.1对于任何非概率断言P，P（Θ1<$p Θ2）蕴涵P（Θ1）且P（Θ 2）对任意p ∈（0，1）。因此，我们的While规则需要一个非概率不变量，它保留了与概率不变量一起展示的守卫的确定性。在实践中（与一般情况相反），这被证明是相当简单的，而且往往相当方便。例如，我们可能只需要证明我们的计数器确定性地在{0，1，.，n}，并且y仅取决于i，例如当分析n顶点图上的随机游动时。我们分别推理主要的不变量，其中可能包括概率命题。8概率终止程序的推理再考虑一下第4节中的以下简单程序。y：= toss（2）;ifythenx：=4else whiletdoskip我们称这个程序为cpartial。根据PrImp的操作语义，这个程序不会终止，因此{ P } c partial { Q }对于任何断言P和Q都是有效的然而，如果我们考虑对应于cpartial的真正概率程序（一个具有随机数和概率步骤的种子），我们知道Pr（x=4y）= 1在成功终止时。更一般地说，对于一个不重新分配y的任意else分支360R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351323如果else分支以概率1终止如果其他branch以概率y0终止我们知道：n∈（2，1） 否则这表明，如果我们有关于每个分支终止的概率的信息，我们可以将其与对每个分支的直接分析相结合，以得出结果的精确概率。这要求（1）每个分支以概率0或1终止，以及（2）每个分支独立分析，并具有自己的后置条件。现在我们注意到我们的逻辑的三个重要特征。(i) if语句的每个分支都有自己独立的派生(ii) if语句的后置条件显式地提到了保护的值(iii) While规则要求循环以概率0或1终止因此，有了简单的限制，如果语句上的守卫在程序中没有重新分配或通过霍尔逻辑推导中的后果规则消除5，我们可以将我们的逻辑与终止分析相结合，以精确地描述概率终止程序。考虑下面的例子，其中c1到c4是不修改y1，y2或y3并且不保证终止的程序：y1：= toss（p）;y2：= toss（q）;y3：=toss（r）;如果y1，则ify2thenc1;x：=1elsec2;x：= 2其他ify3thenc3;x：= 3elsec4;x：= 4假设c1、c2、c3和c4容易被VPHL分析（即它们的while循环确定性地终止或循环），我们应该能够推导出以下后置条件：Pr（x = 1y1y2）= pqPr（x = 2 y2）= p（1 − q）∧Pr（x= 3y1y3）=（1−p）ry1y3）=（1−p）（1−r）现在想象一下，我们知道只有C3永远不会停止。则x取1、2和4的先验概率分别为pq、p（1−q）和（1−p）（1−r），对应于我们的后置条件中的值的先验概率[5]这种限制要求我们谨慎地管理推理的范围，以避免矛盾的断言。例如，如果一个分支是非终止的，我们可以使用While规则来导出false，从而得出关于程序的另一个分支的不正确断言。在我们可以将所有后续命令移动到If语句中的情况下，If规则的形式为我们确保了这种作用域。然而，在循环的一般情况下，作用域更难实施，并且留给逻辑的用户Pr（x= 4πy）=R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351361N11N程序循环是（1-p）r。在程序成功终止后x= 1，概率为pq1−（1−p）r 对于其他终止结果也是如此。另一方面，如果我们无法对结果的可能性得出任何结论。这在一般情况下，任何命题在程序终止时的概率直接取决于确实终止的分支的权重，从而减少了直接将概率分配给停机问题的问题。9扩展VPHL在我们使用VPHL验证一些示例程序之前，我们将介绍一些符号，这些符号将使我们的任务更容易。第一个是从均匀分布中提取。我们将“语法糖”定义为一系列投掷的语法糖：x：= ORM（1）x：=1x：=int n（n）;ifuthenx：=Nelsex：= ORM（N−1）其中u是一个保留的布尔变量。我们可以证明相关的霍尔规则6x游离Px制服其中Px{P}x：= ORM（N）{PN}是Py的类似物，其中[P（b）=p]xP（bNpNNP（b x = N）= 1。VPHL规范中缺少的另一个有用功能是在概率断言的右侧包含标识符的能力。这有一个明显的原因：概率断言指的是一个分布，该分布中的不同状态可以将给定的标识符映射到不同的值。 同时，一些标识符将在我们的程序中确定性地设置，我们可能会引用它们。我们可以将所需的断言表示如下：nk< N，Pr（i = k）= 1 →Pr（b）= f（k），其中b是任何布尔表达式，i是我们希望包含在概率中的标识符，f是我们希望依赖于i的实值函数。这里的泛量化器代表一系列的合取。类似地，我们希望能够说，标识符i确定性地取{1，2，.中的某个值。n}。我们把它写成i∈ {1，2，. n}是[i = 1]的简写|[i = 2|···|.上述两个结构都要求我们对i的可能值有一个上限，但这是经常发生的情况，就像我们分析的例子一样[6]这是为了说明我们原则上可以在逻辑中证明什么，尽管这个规则和给出的例子在Coq中没有得到验证362R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351N10模拟均匀分布作为我们的逻辑的一个简单证明，让我们尝试证明上面的霍尔逻辑规则。在一般情况下证明该规则需要在前提条件上的归纳和在N上的归纳。相反，让为了使用If规则，我们将u替换为u1和u2。（3）算法1return（1/3）;如果u1，则x：=3其他u2：= toss（1/2）如果u2，则x：=2其他x：=1结束如果结束如果现在我们将尝试证明，对于形式为Pr（b）=p的原子命题P，{P}x：= P（N）{Px}。在整个程序中，我们将隐式地使用结果规则将Pr（b）=p转换为Pr（b<$2= 2）=p或Pr（b）=p<$Pr（t 我们偶尔会通过箭头符号（→）来明确这一点。我们将子导子缩进并内联，这在霍尔逻辑分析中很常见：R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351363333算法2均匀推导{Pr（b）=p}return（1/3）;{Pr（u1）=1/3<$Pr（b<$u1）=p/3<$Pr（b<$u1）=2p/3}如果u1，则{3/1 <$[Pr（b）= p/3]<$[u1|} → {P r（b 3 =3）= p}x：= 3{Pr（bx= 3）=p}其他{3/2 <$[Pr（b）= 2 p/3]<$[<$u1|} → {Pr（b）= p}intn（1/2）;{Pr（u2）=1/2<$Pr（b<$u2）=p/2<$Pr（b<$u2）=p/2}如果u2，则{Pr（b）=p}x：= 2{Pr（b<$x= 2）=p}其他{Pr（b）=p}x：= 1{Pr（b<$x= 1）=p}end if{Pr（b<$x= 2<$u2）=p/2<$Pr（b<$x= 1<$u2）=p/2}end if{Pr（bx=3u1）=p/3Pr（b注意ui我们原则上只能得出结论，Pr（b<$x = 1）=1<$Pr（b<$x = 2）=1<$Pr（b<$x = 3）=1，将P（b）=p一直带到后置条件，然后注意到三个合取项加起来就是b本身的概率，但通常我们希望保持警卫的值，我们在本文的扩展版本中，我们展示了如何通过一个不需要缩放的替代If规则来简化这个证明我们通过分析随机游走进一步说明While规则的使用11相关工作在Coq中表示分布的最重要的工作是由ALEA项目[18]基于[1]的工作。ALEA为单位区间和分布的多个概念引入了自己的公理库。ALEA被设计为直接推理概率程序，并形成了Certicrypt加密工具的基础[4]。在本文中，我们的目标比ALEA的目标要有限得多，我们的目标是表示，即具有有限支持的离散分布。对于这些，一个简单的基于树的对象结构被证明是足够的，并且（非常）容易推理。我们的单位区间是基于Coq实数库，限制为[0， 1]。确定性程序的霍尔逻辑是在C.A. R.霍尔[12]。第一次尝试将这种推理方式扩展到364R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）3512344244概率程序出现在Ramshaw的论文[ 20 ]中{P|b} c1{Q1}{P| <$b}c2{Q2}{P}ifbthenc1elsec2{Q1+Q2}其中|b（发音为“A restricted to b“）将谓词分解为“频率”（或子分布），其中b为真，b为假。结论中的加运算符意味着分布的一部分满足Q1，另一部分满足Q2。关于子分布的推理带来了许多我们试图避免的困难，包括Pr（t）= 1在任何严格子分布中都不成立的限制。Den Hartog和De Vink操作员：{b？P}c1{Q1}{<$b？P}c2{Q2}{P}ifbthenc1elsec2{Q1+Q2}有趣的是，？它主要定义在状态分布上，而不是断言。修改他们的例子（使用多集符号），如果Θ ={（θ1，1），（θ2，1），（θ3，1）}，其中θ1和θ3满足b，则b？Θ ={（θ1，1），（θ3，1）}和<$b？Θ ={（θ2，1）}。然后B？P（Θ）断言存在状态ΘJ使得b？ΘJ = Θ和P（Θ）。如何将这一点与其他逻辑结合起来还不清楚，但这需要涉及削弱。同样，后置条件涉及两个子分布。应用pH While规则有两个充分的条件：要么循环是“终止的”（保证在所有状态上终止），要么是“闭合的”，这意味着每次迭代终止的概率有一个下限。虽然第一个条件似乎难以保证，但后者允许我们对PrImp范围之外的一系列程序进行推理。另一方面，它有一个重要的局限性，即它不能推理潜在的非终止程序。Chadha等人。[6]采用了一种类似于我们的方法来处理没有While循环的语言，并证明了它们逻辑的完整性。他们对Toss规则采取了一种有趣的方法，就像赋值规则一样，Toss规则要求我们以后置条件的形式重写前置条件。例如，我们使用以下三元组来获得抛硬币时的后置条件P（y）=1，偏置三分之一：121 1 1{3P（t）+3P（f）=3}y：= toss（3）{Pr（y）=3}。考虑到标识符也不能出现在这里的前提条件中（不像赋值，我们可以赋值x：=x+1），这它们的If规则采用以下形式：{P1}c1{Pr（X）=p1}{P2}c2{Pr（X）=p2}{P1/b<$P2/<$b}ifbthenc1elsec2{Pr（X）=p1+p2}R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351365P/B类似于我们的P|y，在断言中的所有概率项中插入Rbb。然而，子断言没有缩放，相反，我们再次在子概率空间中对它们进行推理 为了允许我们合并后置条件，它包括了一个重要的限制，即两个分支的后置条件必须引用相同的概率-通常这需要显著的弱化。为了推导出一个复杂的后置条件，我们需要反复应用If规则，并通过合取和析取规则连接结果有趣的是，这个限制该版本使用了一个替代的If命令，该命令接受一个免费的布尔标识符，并根据哪个分支将其设置为t或f。这允许形式P1/y<$P2/<$y（其中y是新的标识符）的后置条件，代价是非标准的If规则和新标识符的扩散在相关的形式系统中也做了大量的工作，包括概率保护命令语言[17]（在HOL 4[13]和Isabelle/HOL [8]中形式化），动态逻辑[11，15]和带有测试的Kleene代数[16]。我们建议读者参考Vasquez et al.[22]对概率霍尔逻辑和pGCL进行了比较，并与Chadha等人的相关工作部分进行了比较。[6]对概率验证方法进行最后，与上面提到的Certicrypt项目相关[4]，EasyCrypt加密工具[2]基于两个逻辑系统：pRHL，用于同时推理两个程序的概率关系Hoare逻辑和pHL，用于推理单个程序的概率Hoare逻辑。在Barthe等人[3]中介绍，pRHL基于BentonpHL（在Easy- crypt教程[2]和其他地方简要讨论过）从概率方面解释了从一个状态到另一个状态的转换Easycrypt演示了概率Hoare逻辑在密码设置中的实用性。12今后工作PrImp和VPHL都受到设计的限制。PrImp表达式仅限于布尔和自然数;为了便于分析，我们VPHL同样受到潜在的量化器将允许我们表达关键的想法，如独立性：A和B在Θ i中独立阿尔普，qs.t. Pr（A）=p<$Pr（B）=q<$Pr（A<$B）=pq.VPHL的目的是为概率Hoare逻辑的进一步研究及其应用提供基础。它是可扩展的，这意味着我们可以在不影响语言的情况下添加新规则。新的霍尔规则将分为两类：核心规则和派生规则。核心规则是指在霍尔逻辑中是合理的，但在现有规则的上下文中不是多余的。任何新的核心规则在形式上都可能是类似的366R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351在[6]中的规则。他们会强调完整性而不是可用性，并创建一组可用于推导任何有效Hoare三元组的规则派生规则是可以使用来自逻辑的现有规则派生的规则。尽管从严格意义上讲，这些规则是多余的，但它们使我们能够有效地、直观地推理程序。将这些规则添加到我们的逻辑中可能会对其可用性产生重大影响。在本文中，我们我们设想了一系列用于各种概率结构的规则，扩展了我们对上面的CNORM规则所做的工作。有许多领域，包括密码学，隐私，机器学习和随机算法，这需要正式的分析方法，以及相应的领域特定逻辑，可以针对这些问题进行定制。VPHL应该为今后的工作提供一个坚实的基础引用[1] Audebaud，P.和C. Paulin-Mohring，Proofs of Randomized Algorithms in Coq，Science of ComputerProgramming74（2009），pp. 568-589。[2] Barthe，G.，F. 迪普雷苏瓦湾格雷瓜尔角昆茨湾S. chlobin和P.- Y. Strub，Easycrypt：Atutorial，in：Foundations of Security Analysis and Design VII，Springer，2014 pp. 146比166[3] Barthe，G.，B. G r'egoire，S. Heraud和S. Z. B'eguelin，计算机辅助加密程序的安全性，在：密码学进展-密码学PTO 2011年，施普林格，2011年71比90[4] Barthe，G.，B. G r′egoire和S. ZanellaB'eguelin，Code-bas edcrypt ographicproofs的F ormal certification，in：Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of ProgrammingLanguages，POPL '09（2009），pp. 90比101[5] 本顿，N.， 用于静态分析和程序转换的简单关系正确性证明，第31届ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages，POPL14-25[6] 查达河，L. Cruz-Filipe，P. Mateus和A. Sernadas，Reasoning about probabilistic sequentialprograms，Theoretical Computer Science379（2007），pp.142-165[7] 查达河，P. Mateus和A. Sernadas，Reasoning about states of probabilistic sequential programs，in：Computer Science Logic，Springer，2006，pp.240-255[8] Cock，D.，在Isabelle中使用pGCL验证概率正确性，在：第7次系统软件验证会议，悉尼，澳大利亚，2012年，第100页。1比10[9] Coq开发团队，http://coq.inria.fr/doc网站。[10] Den Hartog，J.和E.P. de Vink，《使用Hoare类逻辑的概率程序》，国际计算机科学基础杂志13（2002），pp.315-340[11] Feldman ， Y. A.和 D. Harel， 概 率 动 态 逻 辑 ， 在 ： 第 十 四 届 ACM 计 算 理 论 研 讨 会 论 文 集 ， STOC'82（1982），pp. 181-195.[12]霍尔角A. R.，计算机程序设计的公理基础，ACM通信12（1969），pp. 576-580。[13] Hurd，J.，A. McIver和C. Morgan，Probably guarded commands mechanically in HOL，TheoreticalComputer Science346（2005），pp.96比112[14] Kozen，D.，Semantics of probabilistic programs，Journal of Computer and System Sciences22（1981），pp. 328-350[15] Kozen，D.，A probabilistic pdl，Journal of Computer and System Sciences30（1985），pp.162-178。R. Rand，S.Zdancewic/电子笔记理论计算机科学319（2015）351
我的内容管理
展开
