00000cab a22000003a 4500 UP-99796217608835180 Buklod 20231007234838.0 m |o d | ta 090514s xx d | ||r ||||| || DENGII eng Bierhoff, Kevin Lightweight object specification with typestates. pp. 25 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. Software. Software engineering. Requirements / Specifications. Design tools and techniques. Software / Program Verification. Theory of Computation. Logics and meanings of programs. Specifying and verifying and reasoning about programs. Design. Languages. Reliability. Verification. Behavioral Subtyping. Refinement. Substitutability. Typestate. Union and intersection types. Software engineering notes. 30, 5 (2005). FO UPD DENG-II Article