Typestate protocol specification in JML. - Taekgoo Kim; Kevin Bierhoff; Jonathan Aldrich; Sungwon Kang (SAVCBS, 2009)