使用VeriFast、VerCors、Plural和KeY检查对象使用情况
On using VeriFast, VerCors, Plural, and KeY to check object usage
摘要：
类型状态是行为类型的一个概念，它描述了有状态对象的协议，用状态机的形式为每个状态指定了可用的方法。通常，带有协议的对象要么被强制以线性方式使用，这限制了程序员可以做什么，要么需要演绎验证来验证这些对象可能被别名化的程序。为了评估面向对象语言的静态验证工具在检查共享对象与协议的正确使用方面的优势和局限性，我们对Java的四种工具进行了调查：VeriFast，VerCors，Plural和KeY。我们描述了一个文件阅读器和一个链表的实现，检查每个工具的能力，静态保证协议的遵守以及协议完成，即使对象是共享的集合，并评估程序员的努力，使代码可以接受这些工具。
英文摘要：
Typestates are a notion of behavioral types that describe protocols for stateful objects, specifying the available methods for each state, in terms of a state machine. Usually, objects with protocol are either forced to be used in a linear way, which restricts what a programmer can do, or deductive verification is required to verify programs where these objects may be aliased. To evaluate the strengths and limitations of static verification tools for object-oriented languages in checking the correct use of shared objects with protocol, we present a survey on four tools for Java: VeriFast, VerCors, Plural, and KeY. We describe the implementation of a file reader and of a linked-list, check for each tool its ability to statically guarantee protocol compliance as well as protocol completion, even when objects are shared in collections, and evaluate the programmer's effort in making the code acceptable to these tools.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
