In this work, we study the fully automated inference of expected result values of probabilistic programs in the presence of natural programming constructs such as procedures, local variables and recursion. While crucial, capturing these constructs becomes highly non-trivial. The key contribution is the definition of a term representation, denoted as infer[.], translating a pre-expectation semantics into first-order constraints, susceptible to automation via standard methods. A crucial step is the use of logical variables, inspired by previous work on Hoare logics for recursive programs. Noteworthy, our methodology is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights. We have implemented this analysis in our prototype ev-imp. We provide ample experimental evidence of the prototype's algorithmic expressibility.
翻译:在这项工作中,我们研究了在程序中包含诸如过程、本地变量和递归等自然编程结构的情况下,完全自动推断概率程序预期结果值的方法。 虽然关键,但捕获这些结构变得非常复杂。关键贡献是定义一个术语表示,称为infer [.],将预期语义转化为一阶约束,可通过标准方法进行自动化。使用逻辑变量是一个关键步骤,受之前关于递归程序Hoare逻辑的工作启发。值得注意的是,我们的方法不限于尾递归,它可以被迭代替换,不需要额外的见解。我们在我们的原型ev-imp中实现了这种分析。我们提供了充分的实验证据,证明了原型算法的表达性。