论文标题
使用验证，vercors，复数和钥匙来检查对象使用情况
On using VeriFast, VerCors, Plural, and KeY to check object usage
论文作者
论文摘要
帕克斯群是一个行为类型的概念，这些概念描述了状态对象的协议，并根据状态机指定了每个状态的可用方法。通常，具有协议的对象要么被迫以线性方式使用，这限制了程序员可以执行的操作，要么需要额外的验证才能验证这些对象可能被别名的程序。为了评估针对对象的语言的静态验证工具的优势和局限性在检查与协议中对共享对象的正确使用时，我们介绍了针对Java的四个工具的调查：Verifast，Vercors，Vercors，Pellural和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.
