AutoFrame：面向对象语言的自动框架推理
AutoFrame: Automatic Frame Inference for Object-Oriented Languages
摘要：
自动程序验证已经取得了巨大的进步，但还没有普及。如何让它不那么痛苦？这篇文章解决了其中一个障碍：需要指定明确的“框架子句”，表示哪些属性不会被操作改变。要求潜在的（人类）证明者说明每个操作改变了什么，以及如何改变，这是公平的，但（机械）证明者也需要知道它没有改变什么。指定和验证这些属性的过程是繁琐且容易出错的，并且必须在软件发展时重复。这也很难证明，因为关于代码更改的所有信息都在代码本身中。这里介绍的自动框架工具完全自动执行此分析。它适用于面向对象的编程，其中问题因别名而复杂化：如果x别名为y，则对x. a的任何更新也会影响y. a，即使更新指令通常甚至不提及y。这方面是最微妙的，并在AutoFrame中通过利用配套工具AutoFrame来解决，AutoFrame也以完全自动的方式执行声音和足够精确的别名分析。目前，AutoFrame的一些实际成果是：（1）自动重建（在普通笔记本电脑上大约25秒）的确切框架子句，总共169个子句，用于8，000行数据结构和算法库，该库以前是（用手工编写的框架条款）使用机械程序证明器验证功能正确性;以及（2）自动生成150，000行图形和GUI库的帧条件（少于4分钟）。AutoFrame的源代码和这些示例可供下载。
英文摘要：
Automatic program verification has made tremendous strides, but is not yet for the masses. How do we make it less painful? This article addresses one of the obstacles: the need to specify explicit "frame clauses", expressing what properties are left unchanged by an operation. It is fair enough to ask the would-be (human) prover to state what each operation changes, and how, but the (mechanical) prover also requires knowledge of what it does not change. The process of specifying and verifying these properties is tedious and error-prone, and must be repeated whenever the software evolves. it is also hard to justify, since all the information about what the code changes is in the code itself. The AutoFrame tool presented here performs this analysis entirely automatically. It applies to object-oriented programming, where the issue is compounded by aliasing: if x is aliased to y, any update to x.a also affects y.a, even though the updating instruction usually does not even mention y. This aspect turns out to be the most delicate, and is addressed in AutoFrame by taking advantage of a companion tool, AutoAlias, which performs sound and sufficiently precise alias analysis, also in an entirely automatic way. Some practical results of AutoFrame so far are: (1) the automatic reconstruction (in about 25 seconds on an ordinary laptop) of the exact frame clauses, a total of 169 clauses, for an 8,000-line data structures and algorithms library which was previously (with the manually written frame clauses) verified for functional correctness using a mechanical program prover; and (2) the automatic generation (in less than 4 minutes) of frame conditions for a 150,000-line graphical and GUI library. The source code of AutoFrame and these examples are available for download.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
