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.

翻译：类型状态是一种行为类型的概念，它通过状态机描述有状态对象的协议，指定每个状态下可用的方法。通常，遵循协议的对象要么被强制以线性方式使用（这会限制程序员的灵活性），要么需要演绎验证来检查这些对象可能存在别名时的程序正确性。为评估面向对象语言中静态验证工具在检查共享协议对象的正确使用方面的优势与局限性，我们针对Java的四种工具（VeriFast、VerCors、Plural和KeY）进行了一项调研。我们实现了文件读取器和链表案例，检测每种工具在对象共享于集合中时静态保证协议合规性及协议完成性的能力，并评估程序员为使代码适配这些工具所需付出的努力。