论文标题
在证明中将陆上公民视为一流的公民
Treating for-Loops as First-Class Citizens in Proofs
论文作者
论文摘要
已证明索引循环示波器是创建声音循环不变规则的有用工具，以突然完成（例如Java）为编程语言创建声音循环规则。这些规则不需要对循环主体进行程序转换，就像处理突然完成的其他方法一样。但是，索引循环范围专门为提供循环循环和工作相当不透明的循环规则而设计。在这里，我们建议用更透明的解决方案替换索引循环范围，这也使我们可以将此想法从循环扩展到循环。我们进一步介绍了段，做和循环的声音循环展开规则，这些规则既不需要循环主体的程序转换，也不需要使用嵌套方式。这种方法允许将循环视为证明的一流公民 - 而不是将循环转换为循环的通常方法 - 这使得半自动化的证据更加透明，更易于遵循用户，以便用户可能需要进行交互才能关闭证明。
Indexed loop scopes have been shown to be a helpful tool in creating sound loop invariant rules in dynamic logic for programming languages with abrupt completion, such as Java. These rules do not require program transformation of the loop body, as other approaches to dealing with abrupt completion do. However, indexed loop scopes were designed specifically to provide a loop invariant rule for while loops and work rather opaquely. Here we propose replacing indexed loop scopes with a more transparent solution, which also lets us extend this idea from while loops to for loops. We further present sound loop unrolling rules for while, do and for loops, which require neither program transformation of the loop body, nor the use of nested modalities. This approach allows for loops to be treated as first-class citizens in proofs -- rather than the usual approach of transforming for loops into while loops -- which makes semi-automated proofs more transparent and easier to follow for the user, whose interactions may be required in order to close the proofs.
