On using VeriFast, VerCors, Plural, and KeY to check object usage

Typestates are a notion of behavioral types that describe a protocol for stateful objects, specifying the available methods for each state. Usually, objects with protocols 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 contributions and limitations of static verification tools 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 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.