Lightweight Object Specification with Typestates

Previous work has proven typestates to be useful for modeling protocols in object-oriented languages. We build on this work by addressing substitutability of subtypes as well as improving precision and conciseness of specifications. We propose a specification technique for objects based on abstract states that incorporates state refinement, method refinement, and orthogonal state dimensions. Union and intersection types form the underlying semantics of method specifications. The approach guarantees substitutability and behavioral subtyping. We designed a dynamic analysis to check existing object-oriented software for protocol conformance and validated our approach by specifying two standard Java libraries. We provide preliminary evidence for the usefulness of our approach