论文标题
具有规则行为规格的Hoare逻辑
A Hoare Logic with Regular Behavioral Specifications
论文作者
论文摘要
我们提出了一种Hoare逻辑，该逻辑将使用正则表达式扩展程序规格，该表达式根据执行过程中出现的事件序列捕获行为。该想法类似于会话类型或类似过程的行为合同，这两个目前流行的研究方向。此处介绍的方法在表达和证明自动化之间达到了特定的平衡，尤其是它可以捕获多个循环迭代的有趣顺序行为。该方法是模块化的，并且与自动演绎验证工具很好地集成在一起。我们使用两个案例研究描述并证明了我们在SECC中的原型实现：电子邮件地址的匹配项以及验证赌场挑战中游戏步骤的规范。
We present a Hoare logic that extends program specifications with regular expressions that capture behaviors in terms of sequences of events that arise during the execution. The idea is similar to session types or process-like behavioral contracts, two currently popular research directions. The approach presented here strikes a particular balance between expressiveness and proof automation, notably, it can capture interesting sequential behavior across multiple iterations of loops. The approach is modular and integrates well with autoactive deductive verification tools. We describe and demonstrate our prototype implementation in SecC using two case studies: A matcher for E-Mail addresses and a specification of the game steps in the VerifyThis Casino challenge.
