Hanoi: A Typestate DSL for Java

Iain McGinniss, University of Glasgow, UK

(Joint work with Simon Gay)

Many APIs contain interfaces in which methods have strict state based preconditions, while mainstream programming languages provide no facility to express these constraints in a concise, human readable, machine verifiable form. Failure to detect violations of these preconditions can result in partial or catastrophic failure of a system, therefore programmers must take great care in understanding and verifying the usage of such APIs. We present a domain specific language, Hanoi, which can be used to express state restrictions in APIs. By classifying Hanoi and existing typestate languages and highlighting their differences, we show Hanoi can be more concise and potentially easier to understand than existing approaches. We also present a simple dynamic checking system which uses Hanoi models to verify interface usage, alleviating the burden on the implementer of such interfaces to defend against incorrect usage.